case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p = 0
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)

case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : ¬p = 0
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
by_cases hp0 : p = 0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : ¬p = 0
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
rw [← Ne.def] at hp0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
have hp0_lt : 0 < p := lt_of_le_of_ne (zero_le _) hp0.symm
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
have hq0_lt : 0 < q := lt_of_lt_of_le hp0_lt hpq
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)

case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
by_cases hq_top : q = ∞
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
have hp_lt_top : p < ∞ := hpq.trans_lt (lt_top_iff_ne_top.mpr hq_top)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0_lt.ne' hp_lt_top.ne
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm' f (ENNReal.toReal p) μ ≤
    snorm' f (ENNReal.toReal q) μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
rw [snorm_eq_snorm' hp0_lt.ne.symm hp_lt_top.ne, snorm_eq_snorm' hq0_lt.ne.symm hq_top]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
hpq_real : ENNReal.toReal p ≤ ENNReal.toReal q
⊢ snorm' f (ENNReal.toReal p) μ ≤
    snorm' f (ENNReal.toReal q) μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm' f (ENNReal.toReal p) μ ≤
    snorm' f (ENNReal.toReal q) μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
have hpq_real : p.toReal ≤ q.toReal := by rwa [ENNReal.toReal_le_toReal hp_lt_top.ne hq_top]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
hpq_real : ENNReal.toReal p ≤ ENNReal.toReal q
⊢ snorm' f (ENNReal.toReal p) μ ≤
    snorm' f (ENNReal.toReal q) μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
exact snorm'_le_snorm'_mul_rpow_measure_univ hp_pos hpq_real hf
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p = 0
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
simp [hp0, zero_le]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
⊢ snorm f p μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
⊢ snorm f p μ ≤ snorm f q μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p - 1 / ENNReal.toReal q)
simp only [hq_top, _root_.div_zero, one_div, ENNReal.top_toReal, sub_zero, snorm_exponent_top,
  GroupWithZero.inv_zero]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : p = ⊤
⊢ snorm f p μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹

case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
⊢ snorm f p μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
⊢ snorm f p μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
by_cases hp_top : p = ∞
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
⊢ snorm' f (ENNReal.toReal p) μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
⊢ snorm f p μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
rw [snorm_eq_snorm' hp0 hp_top]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm' f (ENNReal.toReal p) μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
⊢ snorm' f (ENNReal.toReal p) μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0_lt.ne' hp_top
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snormEssSup f μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p) = snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm' f (ENNReal.toReal p) μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
refine' (snorm'_le_snormEssSup_mul_rpow_measure_univ hp_pos).trans (le_of_eq _)
case neg.e_a.e_a
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ 1 / ENNReal.toReal p = (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snormEssSup f μ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal p) = snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
congr
no goals
case neg.e_a.e_a
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ 1 / ENNReal.toReal p = (ENNReal.toReal p)⁻¹
exact one_div _
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : p = ⊤
⊢ snormEssSup f μ ≤ snormEssSup f μ
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : p = ⊤
⊢ snorm f p μ ≤ snormEssSup f μ * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
simp only [hp_top, ENNReal.rpow_zero, mul_one, ENNReal.top_toReal, sub_zero,
  GroupWithZero.inv_zero, snorm_exponent_top]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : q = ⊤
hp_top : p = ⊤
⊢ snormEssSup f μ ≤ snormEssSup f μ
exact le_rfl
no goals
α : Type u_1
E : Type u_2
F : Type ?u.4103402
G : Type ?u.4103405
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ≥0∞
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hp0_lt : 0 < p
hq0_lt : 0 < q
hq_top : ¬q = ⊤
hp_lt_top : p < ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ ENNReal.toReal p ≤ ENNReal.toReal q
rwa [ENNReal.toReal_le_toReal hp_lt_top.ne hq_top]