-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm_le_eLpNorm_mul_rpow_measure_univ {p q : ℝ≥0∞} (hpq : p ≤ q)
    (hf : AEStronglyMeasurable f μ) :
    eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : ¬p = 0
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
rw [← Ne] at hp0

Result:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < p.toReal
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' f q.toReal μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
exact eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq_real hf

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
have hq0_lt : 0 < q := lt_of_lt_of_le hp0_lt hpq

Result:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
⊢ eLpNorm' f p.toReal μ ≤ eLpNormEssSup f μ * μ Set.univ ^ p.toReal⁻¹

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

Result:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
⊢ eLpNormEssSup f μ * μ Set.univ ^ (1 / p.toReal) = eLpNormEssSup f μ * μ Set.univ ^ p.toReal⁻¹

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
have hp_lt_top : p < ∞ := hpq.trans_lt (lt_top_iff_ne_top.mpr hq_top)

Result:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Proof state:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : p = ⊤
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup f μ

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
simp only [hq_top, _root_.div_zero, one_div, ENNReal.top_toReal, sub_zero, eLpNorm_exponent_top,
  GroupWithZero.inv_zero]

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
⊢ eLpNorm f p μ ≤ eLpNormEssSup f μ * μ Set.univ ^ p.toReal⁻¹

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p = 0
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : ¬p = 0
⊢ eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
⊢ eLpNormEssSup f μ * μ Set.univ ^ (1 / p.toReal) = eLpNormEssSup f μ * μ Set.univ ^ p.toReal⁻¹

Tactic:
congr

Result:
case neg.e_a.e_a
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
⊢ 1 / p.toReal = p.toReal⁻¹