A causal local trial induces a deterministic exact-pair algorithm with its cached query charged.
def
V7.Stage5AboveTwoLowerS5F.replayTrial
{d : ℕ}
(trial : LocalTrial d)
:
trial.State → List (Observation d) → trial.State
The trial state obtained by replaying a recorded observation list.
Equations
- One or more equations did not get rendered due to their size.
- V7.Stage5AboveTwoLowerS5F.replayTrial trial x✝ [] = x✝
Instances For
def
V7.Stage5AboveTwoLowerS5F.trialActionPoint
{d : ℕ}
(trial : LocalTrial d)
(state : trial.State)
(fallback : Point d)
:
Point d
The next point requested by a trial state, or a fallback if the trial has finished.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
V7.Stage5AboveTwoLowerS5F.chargedTrialAlgorithm
{d : ℕ}
(p : ℝ)
(trial : LocalTrial d)
(M D eps : ℝ)
:
The deterministic algorithm induced by a local trial with its cached query charged.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
V7.Stage5AboveTwoLowerS5F.TrialGeneratedFrom
{d : ℕ}
(trial : LocalTrial d)
:
trial.State → List (Observation d) → Prop
The observation list follows the query actions of the trial from the supplied state.
Equations
- One or more equations did not get rendered due to their size.
- V7.Stage5AboveTwoLowerS5F.TrialGeneratedFrom trial x✝ [] = True
Instances For
theorem
V7.Stage5AboveTwoLowerS5F.runFuel_suffix
{d : ℕ}
(trial : LocalTrial d)
(oracle : PairOracle d)
{fuel : ℕ}
{state : trial.State}
{history : List (Observation d)}
{report : TrialReport d}
(hrun : trial.runFuel oracle fuel state history = some report)
:
∃ (suffix : List (Observation d)),
report.trace = history ++ suffix ∧ TrialGeneratedFrom trial state suffix ∧ TraceExact oracle suffix
theorem
V7.Stage5AboveTwoLowerS5F.generatedFrom_action_at
{d : ℕ}
(trial : LocalTrial d)
{state : trial.State}
{trace : List (Observation d)}
(fallback : Point d)
(hgen : TrialGeneratedFrom trial state trace)
{k : ℕ}
(hk : k < trace.length)
:
trialActionPoint trial (replayTrial trial state (List.take k trace)) fallback = (trace.get ⟨k, hk⟩).point
theorem
V7.Stage5AboveTwoLowerS5F.chargedTrace_generated
{d : ℕ}
{p : ℝ}
(trial : LocalTrial d)
(M D eps : ℝ)
(x0 : Point d)
(cached : Observation d)
(suffix : List (Observation d))
(hcached : cached.point = x0)
(hgen : TrialGeneratedFrom trial (trial.initial M D { observation := cached }) suffix)
:
GeneratedBy (chargedTrialAlgorithm p trial M D eps) x0 (cached :: suffix)
theorem
V7.Stage5AboveTwoLowerS5F.chargedTrial_output_spec
{d : ℕ}
{p : ℝ}
(trial : LocalTrial d)
(M D : ℝ)
{eps : ℝ}
(x0 : Point d)
(history : List (Observation d))
(hex : ∃ obs ∈ history, lpNorm (conjugateExponent p) obs.gradient ≤ eps)
:
∃ obs ∈ history,
(chargedTrialAlgorithm p trial M D eps).output x0 history = obs.point ∧ lpNorm (conjugateExponent p) obs.gradient ≤ eps