The concrete above-two phase trajectories satisfy the operational trial contract.
noncomputable def
V7.Stage4AboveTwoFinalTrial.shapeWitness
{d : ℕ}
(p eps M D : ℝ)
(x0 : Point d)
(oracle : PairOracle d)
(m₁ m₂ : ℕ)
:
The concrete above-two trajectories and budgets packaged as an operational witness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
V7.Stage4AboveTwoFinalTrial.fullShape_operational_contract
{d : ℕ}
{eps : ℝ}
{oracle : PairOracle d}
{report : TrialReport d}
{cached : CachedPair d}
{p M D : ℝ}
{x0 : O3.Vec d}
{m₁ m₂ : ℕ}
(hp : 2 < p)
(heps : 0 < eps)
(hM : 0 < M)
(hD : 0 < D)
(hcached : cached.observation = O3.PairOracle.observe oracle x0)
(hshape : FullShape p eps M D x0 oracle report m₁ m₂)
:
AboveTrialOperationalContract p eps M D x0 cached oracle report (shapeWitness p eps M D x0 oracle m₁ m₂)