OAI/Combinatorics/ContingencyTables/Transport/FiniteProjectedHistory.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.FiniteObservableTransport.projected_foldl_sameLaw line 13

   Source documentation

   Intermediate representations may vary as long as their projected next-step law agrees and the representation invariant is preserved.

   theorem projected_foldl_sameLaw {C Z U V : Type*} [Fintype U] [Fintype V]
       (F : C→U→C) (G : Z→V→Z) (e : C→Z) (Valid : C→Prop)
       (hvalid : ∀ c,Valid c→∀ u,Valid (F c u))
       (hstep : ∀ c,Valid c→SameLaw (fun u => e (F c u)) (G (e c)))
       (c : C) (hc : Valid c) (N : ℕ) :
       SameLaw (fun us : Fin N→U => e ((List.ofFn us).foldl F c))
         (fun vs : Fin N→V => (List.ofFn vs).foldl G (e c)) := by
   …

   Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw