OAI/Combinatorics/ContingencyTables/Counting/CompanionBinPopulation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionBinPopulation.coordinatePopulation line 19
2. def OAI.ContingencyTables.CompanionBinPopulation.population line 21
3. abbrev OAI.ContingencyTables.CompanionBinPopulation.Assignments line 24
4. lemma OAI.ContingencyTables.CompanionBinPopulation.assignment_card line 27
5. lemma OAI.ContingencyTables.CompanionBinPopulation.population_eq_card line 33

   Source documentation

   The product formula is exactly B^e times the integer bin population divided by the total number of free assignments.

   lemma population_eq_card (B : ℕ) (N : C → ℕ) (v : C → ℕ) :
       population B N v=(B:ℚ)^Fintype.card C*(Fintype.card (Assignments B N v):ℚ)/
         (∏ c,(N c:ℚ)) := by
   …

   Mentions: OAI.ContingencyTables.CompanionBinPopulation.population, OAI.ContingencyTables.CompanionBinPopulation.Assignments

6. lemma OAI.ContingencyTables.CompanionBinPopulation.coordinate_error line 40
7. lemma OAI.ContingencyTables.CompanionBinPopulation.reverse_bernoulli line 61
8. theorem OAI.ContingencyTables.CompanionBinPopulation.population_bounds line 79

   Source documentation

   The source's alpha_v lies between one half and two, including the empty-coordinate product. No large interval is enumerated to establish the bound; its exact cardinality is the proved ceiling difference.

   theorem population_bounds (B d : ℕ) (N : C → ℕ) (v : C → ℕ)
       (hB : 0 < B) (hd : 1 ≤ d) (hcard : Fintype.card C ≤ d)
       (hN : ∀ c,100*d*B ≤ N c) (hv : ∀ c,v c < B) :
       1/2 ≤ population B N v ∧ population B N v ≤ 2 := by
   …

   Mentions: OAI.ContingencyTables.CompanionBinPopulation.population

9. theorem OAI.ContingencyTables.CompanionBinPopulation.coordinate_nonempty line 121