OAI/Combinatorics/ContingencyTables/Rooted/RootedPointPenaltyProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Executed penalty evaluation at a sampled integer assignment

At an integer point, the coordinate scale in the affine coefficient cancels its inverse in the coordinate. The program therefore forms the unscaled signed affine numerator directly from the sampled integers.

  1. def OAI.ContingencyTables.RootedPointPenaltyProgram.term line 18
  2. def OAI.ContingencyTables.RootedPointPenaltyProgram.termRealizer line 20
  3. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.polynomial_term line 23
  4. def OAI.ContingencyTables.RootedPointPenaltyProgram.tree line 27
  5. def OAI.ContingencyTables.RootedPointPenaltyProgram.treeRealizer line 29
  6. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.polynomial_tree line 33
  7. def OAI.ContingencyTables.RootedPointPenaltyProgram.prepareTree line 41
  8. def OAI.ContingencyTables.RootedPointPenaltyProgram.prepareTreeRealizer line 42
  9. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.polynomial_prepareTree line 44
  10. def OAI.ContingencyTables.RootedPointPenaltyProgram.trees line 47
  11. def OAI.ContingencyTables.RootedPointPenaltyProgram.treesRealizer line 49
  12. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.polynomial_trees line 53
  13. def OAI.ContingencyTables.RootedPointPenaltyProgram.prepare line 57
  14. def OAI.ContingencyTables.RootedPointPenaltyProgram.prepareRealizer line 59
  15. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.polynomial_prepare line 63
  16. def OAI.ContingencyTables.RootedPointPenaltyProgram.output line 69
  17. def OAI.ContingencyTables.RootedPointPenaltyProgram.outputRealizer line 70
  18. theorem OAI.ContingencyTables.RootedPointPenaltyProgram.polynomial_output line 71
  19. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.coefficient_parts line 79
  20. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.coefficient_parts_input line 88
  21. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.tree_data line 94
  22. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.rational_tree_integer line 105
  23. theorem OAI.ContingencyTables.RootedPointPenaltyProgram.tree_value line 125
  24. lemma OAI.ContingencyTables.RootedPointPenaltyProgram.trees_data line 144
  25. theorem OAI.ContingencyTables.RootedPointPenaltyProgram.output_data line 170

    Source documentation

    The executed penalty is exactly the source's rational penalty at the scaled integer assignment, with no numerical approximation.

    theorem output_data (A : Instance (Fin m) (Fin n)) (C : ℕ) (hC : 0<C)
    (x q : Fin m → Fin n → ℕ) (v : FreeCell A.small A.T → ℕ) :
    TreeFraction.val (output (RootedForestPrepareProgram.data A C
      (CompanionOracleDensity.rationalBinWidth A C) x q v))=
      RootedPenaltyProgram.rationalPenalty A (rowColumn A.T) C
        (fun i j => (x i j:ℤ)) (fun i j => (q i j:ℤ))
        (fun f => (CompanionOracleDensity.rationalBinWidth A C:ℚ)*(v f:ℚ)/
          ((A.b f.val.1 f.val.2:ℚ)+1)) := by
…

    Mentions: OAI.ContingencyTables.RootedPointPenaltyProgram.output, OAI.ContingencyTables.RootedForestPrepareProgram.data, OAI.ContingencyTables.CompanionOracleDensity.rationalBinWidth, OAI.ContingencyTables.RootedPenaltyProgram.rationalPenalty

  26. theorem OAI.ContingencyTables.RootedPointPenaltyProgram.output_integerPoint line 195
  27. theorem OAI.ContingencyTables.RootedPointPenaltyProgram.output_denominator_pos line 221