Locality of the infimal smoothing value and its exact value-gradient observations.
theorem
V7.Stage5AboveTwoLowerResume.localSmoothingValue_eventually_eq_lowerKernelPhi
{p : ℝ}
{d : ℕ}
(kernel : SmoothingKernelData p d)
{r theta chi : ℝ}
(hr : 2 < r)
(hrp : r ≤ p)
(htheta : 1 < theta)
(hthetaUpper : theta < 5 / 4)
(htr : 2 * theta < r)
(hchi : 0 < chi)
(hkernelPhi : kernel.phi = lowerKernelPhi r theta)
(ell₁ ell₂ : Point d → ℝ)
(hlip₁ : IsOneLipschitz p ell₁)
(hlip₂ : IsOneLipschitz p ell₂)
(x : Point d)
(heq : ∀ (u : Point d), lpNorm p u ≤ chi → ell₁ (x + u) = ell₂ (x + u))
:
Uniform outer-quarter minimizer control supplies exactly the nearby-centre stability needed by the existing infimal-locality bridge.
theorem
V7.Stage5AboveTwoLowerResume.neighborhoodStability_lowerKernelPhi
{p : ℝ}
{d : ℕ}
(kernel : SmoothingKernelData p d)
{r theta : ℝ}
(hr : 2 < r)
(hrp : r ≤ p)
(htheta : 1 < theta)
(hthetaUpper : theta < 5 / 4)
(htr : 2 * theta < r)
(hkernelPhi : kernel.phi = lowerKernelPhi r theta)
(hvalue :
∀ (chi : ℝ),
0 < chi →
∀ (ell : Point d → ℝ),
O3.IsConvexObjective ell →
IsOneLipschitz p ell →
∀ (x : O3.Vec d), (kernel.smooth chi ell).value x = localSmoothingValue kernel chi ell x)
:
The concrete kernel and the frozen value-realization clause imply the full neighbourhood-stability interface.
theorem
V7.Stage5AboveTwoLowerResume.exactPairLocality_lowerKernelPhi
{p : ℝ}
{d : ℕ}
(kernel : SmoothingKernelData p d)
{r theta : ℝ}
(hr : 2 < r)
(hrp : r ≤ p)
(htheta : 1 < theta)
(hthetaUpper : theta < 5 / 4)
(htr : 2 * theta < r)
(hkernelPhi : kernel.phi = lowerKernelPhi r theta)
(hvalue :
∀ (chi : ℝ),
0 < chi →
∀ (ell : Point d → ℝ),
O3.IsConvexObjective ell →
IsOneLipschitz p ell →
∀ (x : O3.Vec d), (kernel.smooth chi ell).value x = localSmoothingValue kernel chi ell x)
(hgradient : Stage5AboveTwoLower.SmoothingCoordinateGradientCore kernel)
(chi : ℝ)
:
0 < chi →
∀ (ell₁ ell₂ : Point d → ℝ),
O3.IsConvexObjective ell₁ →
IsOneLipschitz p ell₁ →
O3.IsConvexObjective ell₂ →
IsOneLipschitz p ell₂ →
∀ (x : O3.Vec d),
(∀ (v : Point d), lpNorm p v ≤ chi → ell₁ (x + v) = ell₂ (x + v)) →
O3.PairOracle.observe (kernel.smooth chi ell₁) x = O3.PairOracle.observe (kernel.smooth chi ell₂) x
The existing differential bridge upgrades the neighbourhood result to the exact value-gradient observation required by the frozen carrier.