awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₇ : (∫⁻ (a : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
Tactic: simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm,
    Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]
-- 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
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₇ : (∫⁻ (a : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₈ : (∫⁻ (a : α), ENNReal.ofReal |‖f a‖ ^ q| ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
Tactic: simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm,
    Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]
-- 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
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₇ : (∫⁻ (a : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₈ : (∫⁻ (a : α), ENNReal.ofReal |‖f a‖ ^ q| ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₉ : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
Tactic: simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm,
    Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]
-- 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
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₇ : (∫⁻ (a : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₈ : (∫⁻ (a : α), ENNReal.ofReal |‖f a‖ ^ q| ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₉ : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₁₀ : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (q * p) ∂μ) ^ p⁻¹
Tactic: simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm,
    Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]
-- 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
p q : ℝ
hq_pos : 0 < q
simp_rw : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
simp_rw₁ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
simp_rw₂ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw₃ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
simp_rw₄ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))
simp_rw₅ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
simp_rw₆ : (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₇ : (∫⁻ (a : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₈ : (∫⁻ (a : α), ENNReal.ofReal |‖f a‖ ^ q| ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₉ : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
simp_rw₁₀ :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (q * p) ∂μ) ^ p⁻¹
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q
have simp_rw₁₁ : (∫⁻ (a : α), (ENNReal.ofReal ‖f a‖ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (q * p) ∂μ) ^ p⁻¹
Tactic: simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm,
    Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have pos : ∀ (h0 : p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
pos : ∀ (h0 : p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have neg : ∀ (h0 : ¬p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have pos : ∀ (hp_top : p = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have pos : essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q
Tactic: simp only [hp_top, eLpNorm_exponent_top, ENNReal.top_mul', hq_pos.not_ge,
      ENNReal.ofReal_eq_zero, if_false, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
⊢ essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q
have h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
Tactic: have h_rpow : essSup (‖‖f ·‖ₑ ^ q‖ₑ) μ = essSup (‖f ·‖ₑ ^ q) μ := by congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
⊢ essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q
have h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ q
Tactic: have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hq_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ)
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ q
⊢ essSup (fun (x : α) ↦ ‖f x‖ₑ ^ q) μ = HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) q
have h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ q
Tactic: have h_rpow_surj := (ENNReal.rpow_left_bijective hq_pos.ne.symm).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have neg : eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q
Tactic: rw [eLpNorm_eq_eLpNorm' h0 hp_top, eLpNorm_eq_eLpNorm' _ (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
neg : eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have rw : p * ENNReal.ofReal q ≠ 0
Tactic: rw [eLpNorm_eq_eLpNorm' h0 hp_top, eLpNorm_eq_eLpNorm' _ (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ p * ENNReal.ofReal q ≠ 0
have refine : ENNReal.ofReal q ≠ 0
Tactic: refine mul_ne_zero h0 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ ENNReal.ofReal q ≠ 0
have rwa : ¬ENNReal.ofReal q = 0
Tactic: rwa [Ne, ENNReal.ofReal_eq_zero, not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
rwa : ¬ENNReal.ofReal q = 0
⊢ ENNReal.ofReal q ≠ 0
have rwa₁ : ¬q ≤ 0
Tactic: rwa [Ne, ENNReal.ofReal_eq_zero, not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q
have neg : eLpNorm' (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q
Tactic: rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal hq_pos.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q
have rw : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ
Tactic: rw [← eLpNorm_enorm_rpow f hq_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ = eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ
have symm : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
⊢ ∀ᵐ (x : α) ∂μ, LE.le (α := ℝ) 0 ((fun (x : α) ↦ ‖f x‖ ^ q) x)
have h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) 0 ((fun (x : α) ↦ ‖f x‖ ^ q) x)) x} a
Tactic: filter_upwards with x using by positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) 0 ((fun (x : α) ↦ ‖f x‖ ^ q) x)) x} a
⊢ ∀ᵐ (x : α) ∂μ, LE.le (α := ℝ) 0 ((fun (x : α) ↦ ‖f x‖ ^ q) x)
have h₁ : ∀ (a : α), 0 ≤ ‖f a‖ ^ q
Tactic: filter_upwards with x using by positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) p μ
have h : ∀ (x : α), ‖f x‖ₑ ^ q = (ENNReal.ofReal ∘ fun (x : α) ↦ ‖f x‖ ^ q) x
Tactic: convert! eLpNorm_ofReal (fun x ↦ ‖f x‖ ^ q) (by filter_upwards with x using by positivity)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hq_pos : 0 < q
x : α
⊢ ‖f x‖ₑ ^ q = (ENNReal.ofReal ∘ fun (x : α) ↦ ‖f x‖ ^ q) x
have h : ENNReal.ofReal ‖f x‖ ^ q = ENNReal.ofReal (‖f x‖ ^ q)
Tactic: rw [Function.comp_apply, ← ofReal_norm]
-- 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 ε
inst_2 : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ MemLp f p μ
have apply : ∀ (_x : α) (hx : ‖f _x‖ₑ ≤ C), ‖f _x‖ₑ ≤ ‖C‖ₑ
Tactic: apply (memLp_const_enorm hC).of_le_enorm (ε' := ℝ≥0∞) hf <| hfC.mono fun _x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
f : α → ℝ
h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b
hX : AEStronglyMeasurable f μ
p : ℝ≥0∞
ha : ∀ᵐ (x : α) ∂μ, a ≤ f x
hb : ∀ᵐ (x : α) ∂μ, f x ≤ b
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖f a_1‖ ≤ max |a| |b|
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ f x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ b) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖f a_4‖ ≤ max |a| |b|) x} x}
          x}
    a_1
Tactic: filter_upwards [ha, hb] with x using abs_le_max_abs_abs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
f : α → ℝ
h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b
hX : AEStronglyMeasurable f μ
p : ℝ≥0∞
ha : ∀ᵐ (x : α) ∂μ, a ≤ f x
hb : ∀ᵐ (x : α) ∂μ, f x ≤ b
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ b) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖f a_4‖ ≤ max |a| |b|) x} x}
            x}
      a_1
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖f a_1‖ ≤ max |a| |b|
have h₂ : ∀ (a_1 : α), a ≤ f a_1 → f a_1 ≤ b → ‖f a_1‖ ≤ max |a| |b|
Tactic: filter_upwards [ha, hb] with x using abs_le_max_abs_abs
-- 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 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν) ^ (1 / q) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
have h₂ : 0 ≤ 1 / q
Tactic: gcongr
-- 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μν : ν ≤ μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ
have pos : ∀ (hp0 : p = 0), eLpNorm f p ν ≤ 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 α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
pos : ∀ (hp0 : p = 0), eLpNorm f p ν ≤ eLpNorm f p μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ
have neg : ∀ (hp0 : ¬p = 0), eLpNorm f p ν ≤ 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 α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ
have pos : ∀ (hp_top : p = ∞), eLpNorm f p ν ≤ 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 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p ν ≤ eLpNorm f p μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p ν ≤ 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 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p ν ≤ eLpNorm f p μ
have neg : eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ
Tactic: simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_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 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
have pos : ∀ (hp0 : p = 0), eLpNorm f p (μ.restrict s) = 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 α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
pos : ∀ (hp0 : p = 0), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
have neg : ∀ (hp0 : ¬p = 0), eLpNorm f p (μ.restrict s) = 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 α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
have pos : ∀ (hp_top : p = ∞), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
Tactic: by_cases hp_top : p = ∞