Consecutive below-two guard checks match the cached observation and the two phase traces.

noncomputable def V7.Stage3BelowTwoS3F.chainChecks {d : ℕ} (first : Observation d) : List (Observation d) → List (ObservableGuardCheck d)

The cocoercivity checks between consecutive observations, starting from a cached observation.

Equations

• V7.Stage3BelowTwoS3F.chainChecks first [] = []
• V7.Stage3BelowTwoS3F.chainChecks first (obs :: rest) = V7.Stage3BelowTwoS3F.cocoCheck first obs :: V7.Stage3BelowTwoS3F.chainChecks obs rest

@[simp]

theorem V7.Stage3BelowTwoS3F.chainChecks_length {d : ℕ} (first : Observation d) (trace : List (Observation d)) : (chainChecks first trace).length = trace.length

theorem V7.Stage3BelowTwoS3F.chainChecks_append {d : ℕ} (first : Observation d) (xs ys : List (Observation d)) : chainChecks first (xs ++ ys) = chainChecks first xs ++ chainChecks (xs.getLastD first) ys

theorem V7.Stage3BelowTwoS3F.chainChecks_kinds {d : ℕ} (first : Observation d) (trace : List (Observation d)) (check : ObservableGuardCheck d) : check ∈ chainChecks first trace → check.kind = ObservableGuardKind.cocoercivity

theorem V7.Stage3BelowTwoS3F.chainChecks_ledger {d : ℕ} (cached : CachedPair d) (trace : List (Observation d)) : ConsecutiveGuardLedger cached { trace := trace, checkedGuards := chainChecks cached.observation trace, outcome := TrialOutcome.radius cached.observation }

theorem V7.Stage3BelowTwoS3F.chainChecks_ledger_prefix {d : ℕ} (cached : CachedPair d) (pre suf : List (Observation d)) : ConsecutiveGuardLedger cached { trace := pre ++ suf, checkedGuards := chainChecks cached.observation pre, outcome := TrialOutcome.radius cached.observation }

theorem V7.Stage3BelowTwoS3F.chainChecks_data_exact {d : ℕ} (cached : CachedPair d) (oracle : PairOracle d) (trace : List (Observation d)) (hcached : cached.observation = O3.PairOracle.observe oracle cached.observation.point) (htrace : TraceExact oracle trace) : GuardDataExact cached oracle { trace := trace, checkedGuards := chainChecks cached.observation trace, outcome := TrialOutcome.radius cached.observation }

theorem V7.Stage3BelowTwoS3F.chainChecks_data_exact_prefix {d : ℕ} (cached : CachedPair d) (oracle : PairOracle d) (pre suf : List (Observation d)) (hcached : cached.observation = O3.PairOracle.observe oracle cached.observation.point) (hpre : TraceExact oracle pre) : GuardDataExact cached oracle { trace := pre ++ suf, checkedGuards := chainChecks cached.observation pre, outcome := TrialOutcome.radius cached.observation }

theorem V7.Stage3BelowTwoS3F.cocoPairHolds_iff_not_fails {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (x y : Point d) : cocoPairHolds p M (O3.PairOracle.observe oracle x) (O3.PairOracle.observe oracle y) ↔ ¬GuardFails p M oracle (cocoCheck (O3.PairOracle.observe oracle x) (O3.PairOracle.observe oracle y)).failure

theorem V7.Stage3BelowTwoS3F.phaseOneTrace_lastD {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : (phaseOneNewTrace p eps M D x0 oracle m).getLastD (phaseOneObs p eps M D x0 oracle 0) = phaseOneObs p eps M D x0 oracle m

theorem V7.Stage3BelowTwoS3F.phaseTwoTrace_lastD {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : (phaseTwoNewTrace p eps M D x0 oracle m).getLastD (phaseTwoObs p eps M D x0 oracle 0) = phaseTwoObs p eps M D x0 oracle m

theorem V7.Stage3BelowTwoS3F.phaseOne_chain {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : chainChecks (phaseOneObs p eps M D x0 oracle 0) (phaseOneNewTrace p eps M D x0 oracle m) = phaseOneChecks p eps M D x0 oracle m

theorem V7.Stage3BelowTwoS3F.phaseTwo_chain {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : chainChecks (phaseTwoObs p eps M D x0 oracle 0) (phaseTwoNewTrace p eps M D x0 oracle m) = phaseTwoChecks p eps M D x0 oracle m

theorem V7.Stage3BelowTwoS3F.total_chain {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m₁ m₂ : ℕ) (hm₁ : m₁ = horizon p eps M D) : chainChecks (phaseOneObs p eps M D x0 oracle 0) (phaseOneNewTrace p eps M D x0 oracle m₁ ++ phaseTwoNewTrace p eps M D x0 oracle m₂) = allChecks p eps M D x0 oracle m₁ m₂