Assembly of the selected envelope oracle and its coordinate-gradient and smoothness proofs.

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.repairMpd (p : ℝ) (d : ℕ) : ℝ

The explicit curvature bound for the constructed smoothing kernel.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.repairMpd p d = if p ≤ 3 * Real.log ↑d then 5 * p else 15 * Real.exp (2 / 3) * Real.log ↑d

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.dormantOracle (d : ℕ) : PairOracle d

The constant zero oracle used in the preliminary kernel data.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.dormantOracle d = { value := fun (x : O3.Vec d) => 0, gradient := fun (x : O3.Vec d) => 0 }

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.repairKernelBase (p : ℝ) (d : ℕ) : SmoothingKernelData p d

Nonrecursive concrete kernel data used to formulate and select minimizers. Its dormant smooth field is never used in the infimal cost.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.repairSelectedOracle (p : ℝ) (d : ℕ) (chi : ℝ) (ell : Point d → ℝ) : PairOracle d

The infimal smoothing value paired with the selected envelope gradient.

Equations

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

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel (p : ℝ) (d : ℕ) : SmoothingKernelData p d

Final kernel data: its smooth oracle is the literal infimal value paired with the selected primal-envelope gradient.

Equations

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

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairMpd_nonneg {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 0 ≤ repairMpd p d

theorem V7.Stage5AboveTwoLowerS5A2Envelope.selectedDisplacement_concrete_spec {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hlip : IsOneLipschitz p ell) (x : Point d) : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer (repairKernelBase p d) chi ell x (selectedDisplacement (repairKernelBase p d) chi ell x) ∧ lpNorm p (selectedDisplacement (repairKernelBase p d) chi ell x) ≤ chi - chi / 4

theorem V7.Stage5AboveTwoLowerS5A2Envelope.selectedDisplacement_scaled_unit {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hlip : IsOneLipschitz p ell) (x : Point d) : lpNorm p ((1 / chi) • selectedDisplacement (repairKernelBase p d) chi ell x) ≤ 1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairSelectedGradient_support {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hlip : IsOneLipschitz p ell) (x y : Point d) : localSmoothingValue (repairKernelBase p d) chi ell x + O3.pairing (selectedEnvelopeGradient (repairKernelBase p d) chi ell x) (y - x) ≤ localSmoothingValue (repairKernelBase p d) chi ell y

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairSelectedGradient_lipschitz {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hlip : IsOneLipschitz p ell) (x y : Point d) : lpNorm (conjugateExponent p) (selectedEnvelopeGradient (repairKernelBase p d) chi ell x - selectedEnvelopeGradient (repairKernelBase p d) chi ell y) ≤ repairMpd p d / chi * lpNorm p (x - y)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.hasFDerivAt_repairSelectedValue {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hlip : IsOneLipschitz p ell) (x : Point d) : HasFDerivAt (repairSelectedOracle p d chi ell).value (Stage5AboveTwoLower.S5ARepair.pairingCLM ((repairSelectedOracle p d chi ell).gradient x)) x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairSelectedOracle_coordinateGradient {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hlip : IsOneLipschitz p ell) : O3.IsCoordinateGradient (repairSelectedOracle p d chi ell).value (repairSelectedOracle p d chi ell).gradient

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairSelectedOracle_smooth {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hlip : IsOneLipschitz p ell) : IsLpSmooth p (repairMpd p d / chi) (repairSelectedOracle p d chi ell)