Selection of minimizing displacements and differentiation of the resulting envelope.

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.selectedDisplacement {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x : Point d) : Point d

A total classical selector. Under the concrete Stage-5 hypotheses its selected displacement is a minimizer with the already proved uniform margin.

Equations

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

theorem V7.Stage5AboveTwoLowerS5A2Envelope.selectedDisplacement_spec {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x : Point d) (hex : ∃ (v : Point d), Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v ∧ lpNorm p v ≤ chi - chi / 4) : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x (selectedDisplacement kernel chi ell x) ∧ lpNorm p (selectedDisplacement kernel chi ell x) ≤ chi - chi / 4

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.selectedEnvelopeGradient {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x : Point d) : Point d

The envelope gradient obtained from a selected minimizing displacement.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.selectedEnvelopeGradient kernel chi ell x = -kernel.gradPhi ((1 / chi) • V7.Stage5AboveTwoLowerS5A2Envelope.selectedDisplacement kernel chi ell x)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.hasFDerivAt_of_global_support_and_lp_lipschitz {d : ℕ} {p L : ℝ} (hp : 1 < p) (hL : 0 ≤ L) (f : Point d → ℝ) (g : Point d → Point d) (hsupport : ∀ (x : Point d) (y : O3.Point d), f x + O3.pairing (g x) (y - x) ≤ f y) (hlip : ∀ (x y : Point d), lpNorm (conjugateExponent p) (g x - g y) ≤ L * lpNorm p (x - y)) (x : Point d) : HasFDerivAt f (Stage5AboveTwoLower.S5ARepair.pairingCLM (g x)) x

A globally supporting, locally Lipschitz vector field is the genuine Fréchet derivative of its value function. This is the specialized primal Danskin replacement needed by the frozen construction.