Theorem: LipschitzOnWith.sum (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf + Kg) (f + g) s
Tactic:
intro y hy z hz
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z
Tactic:
have translation: ∀ w w' w'' : Y, edist (w + w'') (w' + w'') = edist w w' := by
  intro w w' w''
  simp only [edist_add_right]
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z
Tactic:
simp only [Pi.add_apply, ENNReal.coe_add]
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g z) ≤ (↑Kf + ↑Kg) * edist y z

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g z) ≤ (↑Kf + ↑Kg) * edist y z
Tactic:
calc edist (f y + g y) (f z + g z)
  _ ≤ edist (f y + g y) (g y + f z) + edist (g y + f z) (f z + g z) := by apply edist_triangle
  _ = edist (f y + g y) (f z + g y) + edist (g y + f z) (g z + f z) := by
      simp only [add_comm, edist_add_right, edist_add_left]
  _ ≤ edist (f y) (f z) + edist (g y) (g z) := by rw [translation, translation]
  _ ≤ Kf * edist y z + Kg * edist y z := add_le_add (hf hy hz) (hg hy hz)
  _ = (Kf + Kg) * edist y z := by ring
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
⊢ ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
Tactic:
intro w w' w''
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
w w' w'' : Y
⊢ edist (w + w'') (w' + w'') = edist w w'

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
w w' w'' : Y
⊢ edist (w + w'') (w' + w'') = edist w w'
Tactic:
simp only [edist_add_right]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g z) ≤ edist (f y + g y) (g y + f z) + edist (g y + f z) (f z + g z)
Tactic:
apply edist_triangle
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (g y + f z) + edist (g y + f z) (f z + g z) =
    edist (f y + g y) (f z + g y) + edist (g y + f z) (g z + f z)
Tactic:
simp only [add_comm, edist_add_right, edist_add_left]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g y) + edist (g y + f z) (g z + f z) ≤ edist (f y) (f z) + edist (g y) (g z)
Tactic:
rw [translation, translation]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ ↑Kf * edist y z + ↑Kg * edist y z = (↑Kf + ↑Kg) * edist y z
Tactic:
ring
State after:
no goals