OAI/Combinatorics/ContingencyTables/Transport/DyadicRootBisection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Integer implementation of the correction-root bisection

The two interval endpoints share one dyadic denominator. Every comparison is an inequality between natural powers and products. This is the literal integer algorithm to which the rational correction analysis is applied.

  1. abbrev OAI.ContingencyTables.DyadicRootBisection.State line 17
  2. def OAI.ContingencyTables.DyadicRootBisection.value line 19
  3. def OAI.ContingencyTables.DyadicRootBisection.advance line 21
  4. def OAI.ContingencyTables.DyadicRootBisection.run line 26
  5. def OAI.ContingencyTables.DyadicRootBisection.output line 30
  6. lemma OAI.ContingencyTables.DyadicRootBisection.compare_iff line 34
  7. lemma OAI.ContingencyTables.DyadicRootBisection.advance_denominator line 40
  8. lemma OAI.ContingencyTables.DyadicRootBisection.run_denominator line 45
  9. lemma OAI.ContingencyTables.DyadicRootBisection.advance_bounds line 51
  10. lemma OAI.ContingencyTables.DyadicRootBisection.run_bounds line 58
  11. lemma OAI.ContingencyTables.DyadicRootBisection.value_advance line 70
  12. theorem OAI.ContingencyTables.DyadicRootBisection.run_value line 97

    Source documentation

    Every integer execution is the rational bisection used by the already proved relative-error estimate.

    theorem run_value (c : TreeFraction.Fraction) (hc : 0<c.2) (s n : ℕ) :
    value (run c s n)=RationalRootBisection.interval (TreeFraction.val c) s n := by
…

    Mentions: OAI.ContingencyTables.DyadicRootBisection.value, OAI.ContingencyTables.DyadicRootBisection.run, OAI.ContingencyTables.RationalRootBisection.interval

  13. theorem OAI.ContingencyTables.DyadicRootBisection.output_value line 105
  14. theorem OAI.ContingencyTables.DyadicRootBisection.output_denominator_pos line 118