Conditional Lipschitz and uniqueness bounds for gradients at infimal-convolution minimizers.

def V7.Stage5AboveTwoLowerS5A2Envelope.KernelCocoerciveOnUnit {d : ℕ} (p M : ℝ) (gradPhi : Point d → Point d) : Prop

The exact local kernel inequality needed by the primal envelope route. It is stated only on the unit ell_p ball, matching the frozen Hessian control and the already proved strict interiority of all minimizers.

Equations

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

theorem V7.Stage5AboveTwoLowerS5A2Envelope.minimizer_kernel_gradient_lipschitz {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi M : ℝ} (hp : 1 < p) (hchi : 0 < chi) (hM : 0 ≤ M) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hgradPhi : O3.IsCoordinateGradient kernel.phi kernel.gradPhi) (hcoco : KernelCocoerciveOnUnit p M kernel.gradPhi) {x y vx vy : Point d} (hvx : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x vx) (hvy : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell y vy) (hux : lpNorm p ((1 / chi) • vx) ≤ 1) (huy : lpNorm p ((1 / chi) • vy) ≤ 1) : lpNorm (conjugateExponent p) (kernel.gradPhi ((1 / chi) • vx) - kernel.gradPhi ((1 / chi) • vy)) ≤ M / chi * lpNorm p (x - y)

Exact minimizer-gradient Lipschitz estimate, conditional only on the local kernel cocoercivity wheel.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.minimizer_kernel_gradient_unique {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi M : ℝ} (hp : 1 < p) (hchi : 0 < chi) (hM : 0 ≤ M) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hgradPhi : O3.IsCoordinateGradient kernel.phi kernel.gradPhi) (hcoco : KernelCocoerciveOnUnit p M kernel.gradPhi) {x vx vy : Point d} (hvx : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x vx) (hvy : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x vy) (hux : lpNorm p ((1 / chi) • vx) ≤ 1) (huy : lpNorm p ((1 / chi) • vy) ≤ 1) : kernel.gradPhi ((1 / chi) • vx) = kernel.gradPhi ((1 / chi) • vy)

Any two minimizers at the same centre induce exactly the same kernel gradient.