OAI/Combinatorics/ContingencyTables/Rooted/RootedArithmeticStep.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedArithmeticStep.regroup line 19
2. lemma OAI.ContingencyTables.RootedArithmeticStep.word_finish_law line 25
3. def OAI.ContingencyTables.RootedArithmeticStep.wordSplit line 38
4. def OAI.ContingencyTables.RootedArithmeticStep.finish line 43
5. def OAI.ContingencyTables.RootedArithmeticStep.step line 55
6. lemma OAI.ContingencyTables.RootedArithmeticStep.source_step_eq_finish line 62
7. theorem OAI.ContingencyTables.RootedArithmeticStep.step_law line 89

   Source documentation

   Exact equality of complete one-step laws, including all holding probability. Weight calls and the acceptance coin have not been reused.

   theorem step_law (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k : ℕ)
       (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
       (v : Grid (I := Fin (dimension A)) K) (w : CompanionRationalUpdates.Pair A → CompanionRationalUpdates.Pair A → ℚ)
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.CompanionRationalUpdates.Pair

8. def OAI.ContingencyTables.RootedArithmeticStep.recordedWalk line 109

   Source documentation

   The full recorded finite-word path therefore retains the proved joint-history distribution, rather than merely its terminal marginal.

   def recordedWalk (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k N n : ℕ)
       (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
       (v : Grid (I := Fin (dimension A)) K) (w : CompanionRationalUpdates.Pair A → CompanionRationalUpdates.Pair A → ℚ)
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.CompanionRationalUpdates.Pair

9. theorem OAI.ContingencyTables.RootedArithmeticStep.recordedWalk_law line 116