case inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖

case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ ‖f‖ ≤ c * ‖g‖
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
⊢ ‖f‖ ≤ c * ‖g‖
cases' le_or_lt 0 c with hc hc
case inl.intro
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑c * ‖↑↑g x‖
⊢ ‖f‖ ≤ ↑c * ‖g‖
case inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖
lift c to ℝ≥0 using hc
no goals
case inl.intro
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑c * ‖↑↑g x‖
⊢ ‖f‖ ≤ ↑c * ‖g‖
exact NNReal.coe_le_coe.mpr (nnnorm_le_mul_nnnorm_of_ae_le_mul h)
case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ ENNReal.toReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toReal (snorm (↑↑g) p μ)
case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ ‖f‖ ≤ c * ‖g‖
simp only [norm_def]
case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
this : snorm (fun x => ↑↑f x) p μ = 0 ∧ snorm (fun x => ↑↑g x) p μ = 0
⊢ ENNReal.toReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toReal (snorm (↑↑g) p μ)
case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ ENNReal.toReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toReal (snorm (↑↑g) p μ)
have := snorm_eq_zero_and_zero_of_ae_le_mul_neg h hc p
no goals
case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.421336
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : ℝ
f : { x // x ∈ Lp E p }
g : { x // x ∈ Lp F p }
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
this : snorm (fun x => ↑↑f x) p μ = 0 ∧ snorm (fun x => ↑↑g x) p μ = 0
⊢ ENNReal.toReal (snorm (↑↑f) p μ) ≤ c * ENNReal.toReal (snorm (↑↑g) p μ)
simp [this]