α✝ : Type ?u.961798
E✝ : Type ?u.961801
F✝ : Type ?u.961804
G : Type ?u.961807
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ✝ ν : MeasureTheory.Measure α✝
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
g✝ : E✝ → F✝
c : ℝ≥0
α : Type u_1
E : Type u_2
F : Type u_3
K : ℝ≥0
inst✝² : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hg : LipschitzWith K g
g0 : g 0 = 0
hL : Memℒp f p
a : α
⊢ ‖g (f a)‖ ≤ ↑K * ‖f a‖
α✝ : Type ?u.961798
E✝ : Type ?u.961801
F✝ : Type ?u.961804
G : Type ?u.961807
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ✝ ν : MeasureTheory.Measure α✝
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
g✝ : E✝ → F✝
c : ℝ≥0
α : Type u_1
E : Type u_2
F : Type u_3
K : ℝ≥0
inst✝² : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hg : LipschitzWith K g
g0 : g 0 = 0
hL : Memℒp f p
⊢ ∀ (x : α), ‖g (f x)‖ ≤ ↑K * ‖f x‖
intro a
no goals
α✝ : Type ?u.961798
E✝ : Type ?u.961801
F✝ : Type ?u.961804
G : Type ?u.961807
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ✝ ν : MeasureTheory.Measure α✝
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
g✝ : E✝ → F✝
c : ℝ≥0
α : Type u_1
E : Type u_2
F : Type u_3
K : ℝ≥0
inst✝² : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hg : LipschitzWith K g
g0 : g 0 = 0
hL : Memℒp f p
a : α
⊢ ‖g (f a)‖ ≤ ↑K * ‖f a‖
simpa [g0] using hg.norm_sub_le (f a) 0