awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have hppos : 0 < p.toReal
Tactic: have hppos : 0 < p.toReal := ENNReal.toReal_pos hp hp'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ Eq (α := ℝ≥0∞)
    (liminf (fun (n : ℕ) ↦ (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f n x‖ₑ) atTop : ℝ≥0∞)
    ((ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) : ℝ≥0∞)
have refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
Tactic: refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
⊢ Eq (α := ℝ≥0∞)
    (liminf (fun (n : ℕ) ↦ (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f n x‖ₑ) atTop : ℝ≥0∞)
    ((ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) : ℝ≥0∞)
have refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
Tactic: refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
⊢ Eq (α := ℝ≥0∞)
    (liminf (fun (n : ℕ) ↦ (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f n x‖ₑ) atTop : ℝ≥0∞)
    ((ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) : ℝ≥0∞)
have refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
  (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ
Tactic: refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ
⊢ Eq (α := ℝ≥0∞)
    (liminf (fun (n : ℕ) ↦ (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f n x‖ₑ) atTop : ℝ≥0∞)
    ((ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) : ℝ≥0∞)
have refine_4 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
  (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ
Tactic: refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have this : liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
Tactic: have :
    liminf (fun n => (‖f n x‖ₑ) ^ p.toReal) atTop =
      liminf (fun n => (‖f n x‖ₑ)) atTop ^ p.toReal := by
    change
      liminf (fun n => ENNReal.orderIsoRpow p.toReal hppos (‖f n x‖ₑ)) atTop =
        ENNReal.orderIsoRpow p.toReal hppos (liminf (fun n => (‖f n x‖ₑ)) atTop)
    refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm <;>
      isBoundedDefault
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have hx₁ : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
Tactic: rw [this] at hx
Cleared hypotheses: hx, hppos, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have h : HPow.hPow (α := ℝ≥0∞) (liminf (fun (x_1 : ℕ) ↦ ‖f x_1 x‖ₑ) atTop) p.toReal ^ p.toReal⁻¹ < ∞
Tactic: rw [← ENNReal.rpow_one (liminf (‖f · x‖ₑ) atTop), ← mul_inv_cancel₀ hppos.ne.symm,
    ENNReal.rpow_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
⊢ MemLp f ∞ μ
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MemLp f ∞ μ
have rcases : ∀ (C : ℝ) (hC : ∀ (x : X), ‖f x‖ ≤ C), MemLp f ∞ μ
Tactic: rcases hf.bounded_above_of_compact_support h'f with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ MemLp f ∞ μ
have apply : AEStronglyMeasurable f μ
Tactic: apply memLp_top_of_bound ?_ C (Filter.Eventually.of_forall hC)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    eLpNorm f p μ
have rw : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
  (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
have h₁ : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤
  ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ 1 / p.toReal * p.toReal = 1
have refine : p.toReal ≠ 0
Tactic: refine one_div_mul_cancel ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ p.toReal ≠ 0
have rw : ¬(p = 0 ∨ p = ∞)
Tactic: rw [Ne, ENNReal.toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (hypothesis)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal
have this : 1 / p.toReal * p.toReal = 1
Tactic: have : 1 / p.toReal * p.toReal = 1 := by
    refine one_div_mul_cancel ?_
    rw [Ne, ENNReal.toReal_eq_zero_iff]
    exact not_or_intro hp_ne_zero hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal
have rw : (HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal)) ^
    p.toReal ≤
  eLpNorm f p μ ^ p.toReal
Tactic: rw [← ENNReal.rpow_one (ε * μ { x | ε ≤ ‖f x‖ₑ ^ p.toReal }), ← this, ENNReal.rpow_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
⊢ (HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal)) ^
      p.toReal ≤
    eLpNorm f p μ ^ p.toReal
have h₁ : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
  eLpNorm f p μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal
have h : Eq.{u_1 + 1} (α := α → Prop) (fun (x : α) ↦ ε ≤ ‖f x‖ₑ) fun (x : α) ↦ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
Tactic: convert! mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top hf (ε ^ p.toReal) using 4
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ Eq.{u_1 + 1} (α := α → Prop) (fun (x : α) ↦ ε ≤ ‖f x‖ₑ) fun (x : α) ↦ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
have h : ∀ (x : α), ε ≤ ‖f x‖ₑ ↔ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
x : α
⊢ ε ≤ ‖f x‖ₑ ↔ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
have h : ε ≤ ‖f x‖ₑ ↔ ε ≤ ‖f x‖ₑ
Tactic: rw [ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
have pos : ∀ (h : ε = ∞), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
Tactic: by_cases h : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
pos : ∀ (h : ε = ∞), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
have neg : ∀ (h : ¬ε = ∞), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
Tactic: by_cases h : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ε = ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
have rw : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (hypothesis)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ε = ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
have this : HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
Tactic: have : (0 : ℝ≥0∞) ^ p.toReal = 0 := by
      rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (hypothesis)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
have hεpow : ε ^ p.toReal ≠ 0
Tactic: have hεpow : ε ^ p.toReal ≠ 0 := (ENNReal.rpow_pos (pos_iff_ne_zero.2 hε) h).ne.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (hypothesis)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
have hεpow' : ε ^ p.toReal ≠ ∞
Tactic: have hεpow' : ε ^ p.toReal ≠ ∞ := by finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
have neg : HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal
Tactic: rw [ENNReal.inv_rpow, ← ENNReal.mul_le_mul_iff_right hεpow hεpow', ← mul_assoc,
      ENNReal.mul_inv_cancel hεpow hεpow', one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : ε⁻¹ ^ p.toReal < ∞
Tactic: apply meas_ge_le_mul_pow_eLpNorm_enorm μ hp_ne_zero hp_ne_top hℒp.aestronglyMeasurable hε hε'
    |>.trans_lt (ENNReal.mul_lt_top ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
apply : ε⁻¹ ^ p.toReal < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply₁ : eLpNorm f p μ ^ p.toReal < ∞
Tactic: apply meas_ge_le_mul_pow_eLpNorm_enorm μ hp_ne_zero hp_ne_top hℒp.aestronglyMeasurable hε hε'
    |>.trans_lt (ENNReal.mul_lt_top ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (h : ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
pos : ∀ (h : ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (h : ¬ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
have simp_rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑ε : ℝ≥0∞) ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp_rw [← ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have hq0_lt : 0 < q
Tactic: have hq0_lt : 0 < q := lt_of_lt_of_le hp0_lt hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have pos : ∀ (hpq_eq : p = q),
  eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
Tactic: by_cases hpq_eq : p = q