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 ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p (μ.restrict s) = eLpNorm 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 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
have pos : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.restrict s)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)
Tactic: simp only [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
-- 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 ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
have neg : (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top, eLpNorm'_eq_lintegral_enorm]
-- 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 ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
have neg : ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
Tactic: congr 1
-- 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 ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
have neg : (Function.support (M := ℝ≥0∞) fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s
Tactic: apply setLIntegral_eq_of_support_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ (Function.support (M := ℝ≥0∞) fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s
have this : ¬p.toReal ≤ 0
Tactic: have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have simp_rw : eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
Tactic: simp_rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
have rw : c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
Tactic: rw [eLpNorm'_smul_measure ENNReal.toReal_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
have e_a : 1 / p.toReal = (1 / p).toReal
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ 1 / p.toReal = (1 / p).toReal
have e_a : p.toReal⁻¹ = p⁻¹.toReal
Tactic: simp_rw [one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ p.toReal⁻¹ = p⁻¹.toReal
have e_a : p.toReal⁻¹ = p.toReal⁻¹
Tactic: rw [ENNReal.toReal_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have pos : ∀ (hp0 : p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
pos : ∀ (hp0 : p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have neg : ∀ (hp0 : ¬p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have pos : ∀ (hp_top : p = ∞), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm 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 α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm 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 α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ (↑c : ℝ≥0∞) ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
have simp : (↑c : ℝ≥0∞) ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ (↑c : ℝ≥0∞) ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
have norm_cast : (↑(c ^ p.toReal⁻¹) : ℝ≥0∞) * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have pos : ∀ (hp0 : p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
pos : ∀ (hp0 : p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
have neg : ∀ (hp0 : ¬p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ
have this : 0 ≤ p.toReal⁻¹
Tactic: have : 0 ≤ p.toReal⁻¹ := by positivity
-- 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 ε
hp : p ≠ ∞
c : ℝ≥0
f : α → ε
this : 0 ≤ p.toReal⁻¹
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ
have refine : (↑c : ℝ≥0∞) ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
Tactic: refine (eLpNorm_smul_measure_of_ne_top hp ..).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ
have rw : c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ
Tactic: rw [eLpNorm_smul_measure_of_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
c : ℝ≥0∞
rw : c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ
⊢ eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ
have hp_ne_top : Ne (α := ℝ≥0∞) 1 ∞
Tactic: rw [eLpNorm_smul_measure_of_ne_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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ MemLp f p μ'
have refine : eLpNorm f p μ' < ∞
Tactic: refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩
-- 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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ eLpNorm f p μ' < ∞
have refine : eLpNorm f p (c • μ) < ∞
Tactic: refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_
-- 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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ eLpNorm f p (c • μ) < ∞
have pos : ∀ (hc0 : c = 0), eLpNorm f p (c • μ) < ∞
Tactic: by_cases hc0 : c = 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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
pos : ∀ (hc0 : c = 0), eLpNorm f p (c • μ) < ∞
⊢ eLpNorm f p (c • μ) < ∞
have neg : ∀ (hc0 : ¬c = 0), eLpNorm f p (c • μ) < ∞
Tactic: by_cases hc0 : c = 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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ eLpNorm f p (c • μ) < ∞
have neg : c ^ (1 / p).toReal * eLpNorm f p μ < ∞
Tactic: rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul]
-- 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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal * eLpNorm f p μ < ∞
have neg : c ^ (1 / p).toReal ≠ ∞
Tactic: refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst : ENorm ε
f : α → ε
μ ν : Measure α
⊢ eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν
have simp_rw : ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
Tactic: simp_rw [eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst : ENorm ε
f : α → ε
μ ν : Measure α
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
have rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
Tactic: rw [lintegral_add_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 ε
f : α → ε
h : MemLp f p μ
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ < ∞
have simp_rw : eLpNorm f p μ < ∞
Tactic: simp_rw [MeasureTheory.eLpNorm_enorm, h.eLpNorm_lt_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 ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm f p μ < ∞
have rw : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ < ∞
Tactic: rw [← eLpNorm_enorm]
-- 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
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
⊢ eLpNorm f p μ < ∞
have rw : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ < ∞
Tactic: rw [← eLpNorm_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
hq0_lt : 0 < q
hf_zero : f =ᶠ[ae μ] 0
⊢ eLpNorm' f q μ = 0
have rw : eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
Tactic: rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero hq0_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
hq0_lt : 0 < q
hf_zero : f =ᶠ[ae μ] 0
rw : eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
⊢ eLpNorm' f q μ = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero hq0_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
f : α → ε
hf_zero : f =ᶠ[ae μ] 0
⊢ eLpNorm' f q μ = 0
have rw : eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
Tactic: rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero' hq0_ne hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
f : α → ε
hf_zero : f =ᶠ[ae μ] 0
rw : eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
⊢ eLpNorm' f q μ = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero' hq0_ne hμ]
-- 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 : ESeminormedAddMonoid ε
f : α → ε
hf : f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0
have rw : eLpNorm f p μ = eLpNorm.{u_1, u_7} (ε := ε) 0 p μ
Tactic: rw [← eLpNorm_zero (p := p) (μ := μ) (α := α) (ε := ε)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
p : ℝ
hp : 0 < p
hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ = 0
have rw : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = enorm.{u_7} (E := ε) (0 x)
Tactic: rw [← eLpNorm'_zero hp (μ := μ) (ε := ε), eLpNorm'_congr_enorm_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x (eLpNormEssSup f μ).toNNReal
have simp_rw : ∀ᶠ (x : ℝ≥0) in map (fun (x : α) ↦ ‖f x‖₊) (ae μ), (↑x : ℝ≥0∞) ≤ eLpNormEssSup f μ
Tactic: simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
⊢ eLpNorm f p μ < ∞
have inl : eLpNorm f 0 μ < ∞
Tactic: obtain rfl | hp₀ := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
inl : eLpNorm f 0 μ < ∞
⊢ eLpNorm f p μ < ∞
have inr : ∀ (hp₀ : p ≠ 0), eLpNorm f p μ < ∞
Tactic: obtain rfl | hp₀ := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
⊢ eLpNorm f p μ < ∞
have inr : ∀ (hp₀ : Ne (α := ℝ≥0∞) ∞ 0), eLpNorm f ∞ μ < ∞
Tactic: obtain rfl | hp := eq_or_ne p ∞
Cleared hypotheses: p, hp₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
inr : ∀ (hp₀ : Ne (α := ℝ≥0∞) ∞ 0), eLpNorm f ∞ μ < ∞
⊢ eLpNorm f p μ < ∞
have inr₁ : ∀ (hp : p ≠ ∞), eLpNorm f p μ < ∞
Tactic: obtain rfl | hp := eq_or_ne p ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ eLpNorm f ∞ μ < ∞
have inr : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) fun (x : α) ↦ ‖f x‖₊
Tactic: simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ eLpNorm f p μ < ∞
have inr : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
have inr : ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖ₑ ^ p.toReal ≤ (↑c : ℝ≥0∞)
Tactic: refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖ₑ ^ p.toReal ≤ (↑c : ℝ≥0∞)
have inr : ∃ (c : ℝ≥0), ∀ (x : α), (↑(‖f x‖₊ ^ p.toReal) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)
Tactic: simp_rw [enorm, ← ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∃ (c : ℝ≥0), ∀ (x : α), (↑(‖f x‖₊ ^ p.toReal) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)
have inr : ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : eLpNorm' f q μ = 0
⊢ f =ᶠ[ae μ] 0
have h₁ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
Tactic: simp only [eLpNorm'_eq_lintegral_enorm, lintegral_eq_zero_iff' (hf.enorm.pow_const q), one_div,
    ENNReal.rpow_eq_zero_iff, inv_pos, inv_neg'', hq0.not_gt, and_false, or_false] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
⊢ f =ᶠ[ae μ] 0
have refine : ∀ (x : α) (hx : Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖f a‖ₑ ^ q) x) (0 x)), f x = 0 x
Tactic: refine h.left.mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
x : α
hx : Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖f a‖ₑ ^ q) x) (0 x)
⊢ f x = 0 x
have hx₁ : f x = 0 ∧ 0 < q
Tactic: simp only [Pi.ofNat_apply, ENNReal.rpow_eq_zero_iff, enorm_eq_zero, h.2.not_gt, and_false,
    or_false] at hx
Cleared hypotheses: hx
-- 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
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
have pos : ∀ (h_top : p = ∞), eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: by_cases h_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 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
have neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: by_cases h_top : p = ∞