English
The sum of two lower semicontinuous functions is lower semicontinuous (under a mild regularity on addition).
Русский
Сумма двух нижних полупрерывных функций — тоже нижняя полупрерывность (при нормальных условиях на сложение).
LaTeX
$$$\\text{LowerSemicontinuous } f \\land \\text{LowerSemicontinuous } g \\Rightarrow \\text{LowerSemicontinuous } (f+g)$$$
Lean4
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`. -/
theorem add' {f g : α → γ} (hf : LowerSemicontinuousWithinAt f s x) (hg : LowerSemicontinuousWithinAt g s x)
(hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
LowerSemicontinuousWithinAt (fun z => f z + g z) s x :=
by
intro y hy
obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
∃ u v : Set γ, IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ {p : γ × γ | y < p.fst + p.snd} :=
mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))
by_cases hx₁ : ∃ l, l < f x
· obtain ⟨z₁, z₁lt, h₁⟩ : ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u := exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁
by_cases hx₂ : ∃ l, l < g x
· obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v := exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z
have A1 : min (f z) (f x) ∈ u := by
by_cases H : f z ≤ f x
· simpa [H] using h₁ ⟨h₁z, H⟩
· simpa [le_of_not_ge H]
have A2 : min (g z) (g x) ∈ v := by
by_cases H : g z ≤ g x
· simpa [H] using h₂ ⟨h₂z, H⟩
· simpa [le_of_not_ge H]
have : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩
calc
y < min (f z) (f x) + min (g z) (g x) := h this
_ ≤ f z + g z := add_le_add (min_le_left _ _) (min_le_left _ _)
· simp only [not_exists, not_lt] at hx₂
filter_upwards [hf z₁ z₁lt] with z h₁z
have A1 : min (f z) (f x) ∈ u := by
by_cases H : f z ≤ f x
· simpa [H] using h₁ ⟨h₁z, H⟩
· simpa [le_of_not_ge H]
have : (min (f z) (f x), g x) ∈ u ×ˢ v := ⟨A1, xv⟩
calc
y < min (f z) (f x) + g x := h this
_ ≤ f z + g z := add_le_add (min_le_left _ _) (hx₂ (g z))
· simp only [not_exists, not_lt] at hx₁
by_cases hx₂ : ∃ l, l < g x
· obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v := exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
filter_upwards [hg z₂ z₂lt] with z h₂z
have A2 : min (g z) (g x) ∈ v := by
by_cases H : g z ≤ g x
· simpa [H] using h₂ ⟨h₂z, H⟩
· simpa [le_of_not_ge H] using h₂ ⟨z₂lt, le_rfl⟩
have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
calc
y < f x + min (g z) (g x) := h this
_ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)
· simp only [not_exists, not_lt] at hx₁ hx₂
apply Filter.Eventually.of_forall
intro z
have : (f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩
calc
y < f x + g x := h this
_ ≤ f z + g z := add_le_add (hx₁ (f z)) (hx₂ (g z))
