OAI/Combinatorics/ContingencyTables/Rooted/ForestAffineProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Binary list evaluation of the forest's signed affine numerators

Each coefficient is stored by its nonnegative and nonpositive parts. The program performs two finite product sums and passes their difference to the proved interval-cost routine. Large capacities are never iterated.

  1. abbrev OAI.ContingencyTables.ForestAffineProgram.Term line 18
  2. abbrev OAI.ContingencyTables.ForestAffineProgram.Input line 19
  3. def OAI.ContingencyTables.ForestAffineProgram.positiveTerm line 21
  4. def OAI.ContingencyTables.ForestAffineProgram.negativeTerm line 22
  5. def OAI.ContingencyTables.ForestAffineProgram.positiveTermRealizer line 24
  6. def OAI.ContingencyTables.ForestAffineProgram.negativeTermRealizer line 28
  7. lemma OAI.ContingencyTables.ForestAffineProgram.polynomial_positiveTerm line 32
  8. lemma OAI.ContingencyTables.ForestAffineProgram.polynomial_negativeTerm line 36
  9. def OAI.ContingencyTables.ForestAffineProgram.positiveSumRealizer line 40
  10. def OAI.ContingencyTables.ForestAffineProgram.negativeSumRealizer line 43
  11. lemma OAI.ContingencyTables.ForestAffineProgram.polynomial_positiveSum line 46
  12. lemma OAI.ContingencyTables.ForestAffineProgram.polynomial_negativeSum line 49
  13. def OAI.ContingencyTables.ForestAffineProgram.parts line 52
  14. def OAI.ContingencyTables.ForestAffineProgram.partsRealizer line 55
  15. lemma OAI.ContingencyTables.ForestAffineProgram.polynomial_parts line 62
  16. def OAI.ContingencyTables.ForestAffineProgram.evaluate line 73
  17. def OAI.ContingencyTables.ForestAffineProgram.evaluateRealizer line 76
  18. theorem OAI.ContingencyTables.ForestAffineProgram.polynomial_evaluate line 80
  19. def OAI.ContingencyTables.ForestAffineProgram.signedParts line 84
  20. lemma OAI.ContingencyTables.ForestAffineProgram.signedParts_sub line 86
  21. def OAI.ContingencyTables.ForestAffineProgram.data line 93
  22. lemma OAI.ContingencyTables.ForestAffineProgram.parts_data line 96
  23. theorem OAI.ContingencyTables.ForestAffineProgram.evaluate_data line 109

    Source documentation

    All signs and products in an affine tree term are executed in binary; the resulting fraction is its exact interval penalty.

    theorem evaluate_data (offset : ℤ) (coefficient : Fin q → ℤ) (v : Fin q → ℕ)
    (den : ℕ) (hd : 0<den) :
    TreeFraction.val (evaluate (data offset coefficient v den))=
      max 0 (max (-(((offset:ℚ)+∑ i,(coefficient i:ℚ)*(v i:ℚ))/den))
        (((offset:ℚ)+∑ i,(coefficient i:ℚ)*(v i:ℚ))/den-1)) := by
…

    Mentions: OAI.ContingencyTables.ForestAffineProgram.evaluate, OAI.ContingencyTables.ForestAffineProgram.data

  24. def OAI.ContingencyTables.ForestAffineProgram.forestData line 132
  25. theorem OAI.ContingencyTables.ForestAffineProgram.evaluate_forest line 142

    Source documentation

    This input is the literal cut-derived affine form of the manuscript. The executable value is its exact contribution to the softened penalty.

    theorem evaluate_forest (A : Instance I J) (C : ℕ) (hC : 0<C) (t : TreeCell A.T)
    (x y : I → J → ℤ) (e : Fin q ≃ FreeCell A.small A.T)
    (v : FreeCell A.small A.T → ℕ) :
    TreeFraction.val (evaluate (forestData A C t x y e v))=
      max 0 (max (-rationalScaledTree A C x y (fun f => (v f:ℚ)) t)
        (rationalScaledTree A C x y (fun f => (v f:ℚ)) t-1)) := by
…

    Mentions: OAI.ContingencyTables.ForestAffineProgram.evaluate, OAI.ContingencyTables.ForestAffineProgram.forestData