OAI/Combinatorics/ContingencyTables/Rooted/ForestIntegerEvaluation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Integral numerators for the literal forest penalty

Cut signs and affine completion coefficients are integers in {-1,0,1}. At an integral bin corner the tree value has the single denominator B times its capacity. This identifies the integer arithmetic consumed by the executable interval-penalty program.

  1. def OAI.ContingencyTables.ForestIntegerEvaluation.indicator line 23
  2. def OAI.ContingencyTables.ForestIntegerEvaluation.sign line 25
  3. lemma OAI.ContingencyTables.ForestIntegerEvaluation.sign_cast line 28
  4. lemma OAI.ContingencyTables.ForestIntegerEvaluation.selfSign_square line 33
  5. def OAI.ContingencyTables.ForestIntegerEvaluation.coefficient line 40
  6. lemma OAI.ContingencyTables.ForestIntegerEvaluation.coefficient_cast line 44
  7. def OAI.ContingencyTables.ForestIntegerEvaluation.smallContribution line 58
  8. lemma OAI.ContingencyTables.ForestIntegerEvaluation.smallContribution_cast line 64
  9. def OAI.ContingencyTables.ForestIntegerEvaluation.offset line 76
  10. lemma OAI.ContingencyTables.ForestIntegerEvaluation.offset_cast line 80
  11. def OAI.ContingencyTables.ForestIntegerEvaluation.numerator line 91
  12. theorem OAI.ContingencyTables.ForestIntegerEvaluation.numerator_div line 100

    Source documentation

    The exact affine tree value is a signed integral numerator divided by the explicit natural denominator, even when the original margins have very large binary representations.

    theorem numerator_div (A : Instance I J) (C : ℕ) (hC : 0<C)
    (t : TreeCell A.T) (x q : I → J → ℤ) (v : FreeCell A.small A.T → ℕ) :
    (numerator A C t x q v:ℚ)/
        ((rationalBinWidth A C:ℚ)*A.b t.val.1 t.val.2)=
      rationalScaledTree A C x q (fun f => (v f:ℚ)) t := by
…

    Mentions: OAI.ContingencyTables.ForestIntegerEvaluation.numerator

  13. def OAI.ContingencyTables.ForestIntegerEvaluation.treeData line 128
  14. theorem OAI.ContingencyTables.ForestIntegerEvaluation.treeData_value line 135

    Source documentation

    Each summand of the literal rational forest penalty is exactly the output of the compiled nonnegative interval-arithmetic routine.

    theorem treeData_value (A : Instance I J) (C : ℕ) (hC : 0<C)
    (t : TreeCell A.T) (x q : I → J → ℤ) (v : FreeCell A.small A.T → ℕ) :
    MatchingFPRAS.TreeFraction.val (RationalIntervalProgram.intervalCode (treeData A C t x q v))=
      max 0 (max (-rationalScaledTree A C x q (fun f => (v f:ℚ)) t)
        (rationalScaledTree A C x q (fun f => (v f:ℚ)) t-1)) := by
…

    Mentions: OAI.MatchingFPRAS.TreeFraction.val, OAI.ContingencyTables.RationalIntervalProgram.intervalCode, OAI.ContingencyTables.ForestIntegerEvaluation.treeData