awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
have pos : eLpNorm f ∞ μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [h_top, eLpNorm_exponent_top, eLpNormEssSup_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
pos : eLpNorm f ∞ μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
have pos₁ : eLpNormEssSup f μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [h_top, eLpNorm_exponent_top, eLpNormEssSup_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
pos : eLpNorm f ∞ μ = 0 ↔ f =ᶠ[ae μ] 0
pos₁ : eLpNormEssSup f μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
have pos₂ : f =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [h_top, eLpNorm_exponent_top, eLpNormEssSup_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
have neg : eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [eLpNorm_eq_eLpNorm' h0 h_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have pos : ∀ (hp_zero : p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
pos : ∀ (hp_zero : p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have neg : ∀ (hp_zero : ¬p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have pos : ∀ (hp_top : p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
pos : ∀ (hp_top : p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have neg : ∀ (hp_top : ¬p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have pos : eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ
Tactic: simp_rw [hp_top, eLpNorm_exponent_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have neg : (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
  (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top,
    lintegral_map' (hg.enorm.pow_const p.toReal) hf, Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg :
  (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have neg₁ : (∫⁻ (a : α), ‖g (f a)‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top,
    lintegral_map' (hg.enorm.pow_const p.toReal) hf, Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑(g.compMeasurePreserving f hf) : α → E) p μ = eLpNorm (↑g : β → E) p ν
have rw : eLpNorm ((↑g : β → E) ∘ f) p μ = eLpNorm (↑g : β → E) p ν
Tactic: rw [eLpNorm_congr_ae (g.coeFn_compMeasurePreserving _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have pos : ∀ (hp_zero : p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
pos : ∀ (hp_zero : p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have neg : ∀ (hp_zero : ¬p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have pos : ∀ (hp : p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
pos : ∀ (hp : p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have neg : ∀ (hp : ¬p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
Tactic: by_cases hp : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
have pos : eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ
Tactic: simp_rw [hp, eLpNorm_exponent_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
⊢ MemLp (m0 := mβ) g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ
have simp_rw : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ) ∧ @eLpNorm _ _ _ mβ g p (Measure.map f μ) < ∞ ↔
  AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞
Tactic: simp_rw [MemLp, hf.aestronglyMeasurable_map_iff, hf.eLpNorm_map_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
simp_rw :
  AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ) ∧ @eLpNorm _ _ _ mβ g p (Measure.map f μ) < ∞ ↔
    AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞
⊢ MemLp (m0 := mβ) g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ
have simp_rw₁ : AEStronglyMeasurable (g ∘ f) μ ∧ @eLpNorm _ _ _ mβ g p (Measure.map f μ) < ∞ ↔
  AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞
Tactic: simp_rw [MemLp, hf.aestronglyMeasurable_map_iff, hf.eLpNorm_map_measure]
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
have pos : ∀ (hp0 : p.toReal = 0), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
Tactic: by_cases hp0 : p.toReal = 0
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
pos : ∀ (hp0 : p.toReal = 0), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
have neg : ∀ (hp0 : ¬p.toReal = 0), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
Tactic: by_cases hp0 : p.toReal = 0
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
have pos : ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞
Tactic: simp only [hp0, ENNReal.rpow_zero]
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞
have pos : ∀ (a : α), LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞
Tactic: filter_upwards with _
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
a : α
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞
have pos : LT.lt (α := ℝ≥0∞) 1 ∞
Tactic: rw [liminf_const (1 : ℝ≥0∞)]
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := fun h => by simp [h] at hp0
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
have hp' : p ≠ ∞
Tactic: have hp' : p ≠ ∞ := fun h => by simp [h] at hp0
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
have neg : liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), (↑‖f i a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) atTop ≤ (↑R : ℝ≥0∞) ^ p.toReal
Tactic: refine
    ae_lt_top (.liminf fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
      (lt_of_le_of_lt
          (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
          (lt_of_le_of_lt ?_ (by finiteness : (R : ℝ≥0∞) ^ p.toReal < ∞))).ne
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), (↑‖f i a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) atTop ≤ (↑R : ℝ≥0∞) ^ p.toReal
have hbdd₁ : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (↑R : ℝ≥0∞)
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp hp', one_div] at hbdd
Cleared hypotheses: hbdd
-- 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (↑R : ℝ≥0∞)
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), (↑‖f i a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) atTop ≤ (↑R : ℝ≥0∞) ^ p.toReal
have neg : sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), (↑‖f b a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ} ≤ (↑R : ℝ≥0∞) ^ p.toReal
Tactic: simp_rw [liminf_eq, eventually_atTop]
-- 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∞)
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have pos : ∀ (hp' : p = ∞), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
Tactic: by_cases hp' : p = ∞
-- 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∞)
pos : ∀ (hp' : p = ∞), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have neg : ∀ (hp' : ¬p = ∞), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
Tactic: by_cases hp' : p = ∞
-- 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 : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have hp₁ : Ne (α := ℝ≥0∞) ∞ 0
Tactic: subst hp'
Cleared hypotheses: p, hp, hbdd, hp'
-- 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 = ∞
hp₁ : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have hbdd₁ : ∀ (n : ℕ), eLpNorm (f n) ∞ μ ≤ (↑R : ℝ≥0∞)
Tactic: subst hp'
Cleared hypotheses: p, hp, hbdd, hp'
-- 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
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNorm (f n) ∞ μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have hbdd₁ : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
Tactic: simp_rw [eLpNorm_exponent_top] at hbdd
Cleared hypotheses: hbdd
-- 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
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < (↑R : ℝ≥0∞) + 1
Tactic: have : ∀ n, ∀ᵐ x ∂μ, (‖f n x‖ₑ) < R + 1 := fun n =>
      ae_lt_of_essSup_lt
        (lt_of_le_of_lt (hbdd n) <| ENNReal.lt_add_right ENNReal.coe_ne_top one_ne_zero)
-- 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
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < (↑R : ℝ≥0∞) + 1
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have this₁ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1
Tactic: rw [← ae_all_iff] at this
Cleared hypotheses: 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
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞) x} x}
    a
Tactic: filter_upwards [this] with x hx using lt_of_le_of_lt
        (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
        (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)
-- 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
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have h₁ : ∀ (a : α), (∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1) → LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n a‖ₑ) atTop) ∞
Tactic: filter_upwards [this] with x hx using lt_of_le_of_lt
        (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
        (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)
-- 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 : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
have h : ∀ (x : α) (hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞),
  LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
Tactic: filter_upwards [ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd hfmeas hbdd] with x hx