FiniteVaryingObservable.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Observable transport for independent words of varying widths

lemma OAI.ContingencyTables.FiniteObservableTransport.uniformAverage_pi_snoc line 13

theorem OAI.ContingencyTables.FiniteObservableTransport.varyingWalk_sameLaw line 24

Source documentation

The encoded state type need not be finite. Equality of every actual conditional call transfers the entire variable-width experiment.

theorem varyingWalk_sameLaw {C Z : Type*} (u v : ℕ → ℕ)
    (F : (i : ℕ) → C → (Fin (u i) → Bool) → C)
    (G : (i : ℕ) → Z → (Fin (v i) → Bool) → Z) (e : Z → C)
    (h : ∀ i z,SameLaw (F i (e z)) (fun bits => e (G i z bits)))
    (z : Z) (N : ℕ) :
    SameLaw (varyingWalk u F (e z) N) (fun bits => e (varyingWalk v G z N bits)) := by
…

Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw

theorem OAI.ContingencyTables.FiniteObservableTransport.varyingWalk_sameLaw_prefix line 44

Source documentation

Only stages actually visited need a conditional-law identification.

theorem varyingWalk_sameLaw_prefix {C Z : Type*} (u v : ℕ → ℕ)
    (F : (i : ℕ) → C → (Fin (u i) → Bool) → C)
    (G : (i : ℕ) → Z → (Fin (v i) → Bool) → Z) (e : Z → C)
    (z : Z) (N : ℕ)
    (h : ∀ i,i < N → ∀ s,SameLaw (F i (e s)) (fun bits => e (G i s bits))) :
    SameLaw (varyingWalk u F (e z) N) (fun bits => e (varyingWalk v G z N bits)) := by
…

Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw