Stage 4: exact weight algebra, barycentric identity, and radius bridge

This module isolates the source-exact algebraic parts of the accepted estimate-sequence proof. In particular, it keeps the exceptional first weight separate from the stationary recurrence and proves the radius of the regularized minimizer from its minimizing property and the actual sInf definition of the distance to the minimizer set.

noncomputable def O3.belowWeightIncrement (M tau : ℝ) (k : ℕ) : ℝ

The source increment a_(k+1) = A_(k+1) - A_k, including the exceptional first step.

Equations

• O3.belowWeightIncrement M tau k = O3.belowWeight M tau (k + 1) - O3.belowWeight M tau k

@[simp]

theorem O3.belowWeightIncrement_zero (M tau : ℝ) : belowWeightIncrement M tau 0 = 1 / M

theorem O3.belowWeight_add_increment (M tau : ℝ) (k : ℕ) : belowWeight M tau k + belowWeightIncrement M tau k = belowWeight M tau (k + 1)

With the source increment, A_+ = A_k + a_(k+1) is definitionally the next weight.

theorem O3.belowWeightIncrement_eq_tau_mul {M tau : ℝ} (htau : tau ≠ 1) {k : ℕ} (hk : 1 ≤ k) : belowWeightIncrement M tau k = tau * belowWeight M tau (k + 1)

For the stationary part of the recurrence, the source increment is exactly tau * A_(k+1).

theorem O3.belowWeight_eq_one_sub_tau_mul_succ {M tau : ℝ} (htau : tau ≠ 1) {k : ℕ} (hk : 1 ≤ k) : belowWeight M tau k = (1 - tau) * belowWeight M tau (k + 1)

Equivalent multiplicative form of the later weight recurrence.

theorem O3.belowFirstCoefficient {M tau : ℝ} (hM : M ≠ 0) : M * belowWeightIncrement M tau 0 ^ 2 / belowWeight M tau 1 = 1

The first-step coefficient is exactly one. This theorem deliberately does not route through the later stationary recurrence.

theorem O3.belowFirstCoefficient_eq_betaZero {M tau lambda sigma : ℝ} (hM : M ≠ 0) : M * belowWeightIncrement M tau 0 ^ 2 / belowWeight M tau 1 = 1 + lambda * sigma * belowWeight M tau 0

First-step equality with the source strong-convexity modulus beta_0 = 1 + lambda * sigma * A_0.

theorem O3.belowLaterCoefficient {M lambda sigma : ℝ} (hM : 0 < M) (hlambda : 0 < lambda) (hsigma : 0 < sigma) {k : ℕ} (hk : 1 ≤ k) : M * belowWeightIncrement M (belowTau M lambda sigma) k ^ 2 / belowWeight M (belowTau M lambda sigma) (k + 1) = lambda * sigma * belowWeight M (belowTau M lambda sigma) k

Exact later-step coefficient cancellation from the source tau equation.

theorem O3.belowLaterCoefficient_le_beta {M lambda sigma : ℝ} (hM : 0 < M) (hlambda : 0 < lambda) (hsigma : 0 < sigma) {k : ℕ} (hk : 1 ≤ k) : M * belowWeightIncrement M (belowTau M lambda sigma) k ^ 2 / belowWeight M (belowTau M lambda sigma) (k + 1) ≤ 1 + lambda * sigma * belowWeight M (belowTau M lambda sigma) k

Hence the later potential coefficient is nonpositive against beta_k = 1 + lambda * sigma * A_k.

noncomputable def O3.belowBarycenter {d : ℕ} (A a : ℝ) (x v : Point d) : Point d

Scalar-weighted barycenter used for both y_k and x_(k+1)^a.

Equations

• O3.belowBarycenter A a x v = (A + a)⁻¹ • (A • x + a • v)

theorem O3.belowBarycenter_sub {d : ℕ} {A a : ℝ} (hAa : A + a ≠ 0) (x v vnext : Point d) : belowBarycenter A a x vnext - belowBarycenter A a x v = (a / (A + a)) • (vnext - v)

The exact vector identity used in the one-step potential estimate.

noncomputable def O3.belowPhi {d : ℕ} (p lambda : ℝ) (f : Point d → ℝ) (x0 x : Point d) : ℝ

The exact composite objective Phi = f + lambda * psi_x0.

Equations

• O3.belowPhi p lambda f x0 x = f x + lambda * O3.quadraticRegularizer p x0 x

theorem O3.belowRegularizedMinimizer_radius {d : ℕ} {p lambda : ℝ} (hlambda : 0 < lambda) {f : Point d → ℝ} {x0 xlambda : Point d} (hmin_nonempty : (MinimizerSet f).Nonempty) (hxlambda : ∀ (z : Point d), belowPhi p lambda f x0 xlambda ≤ belowPhi p lambda f x0 z) : lpNorm p (xlambda - x0) ≤ minimizerDistance p f x0

A genuine minimizer of the regularized objective lies no farther from the center than the sInf distance to the original minimizer set. This avoids assuming that the sInf itself is attained.

theorem O3.minimizerDistance_nonneg_of_nonempty {d : ℕ} {p : ℝ} {f : Point d → ℝ} {x0 : Point d} (hmin_nonempty : (MinimizerSet f).Nonempty) : 0 ≤ minimizerDistance p f x0

The source distance to a nonempty minimizer set is nonnegative.

theorem O3.belowRegularizer_le_radius_budget {d : ℕ} {p sigma D R : ℝ} (hsigma : 0 < sigma) (hR : 0 ≤ R) (hDR : R ≤ D) {x0 x : Point d} (hxR : lpNorm p (x - x0) ≤ R) : 1 / sigma * quadraticRegularizer p x0 x ≤ D ^ 2 / (2 * sigma)

Radius comparison gives the exact regularizer budget appearing in the final source gap bound.

theorem O3.belowRegularizedMinimizer_budget {d : ℕ} {p lambda sigma D : ℝ} (hlambda : 0 < lambda) (hsigma : 0 < sigma) {f : Point d → ℝ} {x0 xlambda : Point d} (hmin_nonempty : (MinimizerSet f).Nonempty) (hxlambda : ∀ (z : Point d), belowPhi p lambda f x0 xlambda ≤ belowPhi p lambda f x0 z) (hDR : minimizerDistance p f x0 ≤ D) : 1 / sigma * quadraticRegularizer p x0 xlambda ≤ D ^ 2 / (2 * sigma)

Combined version of the source radius argument and regularizer budget, still using the actual regularized minimizer property rather than a supplied radius certificate.

theorem O3.belowPotential_to_gap {A sigma D phiXa phiXlambda psiStar h : ℝ} (hA : 0 < A) (hsigma : 0 < sigma) (hinvariant : A * phiXa ≤ psiStar) (hevaluation : psiStar ≤ h + A * phiXlambda) (hh : h ≤ D ^ 2 / (2 * sigma)) : phiXa - phiXlambda ≤ D ^ 2 / (2 * sigma * A)

Pure final division step from the potential invariant and evaluation at the regularized minimizer.