no goals
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ snorm (f - g) p μ = snorm (f + -g) p μ
rw [sub_eq_add_neg]
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
x : α
⊢ ‖‖f x + -g x‖‖ ≤ ‖f x‖ + ‖-g x‖
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ snorm (fun x => ‖f x + -g x‖) p μ ≤ snorm (fun x => ‖f x‖ + ‖-g x‖) p μ
refine' snorm_mono_real fun x => _
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
x : α
⊢ ‖f x + -g x‖ ≤ ‖f x‖ + ‖-g x‖
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
x : α
⊢ ‖‖f x + -g x‖‖ ≤ ‖f x‖ + ‖-g x‖
rw [norm_norm]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
x : α
⊢ ‖f x + -g x‖ ≤ ‖f x‖ + ‖-g x‖
exact norm_add_le _ _
no goals
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ snorm (fun x => ‖f x‖ + ‖-g x‖) p μ = snorm (fun x => ‖f x‖ + ‖g x‖) p μ
simp_rw [norm_neg]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.3041589
G : Type ?u.3041592
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ LpAddConst p * (snorm (fun x => ‖f x‖) p μ + snorm (fun x => ‖g x‖) p μ) = LpAddConst p * (snorm f p μ + snorm g p μ)
rw [← snorm_norm f, ← snorm_norm g]