OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleRational.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Exact rational arithmetic for the companion evaluator's bin weights

  1. def OAI.ContingencyTables.CompanionOracleDensity.rationalIndicator line 18
  2. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalIndicator_cast line 20
  3. def OAI.ContingencyTables.CompanionOracleDensity.rationalSign line 23
  4. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalSign_cast line 26
  5. def OAI.ContingencyTables.CompanionOracleDensity.rationalCoefficient line 30
  6. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalCoefficient_cast line 34
  7. def OAI.ContingencyTables.CompanionOracleDensity.rationalSmallContribution line 39
  8. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalSmallContribution_cast line 45
  9. def OAI.ContingencyTables.CompanionOracleDensity.rationalOffset line 56
  10. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalOffset_cast line 60
  11. def OAI.ContingencyTables.CompanionOracleDensity.rationalBinWidth line 67
  12. def OAI.ContingencyTables.CompanionOracleDensity.rationalHeight line 69
  13. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalBinWidth_cast line 71
  14. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalHeight_cast line 75
  15. def OAI.ContingencyTables.CompanionOracleDensity.rationalScaledTree line 79
  16. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalScaledTree_cast line 86
  17. def OAI.ContingencyTables.CompanionOracleDensity.rationalRootConstant line 94
  18. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalRootConstant_cast line 98
  19. def OAI.ContingencyTables.CompanionOracleDensity.rationalD line 106
  20. theorem OAI.ContingencyTables.CompanionOracleDensity.rationalD_cast line 115

    Source documentation

    The rational calculation is termwise equal to the geometric density penalty; it does not use an approximation or enumerate free assignments.

    theorem rationalD_cast (A : Instance I J) (C : ℕ) (z : View A → ℕ)
    (v : Fin (dimension A) → ℚ) :
    (rationalD A C z v:ℝ)=D A C z (fun i => (v i:ℝ)) := by
…

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.CompanionOracleDensity.rationalD, OAI.ContingencyTables.CompanionOracleDensity.D

  21. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalD_nonnegative line 123
  22. def OAI.ContingencyTables.CompanionOracleDensity.gridExponent line 131
  23. theorem OAI.ContingencyTables.CompanionOracleDensity.gridExponent_eq_floor line 135
  24. theorem OAI.ContingencyTables.CompanionOracleDensity.gridWeight_eq_dyadic line 148
  25. theorem OAI.ContingencyTables.CompanionOracleDensity.gridExponent_upper line 155
  26. def OAI.ContingencyTables.CompanionOracleDensity.rationalGridWeight line 180
  27. theorem OAI.ContingencyTables.CompanionOracleDensity.rationalGridWeight_cast line 184
  28. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalGridWeight_positive line 190