OAI/Combinatorics/ContingencyTables/Transport/ExcessContextDefects.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Auxiliary raw profiles satisfy the literal physical defect equation

  1. lemma OAI.ContingencyTables.ExcessContextProfiles.defect_of_pair_totals line 18
  2. def OAI.ContingencyTables.ExcessContextProfiles.boundedExcess line 66
  3. lemma OAI.ContingencyTables.ExcessContextProfiles.naturalProfile_boundedExcess line 76
  4. def OAI.ContingencyTables.ExcessContextProfiles.excessDefectProfile line 84