OAI/Combinatorics/ContingencyTables/Counting/CompanionObservedUpdateLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.CompanionObservedUpdateProgram.LabelIndex line 16
2. def OAI.ContingencyTables.CompanionObservedUpdateProgram.data line 18
3. theorem OAI.ContingencyTables.CompanionObservedUpdateProgram.output_values line 27
4. theorem OAI.ContingencyTables.CompanionObservedUpdateProgram.sameLaw line 53
5. theorem OAI.ContingencyTables.CompanionObservedUpdateProgram.sameLaw_phase line 79

   Source documentation

   The complete executed observation-and-update has the actual phase law.

   theorem sameLaw_phase (C K j : ℕ)
       (hC : 0 < C) (hj : j+1 ≤ rationalHeight A C) (hK : 1 ≤ K)
       (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
       (xi : ℚ) (hxi : 0 < xi) (z : View A→ℕ)
       (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
   …

   Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount