awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hℒp.meas_ge_lt_top'_enorm hp_ne_zero hp_ne_top hε (by simp)

Premises used: MeasureTheory.MemLp.meas_ge_lt_top'_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ (↑ε : ℝ≥0∞) ≠ 0

Tactic:
simp [hε]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ (↑ε : ℝ≥0∞) = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
simp_rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑ε : ℝ≥0∞) ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp_rw [← ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ (↑ε : ℝ≥0∞) ≠ 0

Tactic:
simp [hε]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑ε : ℝ≥0∞) ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply hℒp.meas_ge_lt_top' hp_ne_zero hp_ne_top (by simp [hε])

Premises used: MeasureTheory.MemLp.meas_ge_lt_top'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 μ
⊢ 0 < q

Tactic:
have hq0_lt : 0 < q := lt_of_lt_of_le hp0_lt hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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)
neg :
  ∀ (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)

Tactic:
by_cases hpq_eq : p = q
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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
pos₃ pos₄ : eLpNorm' f q μ ≤ eLpNorm' f q μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)

Tactic:
rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]

Premises used: sub_self, ENNReal.rpow_zero, mul_one
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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
⊢ p < q

Tactic:
have hpq : p < q := lt_of_le_of_ne hpq hpq_eq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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
a : α
⊢ ‖f a‖ₑ ^ p = (‖f a‖ₑ * g a) ^ p

Tactic:
simp [g]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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
⊢ ∫⁻ (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]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
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)
⊢ (∫⁻ (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)

Tactic:
rw [h_rw]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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)
⊢ 1 / p = 1 / q + 1 / r

Tactic:
simp [field]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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)
⊢ 1 / p = 1 / q + 1 / r

Tactic:
have hpqr : 1 / p = 1 / q + 1 / r := by simp [field]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hf.enorm aemeasurable_const

Premises used: MeasureTheory.AEStronglyMeasurable.enorm, ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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
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)
⊢ (∫⁻ (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:
rw [hpqr]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 / q + 1 / r - 1 / q)

Tactic:
simp [r, g]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 :
  (∫⁻ (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)
⊢ (∫⁻ (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:
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]

Premises used: HMul.hMul, Set.univ, HSub.hSub, HDiv.hDiv, ENorm.enorm, HPow.hPow, MeasureTheory.AEStronglyMeasurable.enorm, OfNat.ofNat, DFunLike.coe, ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr, MeasureTheory.lintegral, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ

Tactic:
lintegral_mono_ae ?_

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
refine : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ

Tactic:
refine lintegral_mono_ae ?_

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ

Tactic:
have h_nnnorm_le_eLpNorm_ess_sup := enorm_ae_le_eLpNormEssSup f μ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 μ
h₂ : 0 ≤ q
⊢ ‖f x‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 μ
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q

Tactic:
exact h_nnnorm_le_eLpNorm_ess_sup.mono fun x hx => by gcongr

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ

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
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
rw :
  (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    HPow.hPow (β := ℝ) (eLpNormEssSup f μ) 1 * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
⊢ eLpNorm' f q μ ≤ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)

Tactic:
rw [eLpNorm', ← ENNReal.rpow_one (eLpNormEssSup f μ)]

Premises used: MeasureTheory.eLpNorm', ENNReal.rpow_one, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
nth_rw :
  (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    eLpNormEssSup f μ ^ (q * q⁻¹) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    HPow.hPow (β := ℝ) (eLpNormEssSup f μ) 1 * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)

Tactic:
nth_rw 2 [← mul_inv_cancel₀ (ne_of_lt hq_pos).symm]

Premises used: mul_inv_cancel₀, Ne.symm, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
⊢ 0 ≤ q⁻¹

Tactic:
simp [hq_pos.le]

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
rw :
  (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ q⁻¹ ≤
    HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ^ q⁻¹
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    eLpNormEssSup f μ ^ (q * q⁻¹) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)

Tactic:
rw [ENNReal.rpow_mul, one_div, ← ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ q⁻¹)]

Premises used: ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, one_div
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
h₁ :
  ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ q⁻¹ ≤
    HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ^ q⁻¹

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∂μ
h₁ h₂ h₃ 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∞)
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ HMul.hMul (β := ℝ≥0∞) (eLpNormEssSup f μ ^ q) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rwa [lintegral_const] at h_le

Premises used: MeasureTheory.lintegral_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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)
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)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
hf : AEStronglyMeasurable f μ
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:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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
⊢ 0 < q

Tactic:
have hq0_lt : 0 < q := hp0.pos.trans_le hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∞)
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)
⊢ 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 ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 : eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤
    eLpNorm f ∞ μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / ENNReal.toReal ∞)

Tactic:
simp only [_root_.div_zero, one_div, ENNReal.toReal_top, sub_zero]

Premises used: sub_zero, one_div, ENNReal.toReal_top, div_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ∞)⁻¹
inr₁ :
  ∀ (hp_top : p ≠ ∞),
    eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ 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 ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
hf : AEStronglyMeasurable f μ
hq0_lt : LT.lt (α := ℝ≥0∞) 0 ∞
hp0 : Ne (α := ℝ≥0∞) ∞ 0
hpq : LE.le (α := ℝ≥0∞) ∞ ∞
⊢ eLpNorm f ∞ μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (ENNReal.toReal ∞)⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ≠ ∞
inr :
  eLpNorm' f p.toReal μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ eLpNorm f ∞ μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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 ≠ ∞
⊢ 0 < p.toReal

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
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⁻¹

Tactic:
(eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos).trans (le_of_eq ?_)

Premises used: MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ, LE.le.trans, le_of_eq