OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The selected-root evaluator density on its actual finite bin cube

  1. def OAI.ContingencyTables.RootedOracleDensity.D line 16
  2. lemma OAI.ContingencyTables.RootedOracleDensity.D_nonnegative line 21
  3. theorem OAI.ContingencyTables.RootedOracleDensity.D_bounds line 25
  4. theorem OAI.ContingencyTables.RootedOracleDensity.D_change line 36
  5. theorem OAI.ContingencyTables.RootedOracleDensity.D_continuous line 50
  6. theorem OAI.ContingencyTables.RootedOracleDensity.D_convex line 56
  7. def OAI.ContingencyTables.RootedOracleDensity.rho line 64
  8. def OAI.ContingencyTables.RootedOracleDensity.V line 68
  9. theorem OAI.ContingencyTables.RootedOracleDensity.rho_continuous line 72
  10. theorem OAI.ContingencyTables.RootedOracleDensity.rho_positive line 76
  11. theorem OAI.ContingencyTables.RootedOracleDensity.rho_logConcave line 80
  12. theorem OAI.ContingencyTables.RootedOracleDensity.exponent_change line 87
  13. theorem OAI.ContingencyTables.RootedOracleDensity.bin_comparison line 99