OAI/Combinatorics/ContingencyTables/Counting/CompanionWarmStart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionWarmStart.total line 16
2. lemma OAI.ContingencyTables.CompanionWarmStart.total_positive line 18
3. def OAI.ContingencyTables.CompanionWarmStart.law line 21
4. lemma OAI.ContingencyTables.CompanionWarmStart.free_positive line 24
5. theorem OAI.ContingencyTables.CompanionWarmStart.law_adjacent line 31

   Source documentation

   The exact phase-j transversal law is two-warm for phase j+1. The statement applies in particular to every actual paired transversal.

   theorem law_adjacent (A : Instance I J) (j : ℕ) (S : Set (Labels A×Bool)) :
       law A j S≤2*law A (j+1) S := by
   …

   Mentions: OAI.ContingencyTables.CompanionWarmStart.law

6. theorem OAI.ContingencyTables.CompanionWarmStart.weight_bounds_zero line 45
7. theorem OAI.ContingencyTables.CompanionWarmStart.total_bounds_zero line 56
8. lemma OAI.ContingencyTables.CompanionWarmStart.zero_weight_lower line 64
9. theorem OAI.ContingencyTables.CompanionWarmStart.law_lower line 81

   Source documentation

   An explicit positive minimum mass for the actual transversal law. Its binary size depends on j and the bounded small-cell capacities.

   theorem law_lower (A : Instance I J) (j : ℕ) (S : Set (Labels A×Bool)) :
       (1/2:ℝ)^j/(CompanionFactorialApplication.denominator A*
         ∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1))≤ law A j S := by
   …

   Mentions: OAI.ContingencyTables.CompanionFactorialApplication.denominator, OAI.ContingencyTables.CompanionWarmStart.law