OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleRational.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The computed-root grid weights are exactly dyadic rational values

  1. def OAI.ContingencyTables.RootedOracleDensity.rationalD line 16
  2. theorem OAI.ContingencyTables.RootedOracleDensity.rationalD_cast line 21
  3. lemma OAI.ContingencyTables.RootedOracleDensity.rationalD_nonnegative line 27
  4. def OAI.ContingencyTables.RootedOracleDensity.gridExponent line 33
  5. theorem OAI.ContingencyTables.RootedOracleDensity.gridExponent_eq_floor line 37
  6. theorem OAI.ContingencyTables.RootedOracleDensity.gridWeight_eq_dyadic line 50
  7. def OAI.ContingencyTables.RootedOracleDensity.rationalGridWeight line 57
  8. theorem OAI.ContingencyTables.RootedOracleDensity.rationalGridWeight_cast line 61
  9. theorem OAI.ContingencyTables.RootedOracleDensity.exponentCode_grid line 67