FiniteAdaptiveObservable.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Observable laws under adaptive finite-word calls

The stored state may include rational estimates and is not assumed finite. Each fresh word is finite; equality of every conditional call therefore suffices for equality of the entire executed history.

theorem OAI.ContingencyTables.FiniteObservableTransport.SameLaw.bind line 22
def OAI.ContingencyTables.FiniteObservableTransport.adaptiveRun line 32
theorem OAI.ContingencyTables.FiniteObservableTransport.adaptiveRun_sameLaw line 36
def OAI.ContingencyTables.FiniteObservableTransport.appendStep line 50
theorem OAI.ContingencyTables.FiniteObservableTransport.appendStep_sameLaw line 53
theorem OAI.ContingencyTables.FiniteObservableTransport.adaptiveHistory_sameLaw line 60
Source documentation
This transports complete stored histories, hence also every final estimate and every abort event obtained from that history.
```
theorem adaptiveHistory_sameLaw (F : List Z → X → Z) (G : List Z → Y → Z)
    (h : ∀ history,SameLaw (F history) (G history)) (history : List Z) (N : ℕ) :
    SameLaw (adaptiveRun (appendStep F) history N)
      (adaptiveRun (appendStep G) history N) :=
…
```
Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw, OAI.ContingencyTables.FiniteObservableTransport.adaptiveRun, OAI.ContingencyTables.FiniteObservableTransport.appendStep