Stable interior minimizing displacements imply locality of the infimal-convolution value.

theorem V7.Stage5AboveTwoLower.S5ARepair.eventually_lpNorm_sub_lt {d : ℕ} {p eta : ℝ} (hp : 1 ≤ p) (heta : 0 < eta) (x : Point d) : ∀ᶠ (y : Point d) in nhds x, lpNorm p (y - x) < eta

noncomputable def V7.Stage5AboveTwoLower.S5ARepair.smoothingCost {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x v : Point d) : ℝ

The objective value plus the rescaled kernel penalty at a displacement.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi ell x v = ell (x + v) + chi * kernel.phi ((1 / chi) • v)

def V7.Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x v : Point d) : Prop

The displacement globally minimizes the infimal-convolution cost.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage5AboveTwoLower.S5ARepair.localSmoothingValue_eq_of_minimizer {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x v : Point d) (hv : IsInfimalMinimizer kernel chi ell x v) : localSmoothingValue kernel chi ell x = smoothingCost kernel chi ell x v

theorem V7.Stage5AboveTwoLower.S5ARepair.localSmoothingValue_eventually_eq_of_stable_minimizers {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi : ℝ} {ell₁ ell₂ : Point d → ℝ} {x : Point d} (heq : ∀ (u : Point d), lpNorm p u ≤ chi → ell₁ (x + u) = ell₂ (x + u)) (hstable : ∀ᶠ (y : Point d) in nhds x, ∃ (v₁ : Point d) (v₂ : Point d), IsInfimalMinimizer kernel chi ell₁ y v₁ ∧ IsInfimalMinimizer kernel chi ell₂ y v₂ ∧ lpNorm p (y + v₁ - x) ≤ chi ∧ lpNorm p (y + v₂ - x) ≤ chi) : localSmoothingValue kernel chi ell₁ =ᶠ[nhds x] localSmoothingValue kernel chi ell₂

The exact logical core of value locality. Once minimizers at nearby centres stay inside the original closed smoothing ball, equality of the two objectives on that ball forces equality of the two infimal values.

theorem V7.Stage5AboveTwoLower.S5ARepair.stable_minimizers_of_uniform_interior_margin {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi eta : ℝ} {ell₁ ell₂ : Point d → ℝ} {x : Point d} (hp : 1 ≤ p) (_heta : 0 < eta) (hnear : ∀ᶠ (y : Point d) in nhds x, lpNorm p (y - x) < eta) (hmargin : ∀ᶠ (y : Point d) in nhds x, ∃ (v₁ : Point d) (v₂ : Point d), IsInfimalMinimizer kernel chi ell₁ y v₁ ∧ IsInfimalMinimizer kernel chi ell₂ y v₂ ∧ lpNorm p v₁ ≤ chi - eta ∧ lpNorm p v₂ ≤ chi - eta) : ∀ᶠ (y : Point d) in nhds x, ∃ (v₁ : Point d) (v₂ : Point d), IsInfimalMinimizer kernel chi ell₁ y v₁ ∧ IsInfimalMinimizer kernel chi ell₂ y v₂ ∧ lpNorm p (y + v₁ - x) ≤ chi ∧ lpNorm p (y + v₂ - x) ≤ chi

A uniform interior margin is sufficient for the nearby-centre stability hypothesis above. This isolates the remaining compactness task: produce one positive eta that works for every minimizer in a neighbourhood.