The above-two dual trajectory satisfies its dynamics and exact observation requirements.

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.dualQ_zero {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) : dualQ p eta n oracle 0 = 0

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.dualR_zero {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) : dualR p eta n oracle 0 = -coeffB p eta n n n • oracle.gradient 0

theorem V7.Stage4AboveTwoFinalTrial.dualQ_succ {d : ℕ} (p eta : ℝ) (n k : ℕ) (oracle : PairOracle d) : dualQ p eta n oracle (k + 1) = dualQ p eta n oracle k - increment p eta n (n - 1 - k) • aboveMirrorMap p (dualR p eta n oracle k)

theorem V7.Stage4AboveTwoFinalTrial.dualR_succ {d : ℕ} (p eta : ℝ) (n k : ℕ) (oracle : PairOracle d) : dualR p eta n oracle (k + 1) = dualR p eta n oracle k - weightedSum (k + 2) (fun (i : ℕ) => coeffB p eta n (n - i) (n - 1 - k)) fun (i : ℕ) => oracle.gradient (dualQ p eta n oracle i)

theorem V7.Stage4AboveTwoFinalTrial.antiDiagonal_alpha {d : ℕ} (p eta : ℝ) (n k : ℕ) (hk : k < n) (Z : VectorSeq d) : weightedSum (k + 1) (fun (i : ℕ) => alpha p eta n (n - i) (n - 1 - k)) Z = increment p eta n (n - 1 - k) • Z k

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

The exact observations at the dual queries through the horizon.

Equations

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

noncomputable def V7.Stage4AboveTwoFinalTrial.dualData {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) : AboveDualPhaseData p d n

The concrete dual trajectories and coefficients packaged as above-two phase data.

Equations

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

theorem V7.Stage4AboveTwoFinalTrial.dual_dynamics {d : ℕ} (p eta : ℝ) (n : ℕ) (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) (oracle : PairOracle d) : AboveDualPhaseDynamics (dualData p eta n oracle)

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

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

theorem V7.Stage4AboveTwoFinalTrial.dual_queried_at {d : ℕ} (p eta : ℝ) (n : ℕ) (oracle : PairOracle d) (k : ℕ) (hk : k ≤ n) : QueriedAt (dualTrace p eta n oracle) k (dualQ p eta n oracle k)