OAI/Combinatorics/ContingencyTables/Sampling/ExactRarePublicBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the actual public correction cost by its branch probability

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.exact_scale_absorbed line 13
  2. theorem OAI.ContingencyTables.SmallGraphProfiles.exact_public_correction_bound line 22