awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos :
  ∀ (hpq_eq : p = q),
    eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have neg : ∀ (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
-- 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
hpq_eq : p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have pos : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q - 1 / q)
Tactic: rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]
-- 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
hpq_eq : p = q
pos : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q - 1 / q)
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have pos₁ : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) 0
Tactic: rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]
-- 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
hpq_eq : p = q
pos : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q - 1 / q)
pos₁ : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) 0
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have pos₂ : eLpNorm' f q μ ≤ eLpNorm' f q μ * 1
Tactic: rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]
-- 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
hpq_eq : p = q
pos : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q - 1 / q)
pos₁ : eLpNorm' f q μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) 0
pos₂ : eLpNorm' f q μ ≤ eLpNorm' f q μ * 1
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have pos₃ : eLpNorm' f q μ ≤ eLpNorm' f q μ
Tactic: rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]
-- 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 μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have hpq₁ : p < q
Tactic: have hpq : p < q := lt_of_le_of_ne hpq hpq_eq
-- 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_1 : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun (x : α) ↦ 1
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
Tactic: have h_rw : (∫⁻ a, ‖f a‖ₑ ^ p ∂μ) = ∫⁻ a, (‖f a‖ₑ * g a) ^ p ∂μ :=
    lintegral_congr fun a => by simp [g]
-- 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_1 : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun (x : α) ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have neg : (∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤
  (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
    HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
Tactic: rw [h_rw]
-- 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_1 : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun (x : α) ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
⊢ (∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have hpqr : 1 / p = 1 / q + 1 / r
Tactic: have hpqr : 1 / p = 1 / q + 1 / r := by simp [field]
-- 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_1 : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun (x : α) ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
    (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have rw : (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
  (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
    HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q + 1 / r - 1 / q)
Tactic: rw [hpqr]
-- 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_1 : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun (x : α) ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
have a : (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
  (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) *
    HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
Tactic: calc
    (∫⁻ a : α, (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤
        (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) :=
      ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hf.enorm aemeasurable_const
    _ = (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q) := by
      rw [hpqr]; simp [r, g]
-- 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 ε
q : ℝ
hq_pos : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
have refine : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q
Tactic: refine lintegral_mono_ae ?_
-- 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 ε
q : ℝ
hq_pos : 0 < q
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q
have h_nnnorm_le_eLpNorm_ess_sup : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
Tactic: have h_nnnorm_le_eLpNorm_ess_sup := enorm_ae_le_eLpNormEssSup f μ
-- 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 ε
q : ℝ
hq_pos : 0 < q
h_nnnorm_le_eLpNorm_ess_sup : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
x : α
hx : ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ ‖f x‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q
have h₂ : 0 ≤ q
Tactic: gcongr
-- 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 ε
q : ℝ
hq_pos : 0 < q
⊢ eLpNorm' f q μ ≤ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
Tactic: have h_le : (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ≤ ∫⁻ _ : α, eLpNormEssSup f μ ^ q ∂μ := by
    refine lintegral_mono_ae ?_
    have h_nnnorm_le_eLpNorm_ess_sup := enorm_ae_le_eLpNormEssSup f μ
    exact h_nnnorm_le_eLpNorm_ess_sup.mono fun x hx => by gcongr
-- 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 ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ eLpNorm' f q μ ≤ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have rw : (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
  HPow.hPow (β := ℝ) (eLpNormEssSup f μ) 1 * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
Tactic: rw [eLpNorm', ← ENNReal.rpow_one (eLpNormEssSup f μ)]
-- 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 ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    HPow.hPow (β := ℝ) (eLpNormEssSup f μ) 1 * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have nth_rw : (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
  eLpNormEssSup f μ ^ (q * q⁻¹) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
Tactic: nth_rw 2 [← mul_inv_cancel₀ (ne_of_lt hq_pos).symm]
-- 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 ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    eLpNormEssSup f μ ^ (q * q⁻¹) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have rw : (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ q⁻¹ ≤
  HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ^ q⁻¹
Tactic: rw [ENNReal.rpow_mul, one_div, ← ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ q⁻¹)]
-- 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 ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ q⁻¹ ≤
    HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ^ q⁻¹
have h₁ : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: gcongr
-- 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 ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have h₁ : ∀
  (h_le :
    ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤
      HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)),
  ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rwa [lintegral_const] at h_le
Cleared hypotheses: h_le
-- 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have inl : ∀ (hpq : 0 ≤ q),
  eLpNorm f 0 μ ≤
    eLpNorm f q μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / ENNReal.toReal 0 - 1 / q.toReal)
Tactic: obtain rfl | hp0 := eq_or_ne p 0
Cleared hypotheses: p, 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
inl :
  ∀ (hpq : 0 ≤ q),
    eLpNorm f 0 μ ≤
      eLpNorm f q μ *
        HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / ENNReal.toReal 0 - 1 / q.toReal)
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have inr : ∀ (hp0 : p ≠ 0),
  eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
Tactic: obtain rfl | hp0 := eq_or_ne p 0
-- 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have hq0_lt : 0 < q
Tactic: have hq0_lt : 0 < q := hp0.pos.trans_le 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have inr : ∀ (hpq : p ≤ ∞) (hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞),
  eLpNorm f p μ ≤
    eLpNorm f ∞ μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / ENNReal.toReal ∞)
Tactic: obtain rfl | hq_top := eq_or_ne q ∞
Cleared hypotheses: q, hpq, hq0_lt
-- 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
inr :
  ∀ (hpq : p ≤ ∞) (hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞),
    eLpNorm f p μ ≤
      eLpNorm f ∞ μ *
        HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / ENNReal.toReal ∞)
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have inr₁ : ∀ (hq_top : q ≠ ∞),
  eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
Tactic: obtain rfl | hq_top := eq_or_ne q ∞
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ eLpNorm f p μ ≤
    eLpNorm f ∞ μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / ENNReal.toReal ∞)
have inr : eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: simp only [_root_.div_zero, one_div, ENNReal.toReal_top, sub_zero]
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inr : ∀ (hp0 : Ne (α := ℝ≥0∞) ∞ 0) (hpq : LE.le (α := ℝ≥0∞) ∞ ∞),
  eLpNorm f ∞ μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (ENNReal.toReal ∞)⁻¹
Tactic: obtain rfl | hp_top := eq_or_ne p ∞
Cleared hypotheses: p, hp0, 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
inr :
  ∀ (hp0 : Ne (α := ℝ≥0∞) ∞ 0) (hpq : LE.le (α := ℝ≥0∞) ∞ ∞),
    eLpNorm f ∞ μ ≤
      eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (ENNReal.toReal ∞)⁻¹
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inr₁ : ∀ (hp_top : p ≠ ∞),
  eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: obtain rfl | hp_top := eq_or_ne p ∞
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inr : eLpNorm' f p.toReal μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have hp_pos : 0 < p.toReal
Tactic: have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inr : eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
  eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
Tactic: refine (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos).trans (le_of_eq ?_)
-- 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 : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
have inr : 1 / p.toReal = p.toReal⁻¹
Tactic: congr
-- 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have hp_lt_top : p < ∞
Tactic: have hp_lt_top : p < ∞ := hpq.trans_lt (lt_top_iff_ne_top.mpr hq_top)
-- 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have hp_pos : 0 < p.toReal
Tactic: have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_lt_top.ne
-- 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 : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm f p μ ≤
    eLpNorm f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have inr : eLpNorm' f p.toReal μ ≤
  eLpNorm' f q.toReal μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_lt_top.ne, eLpNorm_eq_eLpNorm' hq0_lt.ne.symm hq_top]