Theorem: LocallyLipschitz.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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz (f + g)
Tactic:
intro x
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t

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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Tactic:
rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩
State after:
case intro.intro.intro
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t

State before:
case intro.intro.intro
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Tactic:
rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩
State after:
case intro.intro.intro.intro.intro.intro
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t

State before:
case intro.intro.intro.intro.intro.intro
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Tactic:
use Kf + Kg, t₁ ∩ t₂
State after:
case h
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)

State before:
case h
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Tactic:
have hf' : LipschitzOnWith Kf f (t₁ ∩ t₂) := hfL.mono (Set.inter_subset_left t₁ t₂)
State after:
case h
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)

State before:
case h
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Tactic:
have hg' : LipschitzOnWith Kg g (t₁ ∩ t₂) := hgL.mono (Set.inter_subset_right t₁ t₂)
State after:
case h
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
hg' : LipschitzOnWith Kg g (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)

State before:
case h
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
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
hg' : LipschitzOnWith Kg g (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Tactic:
exact ⟨Filter.inter_mem h₁t h₂t, hf'.sum hg'⟩
State after:
no goals