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

Uniform exterior sphere condition

This file defines the uniform exterior sphere condition for a set U in EuclideanSpace ℝ (Fin d): there is a radius R > 0 such that every boundary point x₀ of U is touched by a closed ball of radius R whose interior misses closure U.

Main results

• ViscositySolns.uniformExteriorSphere_ball: Euclidean balls satisfy the condition, with radius equal to their own radius.
• ViscositySolns.UniformExteriorSphere.exists_radius_le: the radius can be taken as small as desired.
• ViscositySolns.uniformExteriorSphere_of_contDiff_levelSet: a bounded sublevel set {ρ < 0} of a C² function ρ whose gradient does not vanish on the boundary satisfies the condition.

Proof outline for level sets

On the compact boundary ‖∇ρ‖ ≥ c > 0, and fderiv ℝ ρ is Λ-Lipschitz on a closed ball containing the 1-neighbourhood of closure U. At a boundary point x₀ put y = x₀ + R • ν with ν = ∇ρ x₀ / ‖∇ρ x₀‖. If ‖x - y‖ < R then ‖∇ρ x₀‖ ‖x - x₀‖² < 2R ⟪∇ρ x₀, x - x₀⟫, while the first-order Taylor bound gives ρ x ≥ ⟪∇ρ x₀, x - x₀⟫ - Λ ‖x - x₀‖². For 2RΛ ≤ c this forces ρ x > 0, so x ∉ closure U.

def ViscositySolns.UniformExteriorSphere {d : ℕ} (U : Set (EuclideanSpace ℝ (Fin d))) : Prop

Uniform exterior sphere condition.

Equations

• ViscositySolns.UniformExteriorSphere U = ∃ R > 0, ∀ x₀ ∈ frontier U, ∃ (y : EuclideanSpace ℝ (Fin d)), dist x₀ y = R ∧ ∀ x ∈ closure U, R ≤ dist x y

theorem ViscositySolns.exists_exteriorSphere_of_le {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} {x₀ y : EuclideanSpace ℝ (Fin d)} {R R' : ℝ} (hR' : 0 < R') (hR'R : R' ≤ R) (hy : dist x₀ y = R) (hU : ∀ x ∈ U, R ≤ dist x y) : ∃ (y' : EuclideanSpace ℝ (Fin d)), dist x₀ y' = R' ∧ ∀ x ∈ U, R' ≤ dist x y'

An exterior sphere of radius R at x₀ can be replaced by a smaller one of radius R' ∈ (0, R] touching at the same point: shrink the centre towards x₀.

theorem ViscositySolns.UniformExteriorSphere.exists_radius_le {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : UniformExteriorSphere U) {R₀ : ℝ} (hR₀ : 0 < R₀) : ∃ R > 0, R ≤ R₀ ∧ ∀ x₀ ∈ frontier U, ∃ (y : EuclideanSpace ℝ (Fin d)), dist x₀ y = R ∧ ∀ x ∈ closure U, R ≤ dist x y

If the uniform exterior sphere condition holds, it holds with a radius no larger than any prescribed R₀ > 0.

theorem ViscositySolns.uniformExteriorSphere_ball {d : ℕ} (c : EuclideanSpace ℝ (Fin d)) {t : ℝ} (ht : 0 < t) : UniformExteriorSphere (Metric.ball c t)

A Euclidean ball satisfies the uniform exterior sphere condition with its own radius: at x₀ on the boundary, use the ball centred at the reflection x₀ + (x₀ - c) of the centre through x₀.

theorem ViscositySolns.exists_norm_fderiv_sub_le_of_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : E → ℝ} (hρ : ContDiff ℝ 2 ρ) {K : Set E} (hK : IsCompact K) (hKc : Convex ℝ K) : ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ w ∈ K, ∀ z ∈ K, ‖fderiv ℝ ρ w - fderiv ℝ ρ z‖ ≤ Λ * ‖w - z‖

A C² function has Lipschitz derivative on every convex compact set.

theorem ViscositySolns.le_of_norm_fderiv_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : E → ℝ} (hρ : Differentiable ℝ ρ) {x₀ x : E} {Λ : ℝ} (hΛ : ∀ w ∈ Metric.closedBall x₀ ‖x - x₀‖, ‖fderiv ℝ ρ w - fderiv ℝ ρ x₀‖ ≤ Λ * ‖x - x₀‖) : ρ x₀ + (fderiv ℝ ρ x₀) (x - x₀) - Λ * ‖x - x₀‖ ^ 2 ≤ ρ x

First-order Taylor lower bound: if fderiv ℝ ρ stays within Λ ‖x - x₀‖ of fderiv ℝ ρ x₀ on the closed ball closedBall x₀ ‖x - x₀‖, then ρ x ≥ ρ x₀ + fderiv ℝ ρ x₀ (x - x₀) - Λ ‖x - x₀‖².

theorem ViscositySolns.uniformExteriorSphere_of_contDiff_levelSet {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hUb : Bornology.IsBounded U) (hC2 : ∃ (ρ : EuclideanSpace ℝ (Fin d) → ℝ), ContDiff ℝ 2 ρ ∧ U = {x : EuclideanSpace ℝ (Fin d) | ρ x < 0} ∧ ∀ x ∈ frontier U, gradient ρ x ≠ 0) : UniformExteriorSphere U

A bounded sublevel set {ρ < 0} of a C² function whose gradient does not vanish on the boundary satisfies the uniform exterior sphere condition.