Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Compact neighborhoods for the maximum-principle proof

This file contains product-neighborhood localization lemmas used in the finite-dimensional maximum-principle proof.

theorem ViscositySolns.exists_compact_translated_product_subset_of_mem_nhdsWithin_prod {n : ℕ} {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {P : Set (DoubledPoint n)} {x0 y0 : Point n} (hx0C : x0 ∈ C) (hy0D : y0 ∈ D) (hP : P ∈ nhdsWithin (x0, y0) (C ×ˢ D)) : ∃ (K : Set (Point n)) (L : Set (Point n)), K.Nonempty ∧ L.Nonempty ∧ IsCompact K ∧ IsCompact L ∧ 0 ∈ K ∧ 0 ∈ L ∧ (fun (x : Point n) => x0 + x) '' K ∈ nhdsWithin x0 C ∧ (fun (y : Point n) => y0 + y) '' L ∈ nhdsWithin y0 D ∧ (fun (x : Point n) => x0 + x) '' K ⊆ C ∧ (fun (y : Point n) => y0 + y) '' L ⊆ D ∧ (∀ x ∈ K, ∀ y ∈ L, (x0 + x, y0 + y) ∈ P) ∧ {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} ⊆ P

A relative neighborhood of a point in C × D contains a translated compact product neighborhood.

In quantified mathematical form, assume x0 ∈ C, y0 ∈ D, the relative topologies on C and D are locally compact, and P ∈ nhdsWithin (x0, y0) (C × D). Then there exist compact nonempty sets K, L ⊆ R^n, both containing 0, such that

• x0 + K ⊆ C;
• y0 + L ⊆ D;
• for every x ∈ K and y ∈ L, (x0 + x, y0 + y) ∈ P.

The sets are obtained by choosing compact relative closed-ball neighborhoods of x0 and y0 inside the product neighborhood and then translating the base point to the origin.

theorem ViscositySolns.exists_compact_translated_product_isMaxOn_of_hasDoubledLocalMaximumOn {n : ℕ} {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {x0 y0 : Point n} (hlocal : HasDoubledLocalMaximumOn C D u v φ x0 y0) : ∃ (K : Set (Point n)) (L : Set (Point n)), K.Nonempty ∧ L.Nonempty ∧ IsCompact K ∧ IsCompact L ∧ 0 ∈ K ∧ 0 ∈ L ∧ (fun (x : Point n) => x0 + x) '' K ∈ nhdsWithin x0 C ∧ (fun (y : Point n) => y0 + y) '' L ∈ nhdsWithin y0 D ∧ (fun (x : Point n) => x0 + x) '' K ⊆ C ∧ (fun (y : Point n) => y0 + y) '' L ⊆ D ∧ IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - φ q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)

A doubled local maximum supplies compact translated neighborhoods on which the same inequality is a genuine maximum inequality.

In quantified mathematical form, assume x0 ∈ C, y0 ∈ D, and (x0, y0) is a local maximum point of

(x, y) ↦ u(x) - v(y) - φ(x, y)

relative to C × D. If the relative topologies on C and D are locally compact, then there exist compact nonempty sets K, L ⊆ R^n, both containing 0, such that x0 + K ⊆ C, y0 + L ⊆ D, and (x0, y0) is a maximum point of the same doubled objective on the translated product set

{(x, y) | x - x0 ∈ K and y - y0 ∈ L}.