OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleCorrection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exact population correction for the computed-root completion count

Integer bins and their executable interval draws are the existing physical bins. Only their positive density weights change with the explicit root selector. All normalizer identities are finite sums.

  1. def OAI.ContingencyTables.RootedOracleDensity.gridWeight line 22
  2. lemma OAI.ContingencyTables.RootedOracleDensity.gridWeight_positive line 26
  3. lemma OAI.ContingencyTables.RootedOracleDensity.density_at_integer line 30
  4. lemma OAI.ContingencyTables.RootedOracleDensity.sum_density_integer line 51
  5. def OAI.ContingencyTables.RootedOracleDensity.binSum line 60
  6. lemma OAI.ContingencyTables.RootedOracleDensity.binSum_positive line 64
  7. def OAI.ContingencyTables.RootedOracleDensity.correctedMass line 70
  8. def OAI.ContingencyTables.RootedOracleDensity.correction line 75
  9. lemma OAI.ContingencyTables.RootedOracleDensity.correctedMass_nonnegative line 80
  10. theorem OAI.ContingencyTables.RootedOracleDensity.correction_bounds line 87
  11. lemma OAI.ContingencyTables.RootedOracleDensity.corrected_mass_product line 129
  12. theorem OAI.ContingencyTables.RootedOracleDensity.corrected_expectation line 142
  13. theorem OAI.ContingencyTables.RootedOracleDensity.correctedMass_total line 151
  14. def OAI.ContingencyTables.RootedOracleDensity.ratioObservable line 180
  15. def OAI.ContingencyTables.RootedOracleDensity.ratioMean line 184
  16. lemma OAI.ContingencyTables.RootedOracleDensity.ratioMean_eq line 189
  17. lemma OAI.ContingencyTables.RootedOracleDensity.binSum_zero line 204
  18. lemma OAI.ContingencyTables.RootedOracleDensity.ratio_telescope line 210
  19. theorem OAI.ContingencyTables.RootedOracleDensity.oracle_telescope line 222