The normalized completion is a convex objective with the stated coordinate gradient.

noncomputable def V7.Stage5AboveTwoLowerS5F.unitDelta (p : ℝ) (T : ℕ) : ℝ

The normalized separation scale T ^ (-1 / p).

Equations

• V7.Stage5AboveTwoLowerS5F.unitDelta p T = ↑T ^ (-1 / p)

noncomputable def V7.Stage5AboveTwoLowerS5F.unitDeltaStep (p : ℝ) (T : ℕ) : ℝ

The affine-piece offset used in the normalized resisting construction.

Equations

• V7.Stage5AboveTwoLowerS5F.unitDeltaStep p T = V7.Stage5AboveTwoLowerS5F.unitDelta p T / (2 * ↑T)

noncomputable def V7.Stage5AboveTwoLowerS5F.unitChi (p : ℝ) (T : ℕ) : ℝ

The smoothing scale, equal to half the normalized affine-piece offset.

Equations

• V7.Stage5AboveTwoLowerS5F.unitChi p T = V7.Stage5AboveTwoLowerS5F.unitDeltaStep p T / 2

noncomputable def V7.Stage5AboveTwoLowerS5F.unitParameters (p : ℝ) (d T : ℕ) (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) : PrefixParameters p d T

The explicit kernel and scales initializing the normalized resisting construction.

Equations

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

theorem V7.Stage5AboveTwoLowerS5F.unitDelta_pos {p : ℝ} {T : ℕ} (hT : 1 ≤ T) : 0 < unitDelta p T

theorem V7.Stage5AboveTwoLowerS5F.unitDeltaStep_pos {p : ℝ} {T : ℕ} (hT : 1 ≤ T) : 0 < unitDeltaStep p T

theorem V7.Stage5AboveTwoLowerS5F.unitChi_pos {p : ℝ} {T : ℕ} (hT : 1 ≤ T) : 0 < unitChi p T

theorem V7.Stage5AboveTwoLowerS5F.unitBeta_pos {p : ℝ} {d T : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (hT : 1 ≤ T) : 0 < unitChi p T / Stage5AboveTwoLowerS5A2Envelope.repairMpd p d

noncomputable def V7.Stage5AboveTwoLowerS5F.unitCompletionData (p : ℝ) (d T : ℕ) (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) : LowerCompletionData p d T

The complete normalized resisting data for a deterministic algorithm.

Equations

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

theorem V7.Stage5AboveTwoLowerS5F.unitCompletionData_assumptions {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hp : 2 < p) (hd : 2 ≤ d) (hT : 1 ≤ T) (hTd : T ≤ d) : LowerCompletionAssumptions (unitCompletionData p d T algorithm hT hTd)

theorem V7.Stage5AboveTwoLowerS5F.convexObjective_of_global_support {d : ℕ} (f : Point d → ℝ) (g : Point d → Point d) (hsupport : ∀ (x y : Point d), f x + pairing (g x) (y - x) ≤ f y) : O3.IsConvexObjective f

A global supporting field implies convexity; this local wheel avoids any packaged convex-envelope dependency.

theorem V7.Stage5AboveTwoLowerS5F.coordinateGradient_const_mul {d : ℕ} (f : Point d → ℝ) (g : Point d → Point d) (c : ℝ) (hgrad : O3.IsCoordinateGradient f g) : O3.IsCoordinateGradient (fun (x : O3.Vec d) => c * f x) fun (x : O3.Vec d) => c • g x

noncomputable def V7.Stage5AboveTwoLowerS5F.unitObjectiveData (p : ℝ) (d T : ℕ) (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) : LowerObjectiveData p d T

The normalized completed resisting data viewed as objective data.

Equations

• V7.Stage5AboveTwoLowerS5F.unitObjectiveData p d T algorithm hT hTd = { toLowerCompletionData := V7.Stage5AboveTwoLowerS5F.unitCompletionData p d T algorithm hT hTd }

theorem V7.Stage5AboveTwoLowerS5F.unitObjectiveData_assumptions {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hp : 2 < p) (hd : 2 ≤ d) (hT : 1 ≤ T) (hTd : T ≤ d) : LowerObjectiveAssumptions (unitObjectiveData p d T algorithm hT hTd)