α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) ⊤ μ
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f p μ * snorm g ⊤ μ
rw [← snorm_norm f, ← snorm_norm g]
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => (fun a => ↑a) (‖f x‖₊ * ‖g x‖₊)) p μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) ⊤ μ
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) ⊤ μ
refine' (snorm_mono_ae_real h).trans _
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => ‖g x‖ * ‖f x‖) p μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) ⊤ μ
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => (fun a => ↑a) (‖f x‖₊ * ‖g x‖₊)) p μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) ⊤ μ
simp_rw [mul_comm ‖f _‖₊, val_eq_coe, NNReal.coe_mul, coe_nnnorm]
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => ‖g x‖ * ‖f x‖) p μ ≤ snorm (fun x => ‖g x‖) ⊤ μ * snorm (fun x => ‖f x‖) p μ
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => ‖g x‖ * ‖f x‖) p μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) ⊤ μ
rw [mul_comm]
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
x : α
x✝ : ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ ‖(fun x => ‖g x‖) x * ‖f x‖‖₊ ≤ ‖(fun x => ‖g x‖) x‖₊ * ‖‖f x‖‖₊
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => ‖g x‖ * ‖f x‖) p μ ≤ snorm (fun x => ‖g x‖) ⊤ μ * snorm (fun x => ‖f x‖) p μ
refine' snorm_le_snorm_top_mul_snorm p (fun x => ‖g x‖) hf.norm _ (h.mono fun x _ => _)
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
x : α
x✝ : ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ ‖‖g x‖‖₊ * ‖‖f x‖‖₊ ≤ ‖‖g x‖‖₊ * ‖‖f x‖‖₊
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
x : α
x✝ : ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ ‖(fun x => ‖g x‖) x * ‖f x‖‖₊ ≤ ‖(fun x => ‖g x‖) x‖₊ * ‖‖f x‖‖₊
simp_rw [nnnorm_mul]
no goals
α : Type u_1
E : Type u_2
F : Type u_4
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
x : α
x✝ : ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ ‖‖g x‖‖₊ * ‖‖f x‖‖₊ ≤ ‖‖g x‖‖₊ * ‖‖f x‖‖₊
rfl