OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperSuccessRatio.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.paperLarge line 17
2. lemma OAI.ContingencyTables.SmallGraphProfiles.large_padding_rows line 20
3. lemma OAI.ContingencyTables.SmallGraphProfiles.large_padding_columns line 31
4. lemma OAI.ContingencyTables.SmallGraphProfiles.paper_padded_count_le line 43
5. theorem OAI.ContingencyTables.SmallGraphProfiles.state_mass_le_original_count line 80

   Source documentation

   The numerator counts original tables through the padding bijection; the denominator counts all actual small-state/completion pairs.

   theorem state_mass_le_original_count (r : I → ℕ) (c : J → ℕ)
       (htotal : ∑ i,r i=∑ j,c j) (hd : 14 ≤ dimensionAllowance (I := I) (J := J)) :
   …

6. theorem OAI.ContingencyTables.SmallGraphProfiles.stationary_success_ratio line 93