α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
⊢ snorm f p μ' < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
⊢ Memℒp f p
refine' ⟨hf.1.mono' (Measure.absolutelyContinuous_of_le_smul hμ'_le), _⟩
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
⊢ snorm f p (c • μ) < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
⊢ snorm f p μ' < ⊤
refine' (snorm_mono_measure f hμ'_le).trans_lt _
case pos
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : c = 0
⊢ snorm f p (c • μ) < ⊤

case neg
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : ¬c = 0
⊢ snorm f p (c • μ) < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
⊢ snorm f p (c • μ) < ⊤
by_cases hc0 : c = 0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : ¬c = 0
⊢ c ^ ENNReal.toReal (1 / p) * snorm f p μ < ⊤
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : ¬c = 0
⊢ snorm f p (c • μ) < ⊤
rw [snorm_smul_measure_of_ne_zero hc0, smul_eq_mul]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : ¬c = 0
⊢ c ^ ENNReal.toReal (1 / p) ≠ ⊤
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : ¬c = 0
⊢ c ^ ENNReal.toReal (1 / p) * snorm f p μ < ⊤
refine' ENNReal.mul_lt_top _ hf.2.ne
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : ¬c = 0
⊢ c ^ ENNReal.toReal (1 / p) ≠ ⊤
simp [hc, hc0]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.2303726
G : Type ?u.2303729
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : Memℒp f p
hc0 : c = 0
⊢ snorm f p (c • μ) < ⊤
simp [hc0]