case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑(compLp hg g0 f - compLp hg g0 f') x‖ ≤ ↑c * ‖↑↑(f - f') x‖
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
⊢ ‖compLp hg g0 f - compLp hg g0 f'‖ ≤ ↑c * ‖f - f'‖
apply Lp.norm_le_mul_norm_of_ae_le_mul
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
a : α
ha1 : ↑↑(compLp hg g0 f) a = (g ∘ ↑↑f) a
ha2 : ↑↑(compLp hg g0 f') a = (g ∘ ↑↑f') a
ha3 : ↑↑(compLp hg g0 f - compLp hg g0 f') a = (↑↑(compLp hg g0 f) - ↑↑(compLp hg g0 f')) a
ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a
⊢ ‖↑↑(compLp hg g0 f - compLp hg g0 f') a‖ ≤ ↑c * ‖↑↑(f - f') a‖
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑(compLp hg g0 f - compLp hg g0 f') x‖ ≤ ↑c * ‖↑↑(f - f') x‖
filter_upwards [hg.coeFn_compLp g0 f, hg.coeFn_compLp g0 f',
  Lp.coeFn_sub (hg.compLp g0 f) (hg.compLp g0 f'), Lp.coeFn_sub f f'] with a ha1 ha2 ha3 ha4
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
a : α
ha1 : ↑↑(compLp hg g0 f) a = (g ∘ ↑↑f) a
ha2 : ↑↑(compLp hg g0 f') a = (g ∘ ↑↑f') a
ha3 : ↑↑(compLp hg g0 f - compLp hg g0 f') a = (↑↑(compLp hg g0 f) - ↑↑(compLp hg g0 f')) a
ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a
⊢ dist (g (↑↑f a)) (g (↑↑f' a)) ≤ ↑c * dist (↑↑f a) (↑↑f' a)
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
a : α
ha1 : ↑↑(compLp hg g0 f) a = (g ∘ ↑↑f) a
ha2 : ↑↑(compLp hg g0 f') a = (g ∘ ↑↑f') a
ha3 : ↑↑(compLp hg g0 f - compLp hg g0 f') a = (↑↑(compLp hg g0 f) - ↑↑(compLp hg g0 f')) a
ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a
⊢ ‖↑↑(compLp hg g0 f - compLp hg g0 f') a‖ ≤ ↑c * ‖↑↑(f - f') a‖
simp only [ha1, ha2, ha3, ha4, ← dist_eq_norm, Pi.sub_apply, Function.comp_apply]
no goals
case h
α : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.2355804
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : { x // x ∈ Lp E p }
a : α
ha1 : ↑↑(compLp hg g0 f) a = (g ∘ ↑↑f) a
ha2 : ↑↑(compLp hg g0 f') a = (g ∘ ↑↑f') a
ha3 : ↑↑(compLp hg g0 f - compLp hg g0 f') a = (↑↑(compLp hg g0 f) - ↑↑(compLp hg g0 f')) a
ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a
⊢ dist (g (↑↑f a)) (g (↑↑f' a)) ≤ ↑c * dist (↑↑f a) (↑↑f' a)
exact hg.dist_le_mul (f a) (f' a)