The literal Euclidean trajectories packaged with their dynamics and exact traces.

noncomputable def V7.Stage1E03.sourceEstimateState {d : ℕ} (oracle : PairOracle d) (M : ℝ) (x0 : Point d) : ℕ → O3.EuclideanEstimateState d

The literal recursive estimate state driven by an arbitrary value-gradient oracle.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage1E03.sourceEstimateState oracle M x0 0 = { accelerated := x0, cumulativeGradient := 0 }

noncomputable def V7.Stage1E03.sourceEstimateMinimizer {d : ℕ} (oracle : PairOracle d) (M : ℝ) (x0 : Point d) (k : ℕ) : Point d

The quadratic potential minimizer associated with the source estimate state.

Equations

• V7.Stage1E03.sourceEstimateMinimizer oracle M x0 k = O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer M x0 (V7.Stage1E03.sourceEstimateState oracle M x0 k).cumulativeGradient

noncomputable def V7.Stage1E03.sourcePhaseAWeight : ℕ → ℝ

The source estimate-weight increment, extended by zero at index zero.

Equations

• V7.Stage1E03.sourcePhaseAWeight 0 = 0
• V7.Stage1E03.sourcePhaseAWeight k.succ = O3.euclideanWeight (O3.euclideanA k)

noncomputable def V7.Stage1E03.sourcePhaseAData {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M D : ℝ) (m : ℕ) : EuclideanGapData d m

The literal source estimate execution packaged as Euclidean gap-phase data.

Equations

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

noncomputable def V7.Stage1E03.sourcePhaseBData {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (n : ℕ) (U : Point d) : OGMGData d n

The literal source OGM-G execution packaged as finite phase data.

Equations

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

@[simp]

theorem V7.Stage1E03.sourceEstimateState_zero {d : ℕ} (oracle : PairOracle d) (M : ℝ) (x0 : Point d) : sourceEstimateState oracle M x0 0 = { accelerated := x0, cumulativeGradient := 0 }

@[simp]

theorem V7.Stage1E03.sourceEstimateState_succ {d : ℕ} (oracle : PairOracle d) (M : ℝ) (x0 : Point d) (k : ℕ) : sourceEstimateState oracle M x0 (k + 1) = nextEstimateState M x0 k (sourceEstimateState oracle M x0 k) (O3.PairOracle.observe oracle (estimateQuery M x0 k (sourceEstimateState oracle M x0 k)))

theorem V7.Stage1E03.sourceEstimate_cumulative {d : ℕ} (oracle : PairOracle d) (M : ℝ) (x0 : Point d) (k : ℕ) : (sourceEstimateState oracle M x0 k).cumulativeGradient = fun (j : Fin d) => ∑ i ∈ Finset.range k, O3.euclideanWeight (O3.euclideanA i) * oracle.gradient (estimateQuery M x0 i (sourceEstimateState oracle M x0 i)) j

theorem V7.Stage1E03.sourcePhaseA_dynamics {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M D : ℝ) (m : ℕ) (hM : 0 < M) : EuclideanGapDynamics (sourcePhaseAData inst M D m)

theorem V7.Stage1E03.sourcePhaseB_dynamics {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (n : ℕ) (U : Point d) (hM : 0 < M) (hn : 1 ≤ n) : OGMGDynamics (sourcePhaseBData inst M n U)

theorem V7.Stage1E03.sourcePhaseA_trace_exact {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M D : ℝ) (m : ℕ) : TraceExact inst.oracle (sourcePhaseAData inst M D m).trace

theorem V7.Stage1E03.sourcePhaseB_trace_exact {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (n : ℕ) (U : Point d) : TraceExact inst.oracle (sourcePhaseBData inst M n U).trace

@[simp]

theorem V7.Stage1E03.phaseABudget_eq (n fuel : ℕ) : phaseABudget n fuel = 2 * fuel + n + 1