-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le {p q : ℝ} [IsFiniteMeasure μ]
    (hf : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm' f q μ < ∞) (hp_nonneg : 0 ≤ p)
    (hpq : p ≤ q) : eLpNorm' f p μ < ∞

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) < ⊤

Tactic:
rw [ENNReal.mul_lt_top_iff]

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ < ⊤ ∧ μ Set.univ ^ (1 / p - 1 / q) < ⊤ ∨ eLpNorm' f q μ = 0 ∨ μ Set.univ ^ (1 / p - 1 / q) = 0

Proof state:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f p μ < ⊤

Tactic:
rw [le_antisymm hp_nonpos hp_nonneg]

Result:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f 0 μ < ⊤

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
⊢ eLpNorm' f p μ < ⊤

Tactic:
rcases le_or_lt p 0 with hp_nonpos | hp_pos

Result:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f p μ < ⊤

case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ eLpNorm' f p μ < ⊤

Proof state:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f p μ < ⊤

Tactic:
calc
  eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) :=
    eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq hf
  _ < ∞ := by
    rw [ENNReal.mul_lt_top_iff]
    refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (measure_ne_top μ Set.univ)⟩
    rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Result:
no goals

Proof state:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ eLpNorm' f p μ < ⊤

Tactic:
have hq_pos : 0 < q := lt_of_lt_of_le hp_pos hpq

Result:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f p μ < ⊤

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ < ⊤ ∧ μ Set.univ ^ (1 / p - 1 / q) < ⊤ ∨ eLpNorm' f q μ = 0 ∨ μ Set.univ ^ (1 / p - 1 / q) = 0

Tactic:
refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (measure_ne_top μ Set.univ)⟩

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q

Proof state:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f 0 μ < ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q

Tactic:
rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Result:
no goals