OAI/Combinatorics/ContingencyTables/Rooted/ForestPenaltyProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Exact rational assembly of the companion forest penalty

The natural root discrepancy and the finite list of tree affine forms are combined by polynomial binary arithmetic to compute rationalD, including the original maximum-forest cuts.

  1. abbrev OAI.ContingencyTables.ForestPenaltyProgram.Input line 19
  2. def OAI.ContingencyTables.ForestPenaltyProgram.rootFractionRealizer line 21
  3. def OAI.ContingencyTables.ForestPenaltyProgram.scaleFractionRealizer line 24
  4. def OAI.ContingencyTables.ForestPenaltyProgram.treeSum line 27
  5. def OAI.ContingencyTables.ForestPenaltyProgram.treeSumRealizer line 30
  6. lemma OAI.ContingencyTables.ForestPenaltyProgram.polynomial_treeSum line 35
  7. def OAI.ContingencyTables.ForestPenaltyProgram.penaltyCode line 39
  8. def OAI.ContingencyTables.ForestPenaltyProgram.rootSumRealizer line 42
  9. lemma OAI.ContingencyTables.ForestPenaltyProgram.polynomial_rootSum line 46
  10. def OAI.ContingencyTables.ForestPenaltyProgram.penaltyCodeRealizer line 51
  11. theorem OAI.ContingencyTables.ForestPenaltyProgram.polynomial_penaltyCode line 57
  12. lemma OAI.ContingencyTables.ForestPenaltyProgram.penaltyCode_value line 62
  13. abbrev OAI.ContingencyTables.ForestPenaltyProgram.ExponentInput line 76
  14. def OAI.ContingencyTables.ForestPenaltyProgram.weightedPenalty line 78
  15. def OAI.ContingencyTables.ForestPenaltyProgram.weightedPenaltyRealizer line 81
  16. lemma OAI.ContingencyTables.ForestPenaltyProgram.polynomial_weightedPenalty line 86
  17. def OAI.ContingencyTables.ForestPenaltyProgram.exponentCode line 90
  18. def OAI.ContingencyTables.ForestPenaltyProgram.exponentCodeRealizer line 92
  19. theorem OAI.ContingencyTables.ForestPenaltyProgram.polynomial_exponentCode line 96
  20. lemma OAI.ContingencyTables.ForestPenaltyProgram.exponentCode_value line 99
  21. def OAI.ContingencyTables.ForestPenaltyProgram.rootCount line 111

    Source documentation

    This is the integral root part occurring in the source's exact forest completion, before multiplying by the softening strength.

    def rootCount (A : Instance I J) (x y : I → J → ℤ) : ℕ :=
…
  22. lemma OAI.ContingencyTables.ForestPenaltyProgram.rootCount_cast line 115
  23. def OAI.ContingencyTables.ForestPenaltyProgram.data line 127
  24. theorem OAI.ContingencyTables.ForestPenaltyProgram.penaltyCode_data line 136

    Source documentation

    The compiled finite arithmetic computes the actual rational penalty; this statement uses no oracle or approximate-evaluation premise.

    theorem penaltyCode_data (A : Instance I J) (C : ℕ) (hC : 0<C) (z : View A → ℕ)
    (trees : Fin t ≃ TreeCell A.T) (free : Fin q ≃ FreeCell A.small A.T)
    (v : FreeCell A.small A.T → ℕ) :
    TreeFraction.val (penaltyCode (data A C z trees free v))=
      rationalD A C z (fun i => (v (index A i):ℚ)) := by
…

    Mentions: OAI.ContingencyTables.ForestPenaltyProgram.penaltyCode, OAI.ContingencyTables.ForestPenaltyProgram.data

  25. theorem OAI.ContingencyTables.ForestPenaltyProgram.exponentCode_data line 154