-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem MemLp.mono_exponent {p q : ℝ≥0∞} [IsFiniteMeasure μ] {f : α → E} (hfq : MemLp f q μ)
    (hpq : p ≤ q) : MemLp f p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : ¬q = ⊤
⊢ q ≠ 0

Tactic:
by_contra hq_eq_zero

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : ¬q = ⊤
hq_eq_zero : q = 0
⊢ False

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q.toReal μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : ¬q = ⊤
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ < ⊤

Tactic:
exact eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le hfq_m hfq_lt_top hp_pos.le hpq_real

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ eLpNorm f p μ < ⊤

Tactic:
have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : p = ⊤
hq_top : q = ⊤
⊢ eLpNorm f p μ < ⊤

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : ¬q = ⊤
hq_eq_zero : q = 0
⊢ False

Tactic:
have hp_eq_zero : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) (zero_le _)

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : ¬q = ⊤
hq_eq_zero : q = 0
hp_eq_zero : p = 0
⊢ False

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hfq : MemLp f q μ
hpq : p ≤ q
⊢ MemLp f p μ

Tactic:
obtain ⟨hfq_m, hfq_lt_top⟩ := hfq

Result:
case intro
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
⊢ MemLp f p μ

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
⊢ eLpNorm f p μ < ⊤

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ eLpNorm f p μ < ⊤

case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p μ < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : q = ⊤
⊢ eLpNorm' f p.toReal μ < ⊤

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : q = ⊤
⊢ eLpNorm' f p.toReal μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p μ < ⊤

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top

Result:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
⊢ eLpNorm f p μ < ⊤

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ q = ⊤

Tactic:
rwa [hp_top, top_le_iff] at hpq

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
⊢ eLpNorm f p μ < ⊤

Tactic:
by_cases hq_top : q = ∞

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : q = ⊤
⊢ eLpNorm f p μ < ⊤

case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : ¬q = ⊤
⊢ eLpNorm f p μ < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : q = ⊤
⊢ eLpNorm f p μ < ⊤

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Result:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
f : α → E
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ⊤
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < p.toReal
hq_top : q = ⊤
⊢ eLpNorm' f p.toReal μ < ⊤