The literal below-two primal trajectory has the required dynamics and exact observations.

structure V7.Stage3BelowTwoS3F.PrimalState (d : ℕ) : Type

The dual accumulator, mirror point, and query point of a primal iteration.

• s : Point d

  The accumulated dual vector.

• v : Point d

  The mirror-map image of the dual accumulator.

• x : Point d

  The current primal query point.

noncomputable def V7.Stage3BelowTwoS3F.primalState {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : ℕ → PrimalState d

The literal below-two primal trajectory starting at the zero normalized state.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage3BelowTwoS3F.primalState p n oracle 0 = { s := 0, v := 0, x := 0 }

@[simp]

theorem V7.Stage3BelowTwoS3F.primalState_zero {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : primalState p n oracle 0 = { s := 0, v := 0, x := 0 }

theorem V7.Stage3BelowTwoS3F.primalState_succ {d : ℕ} (p : ℝ) (n k : ℕ) (oracle : PairOracle d) : primalState p n oracle (k + 1) = have old := primalState p n oracle k; have sNext := old.s - increment n k • oracle.gradient old.x; have vNext := belowMirrorMap p sNext; have xNext := (weight n k / weight n (k + 1)) • old.x + (increment n (k + 1) / weight n (k + 1)) • vNext + (increment n k / weight n (k + 1)) • (vNext - old.v); { s := sNext, v := vNext, x := xNext }

noncomputable def V7.Stage3BelowTwoS3F.primalTrace {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : List (Observation d)

The exact observations of the primal trajectory through the horizon.

Equations

• V7.Stage3BelowTwoS3F.primalTrace p n oracle = List.map (fun (k : ℕ) => O3.PairOracle.observe oracle (V7.Stage3BelowTwoS3F.primalState p n oracle k).x) (List.range (n + 1))

noncomputable def V7.Stage3BelowTwoS3F.primalData {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) (z : Point d) (fstar : ℝ) : BelowPrimalData p d n

The concrete primal trajectory packaged with a comparison minimizer and minimum value.

Equations

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

theorem V7.Stage3BelowTwoS3F.primal_dynamics {d : ℕ} (p : ℝ) (n : ℕ) (hn : 1 ≤ n) (oracle : PairOracle d) (z : Point d) (fstar : ℝ) : BelowPrimalDynamics (primalData p n oracle z fstar)

theorem V7.Stage3BelowTwoS3F.primal_trace_exact {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : TraceExact oracle (primalTrace p n oracle)

theorem V7.Stage3BelowTwoS3F.primal_trace_length {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : (primalTrace p n oracle).length = n + 1

theorem V7.Stage3BelowTwoS3F.primal_queried_at {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) (k : ℕ) (hk : k ≤ n) : QueriedAt (primalTrace p n oracle) k (primalState p n oracle k).x