FiniteEncodedHistory.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Complete histories under an encoded transition law

def OAI.ContingencyTables.FiniteObservableTransport.traceAfter line 12
def OAI.ContingencyTables.FiniteObservableTransport.traceStates line 16
lemma OAI.ContingencyTables.FiniteObservableTransport.traceAfter_map line 19
lemma OAI.ContingencyTables.FiniteObservableTransport.traceStates_map line 26
theorem OAI.ContingencyTables.FiniteObservableTransport.traceStates_sameLaw line 37
Source documentation
Equality of the encoded row laws transfers the whole finite history, including observables depending on every visited state.
```
theorem traceStates_sameLaw (F : C → U → C) (G : Z → V → Z) (e : Z → C)
    (h : ∀ z,SameLaw (F (e z)) (fun v => e (G z v))) (z : Z) (N : ℕ) :
    SameLaw (fun us : Fin N → U => traceStates F (e z) (List.ofFn us))
      (fun vs : Fin N → V => (traceStates G z (List.ofFn vs)).map e) := by
…
```
Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw, OAI.ContingencyTables.FiniteObservableTransport.traceStates

theorem OAI.ContingencyTables.FiniteObservableTransport.foldl_sameLaw line 57

Source documentation

The same encoding argument also transports a terminal state without requiring a decoder or finiteness of the encoded state space.

theorem foldl_sameLaw (F : C → U → C) (G : Z → V → Z) (e : Z → C)
    (h : ∀ z,SameLaw (F (e z)) (fun v => e (G z v))) (z : Z) (N : ℕ) :
    SameLaw (fun us : Fin N → U => (List.ofFn us).foldl F (e z))
      (fun vs : Fin N → V => e ((List.ofFn vs).foldl G z)) := by
…

Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw

lemma OAI.ContingencyTables.FiniteObservableTransport.traceAfter_fold line 77
Source documentation
The reverse accumulator used by a bounded fold has precisely the chronological history after reversing its stored list.
```
lemma traceAfter_fold (F : C → U → C) (us : List U) (c : C) (history : List C) :
    (us.foldl (fun s u => let d := F s.1 u; (d,d::s.2)) (c,history)).2.reverse=
…
```
lemma OAI.ContingencyTables.FiniteObservableTransport.traceStates_fold line 88