The above-two trial parameters, explicit primal trajectory, and mutually recursive dual trajectory.

noncomputable def V7.Stage4AboveTwoFinalTrial.delta (eps M D : ℝ) : ℝ

The accuracy normalized by the trial's smoothness and distance estimates.

Equations

• V7.Stage4AboveTwoFinalTrial.delta eps M D = eps / (M * D)

noncomputable def V7.Stage4AboveTwoFinalTrial.etaF (p : ℝ) : ℝ

The primal phase error budget 1 / p.

Equations

• V7.Stage4AboveTwoFinalTrial.etaF p = 1 / p

noncomputable def V7.Stage4AboveTwoFinalTrial.etaD (p eps M D : ℝ) : ℝ

The dual phase error budget determined by the normalized accuracy.

Equations

• V7.Stage4AboveTwoFinalTrial.etaD p eps M D = V7.Stage4AboveTwoFinalTrial.delta eps M D ^ V7.conjugateExponent p / V7.conjugateExponent p

noncomputable def V7.Stage4AboveTwoFinalTrial.nF (p eps M D : ℝ) : ℕ

The ceiling of the primal horizon required by the above-two gap bound.

Equations

• V7.Stage4AboveTwoFinalTrial.nF p eps M D = ⌈(V7.aboveHp p / V7.Stage4AboveTwoFinalTrial.delta eps M D) ^ (p / (p + 2))⌉₊

noncomputable def V7.Stage4AboveTwoFinalTrial.nD (p eps M D : ℝ) : ℕ

The ceiling of the dual horizon required by the above-two gradient bound.

Equations

• V7.Stage4AboveTwoFinalTrial.nD p eps M D = ⌈(V7.aboveJp p / V7.Stage4AboveTwoFinalTrial.delta eps M D) ^ (p / (p + 2))⌉₊

theorem V7.Stage4AboveTwoFinalTrial.delta_pos {eps M D : ℝ} (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) : 0 < delta eps M D

theorem V7.Stage4AboveTwoFinalTrial.etaF_pos {p : ℝ} (hp : 2 < p) : 0 < etaF p

theorem V7.Stage4AboveTwoFinalTrial.etaD_pos {p eps M D : ℝ} (hp : 2 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) : 0 < etaD p eps M D

theorem V7.Stage4AboveTwoFinalTrial.one_le_nF {p eps M D : ℝ} (hp : 2 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) : 1 ≤ nF p eps M D

theorem V7.Stage4AboveTwoFinalTrial.one_le_nD {p eps M D : ℝ} (hp : 2 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) : 1 ≤ nD p eps M D

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

The dual accumulator, mirror point, and query point of an above-two primal iteration.

• s : Point d

  The accumulated dual vector.

• v : Point d

  The power mirror-map image of the accumulated dual vector.

• x : Point d

  The current primal query point.

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

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

Equations

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

@[simp]

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

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

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

The exact observations at the primal queries through the horizon.

Equations

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

noncomputable def V7.Stage4AboveTwoFinalTrial.primalData {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) (fstar : ℝ) : AbovePrimalPhaseData p d n

The concrete above-two primal trajectory packaged with its minimum objective value.

Equations

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

theorem V7.Stage4AboveTwoFinalTrial.primal_dynamics {d : ℕ} (p eta : ℝ) (n : ℕ) (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) (oracle : PairOracle d) (fstar : ℝ) : AbovePrimalPhaseDynamics (primalData p eta n oracle fstar)

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

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

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

@[irreducible]

noncomputable def V7.Stage4AboveTwoFinalTrial.dualQ {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) : ℕ → Point d

The recursively generated normalized query points of the above-two dual phase.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage4AboveTwoFinalTrial.dualQ p eta n oracle 0 = 0

@[irreducible]

noncomputable def V7.Stage4AboveTwoFinalTrial.dualR {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) : ℕ → Point d

The recursively accumulated vectors of the above-two dual phase.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage4AboveTwoFinalTrial.dualR p eta n oracle 0 = -V7.Stage4AboveTwoFinalTrial.coeffB p eta n n n • oracle.gradient 0