OAI/Combinatorics/ContingencyTables/Machines/RationalIntervalProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact binary arithmetic for a forest interval penalty

A signed affine numerator is stored as a difference of two naturals. Its distance outside the interval [0,1] is a nonnegative fraction with the same denominator; no signed rational comparison is required.

  1. abbrev OAI.ContingencyTables.RationalIntervalProgram.Input line 17
  2. def OAI.ContingencyTables.RationalIntervalProgram.numerator line 19
  3. def OAI.ContingencyTables.RationalIntervalProgram.numeratorRealizer line 21
  4. lemma OAI.ContingencyTables.RationalIntervalProgram.polynomial_numerator line 28
  5. def OAI.ContingencyTables.RationalIntervalProgram.intervalCode line 40
  6. def OAI.ContingencyTables.RationalIntervalProgram.intervalCodeRealizer line 43
  7. theorem OAI.ContingencyTables.RationalIntervalProgram.polynomial_intervalCode line 47
  8. lemma OAI.ContingencyTables.RationalIntervalProgram.intervalCode_denominator line 51
  9. theorem OAI.ContingencyTables.RationalIntervalProgram.intervalCode_value line 58

    Source documentation

    Exact agreement with the interval cost in the forest density. The only side condition is the strictly positive tree capacity denominator.

    theorem intervalCode_value (p n d : ℕ) (hd : 0<d) :
    TreeFraction.val (intervalCode ((p,n),d))=
      max 0 (max (-(((p:ℚ)-n)/d)) (((p:ℚ)-n)/d-1)) := by
…

    Mentions: OAI.ContingencyTables.RationalIntervalProgram.intervalCode