Stage 8: the actual guarded Euclidean estimate sequence

The state stores only recursively computed vector data. The estimate minimizer, query, two oracle observations, literal potential, and guard are deterministic definitions, while their correctness properties are theorems.

noncomputable def O3.euclideanBarycenter {d : ℕ} (A a : ℝ) (x z : Vec d) : Vec d

The normalized weighted average of an accelerated point and an estimate minimizer.

Equations

• O3.euclideanBarycenter A a x z = (A + a)⁻¹ • (A • x + a • z)

structure O3.EuclideanEstimateState (d : ℕ) : Type

The accelerated iterate and accumulated gradient of the Euclidean estimate sequence.

• accelerated : Vec d

  The current accelerated iterate.

• cumulativeGradient : Vec d

  The sum of gradients weighted by the estimate-sequence increments.

noncomputable def O3.euclideanEstimateState {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) : ℕ → EuclideanEstimateState d

The recursively updated Euclidean accelerated iterate and accumulated gradient.

Equations

• One or more equations did not get rendered due to their size.
• O3.euclideanEstimateState P M 0 = { accelerated := P.x0, cumulativeGradient := 0 }

noncomputable def O3.euclideanEstimateMinimizer {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : Vec d

The minimizer of the quadratic estimate potential at iteration k.

Equations

• O3.euclideanEstimateMinimizer P M k = O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer M P.x0 (O3.euclideanEstimateState P M k).cumulativeGradient

noncomputable def O3.euclideanEstimateQuery {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : Vec d

The Euclidean oracle query obtained by averaging the iterate and estimate minimizer.

Equations

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

noncomputable def O3.euclideanEstimateObservation {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : Observation d

The value-gradient observation at the Euclidean estimate query.

Equations

• O3.euclideanEstimateObservation P M k = P.oracle.observe (O3.euclideanEstimateQuery P M k)

noncomputable def O3.euclideanEstimateConstant {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) : ℕ → ℝ

The accumulated constant term of the Euclidean estimate potential.

Equations

• One or more equations did not get rendered due to their size.
• O3.euclideanEstimateConstant P M 0 = 0

noncomputable def O3.euclideanEstimateFunction {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) : ℕ → Vec d → ℝ

The literal recursively accumulated source potential.

Equations

• One or more equations did not get rendered due to their size.
• O3.euclideanEstimateFunction P M 0 = fun (x : O3.Vec d) => M / 2 * O3.lpNorm 2 (x - P.x0) ^ 2

noncomputable def O3.euclideanEstimateMinimum {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : ℝ

The Euclidean estimate potential evaluated at its minimizer.

Equations

• O3.euclideanEstimateMinimum P M k = O3.euclideanEstimateFunction P M k (O3.euclideanEstimateMinimizer P M k)

noncomputable def O3.euclideanEstimateGuard {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : GuardCheck

The upper-model guard between the estimate query and the next accelerated iterate.

Equations

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

def O3.EuclideanEstimateAccepted {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (m : ℕ) : Prop

Every Euclidean upper-model guard before the given horizon is accepted.

Equations

• O3.EuclideanEstimateAccepted P M m = ∀ k < m, (O3.euclideanEstimateGuard P M k).Holds

@[simp]

theorem O3.euclideanEstimateState_zero {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) : euclideanEstimateState P M 0 = { accelerated := P.x0, cumulativeGradient := 0 }

theorem O3.euclideanEstimateState_succ_cumulative {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : (euclideanEstimateState P M (k + 1)).cumulativeGradient = (euclideanEstimateState P M k).cumulativeGradient + euclideanWeight (euclideanA k) • (euclideanEstimateObservation P M k).gradient

theorem O3.euclideanEstimateState_succ_accelerated {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) : (euclideanEstimateState P M (k + 1)).accelerated = euclideanBarycenter (euclideanA k) (euclideanWeight (euclideanA k)) (euclideanEstimateState P M k).accelerated (euclideanEstimateMinimizer P M (k + 1))

theorem O3.euclideanEstimateFunction_eq_canonical {d : ℕ} (P : AdmissibleInstance d 2) (M : ℝ) (k : ℕ) (x : Vec d) : euclideanEstimateFunction P M k x = Stage8EuclideanMinimizer.euclideanPsi M P.x0 (euclideanEstimateState P M k).cumulativeGradient (euclideanEstimateConstant P M k) x

Exact canonical form of the literal recursive Psi_k.

theorem O3.euclideanEstimateFunction_strongLower {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (hM : 0 < M) (k : ℕ) (x : Vec d) : euclideanEstimateFunction P M k x ≥ euclideanEstimateMinimum P M k + M / 2 * lpNorm 2 (x - euclideanEstimateMinimizer P M k) ^ 2

theorem O3.euclideanEstimateMinimum_le_function {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (hM : 0 < M) (k : ℕ) (x : Vec d) : euclideanEstimateMinimum P M k ≤ euclideanEstimateFunction P M k x

theorem O3.euclideanBarycenter_sub {d : ℕ} {A a : ℝ} (hAa : A + a ≠ 0) (x z zNext : Vec d) : euclideanBarycenter A a x zNext - euclideanBarycenter A a x z = (a / (A + a)) • (zNext - z)

The actual two barycenters have the source displacement.

theorem O3.euclideanBarycenter_balance {d : ℕ} {A a : ℝ} (hAa : A + a ≠ 0) (x z : Vec d) : A • (x - euclideanBarycenter A a x z) + a • (z - euclideanBarycenter A a x z) = 0

The old barycenter identity needed to combine convexity and the model.