case inl
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ snorm' f p μ < ⊤

case inr
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ snorm' f p μ < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
⊢ snorm' f p μ < ⊤
cases' le_or_lt p 0 with hp_nonpos hp_pos
case inr
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ snorm' f p μ < ⊤
case inr
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ snorm' f p μ < ⊤
have hq_pos : 0 < q := lt_of_lt_of_le hp_pos hpq
no goals
case inr
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ snorm' f p μ < ⊤
calc
  snorm' f p μ ≤ snorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) :=
    snorm'_le_snorm'_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]
case inl
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ snorm' f 0 μ < ⊤
case inl
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ snorm' f p μ < ⊤
rw [le_antisymm hp_nonpos hp_nonneg]
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ snorm' f 0 μ < ⊤
simp
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ snorm' f q μ < ⊤ ∧ ↑↑μ Set.univ ^ (1 / p - 1 / q) < ⊤ ∨ snorm' f q μ = 0 ∨ ↑↑μ Set.univ ^ (1 / p - 1 / q) = 0
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q) < ⊤
rw [ENNReal.mul_lt_top_iff]
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ snorm' f q μ < ⊤ ∧ ↑↑μ Set.univ ^ (1 / p - 1 / q) < ⊤ ∨ snorm' f q μ = 0 ∨ ↑↑μ Set.univ ^ (1 / p - 1 / q) = 0
refine' Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg _ (measure_ne_top μ Set.univ)⟩
no goals
α : Type u_1
E : Type u_2
F : Type ?u.4187857
G : Type ?u.4187860
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
p q : ℝ
inst✝ : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
hfq_lt_top : snorm' f q μ < ⊤
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q
rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv hq_pos hp_pos]