α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
⊢ ENNReal.toNNReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toNNReal (snorm (↑↑g) p μ)
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
⊢ ‖f‖₊ ≤ c * ‖g‖₊
simp only [nnnorm_def]
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : snorm (fun x => ↑↑f x) p μ ≤ c • snorm (fun x => ↑↑g x) p μ
⊢ ENNReal.toNNReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toNNReal (snorm (↑↑g) p μ)
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
⊢ ENNReal.toNNReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toNNReal (snorm (↑↑g) p μ)
have := snorm_le_nnreal_smul_snorm_of_ae_le_mul h p
case ha
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : snorm (fun x => ↑↑f x) p μ ≤ c • snorm (fun x => ↑↑g x) p μ
⊢ snorm (fun x => ↑↑f x) p μ ≠ ⊤

case hb
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : snorm (fun x => ↑↑f x) p μ ≤ c • snorm (fun x => ↑↑g x) p μ
⊢ c • snorm (fun x => ↑↑g x) p μ ≠ ⊤
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : snorm (fun x => ↑↑f x) p μ ≤ c • snorm (fun x => ↑↑g x) p μ
⊢ ENNReal.toNNReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toNNReal (snorm (↑↑g) p μ)
rwa [← ENNReal.toNNReal_le_toNNReal, ENNReal.smul_def, smul_eq_mul, ENNReal.toNNReal_mul,
  ENNReal.toNNReal_coe] at this
no goals
case ha
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : snorm (fun x => ↑↑f x) p μ ≤ c • snorm (fun x => ↑↑g x) p μ
⊢ snorm (fun x => ↑↑f x) p μ ≠ ⊤
exact (Lp.memℒp _).snorm_ne_top
no goals
case hb
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.418576
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ≥0
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : snorm (fun x => ↑↑f x) p μ ≤ c • snorm (fun x => ↑↑g x) p μ
⊢ c • snorm (fun x => ↑↑g x) p μ ≠ ⊤
exact ENNReal.mul_ne_top ENNReal.coe_ne_top (Lp.memℒp _).snorm_ne_top