OAI/Combinatorics/ContingencyTables/Rooted/RootedPenaltyEvaluateProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

A polynomial binary program for the actual forest exponent

The bin width and height are computed from the dimension allowance, capacity scale and phase coefficient. All forest metadata is generated from the cell arrays by RootedForestPrepareProgram.

  1. abbrev OAI.ContingencyTables.RootedPenaltyEvaluateProgram.Parameters line 18
  2. abbrev OAI.ContingencyTables.RootedPenaltyEvaluateProgram.Input line 19
  3. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.squareDimension line 21
  4. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.squareDimensionRealizer line 22
  5. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_squareDimension line 24
  6. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.scaledSquare line 29
  7. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.scaledSquareRealizer line 30
  8. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_scaledSquare line 33
  9. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.width line 38
  10. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.widthRealizer line 39
  11. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_width line 42
  12. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.baseHeight line 46
  13. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.baseHeightRealizer line 47
  14. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_baseHeight line 50
  15. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.height line 54
  16. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.heightRealizer line 55
  17. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_height line 58
  18. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.forestInput line 63
  19. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.forestInputRealizer line 65
  20. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_forestInput line 69
  21. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.exponentInput line 77
  22. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.exponentInputRealizer line 79
  23. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_exponentInput line 84
  24. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.evaluate line 90
  25. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.evaluateRealizer line 91
  26. theorem OAI.ContingencyTables.RootedPenaltyEvaluateProgram.polynomial_evaluate line 94
  27. def OAI.ContingencyTables.RootedPenaltyEvaluateProgram.data line 99
  28. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.width_data line 104
  29. lemma OAI.ContingencyTables.RootedPenaltyEvaluateProgram.height_data line 109
  30. theorem OAI.ContingencyTables.RootedPenaltyEvaluateProgram.exponentInput_data line 115
  31. theorem OAI.ContingencyTables.RootedPenaltyEvaluateProgram.evaluate_data line 129

    Source documentation

    The code evaluates the literal rational forest penalty with its source normalization, without an affine-data or evaluator hypothesis.

    theorem evaluate_data {m n : ℕ} (A : Instance (Fin m) (Fin n)) (C a : ℕ) (hC : 0 < C)
    (x q : Fin m → Fin n → ℕ) (v : FreeCell A.small A.T → ℕ) :
    evaluate (data A C a x q v)=
      ⌊(a:ℚ)/CompanionOracleDensity.rationalHeight A C*
        RootedPenaltyProgram.rationalPenalty A (rowColumn A.T) C
          (fun i j => (x i j:ℤ)) (fun i j => (q i j:ℤ)) (fun f => (v f:ℚ))⌋₊ := by
…

    Mentions: OAI.ContingencyTables.RootedPenaltyEvaluateProgram.evaluate, OAI.ContingencyTables.RootedPenaltyEvaluateProgram.data, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.RootedPenaltyProgram.rationalPenalty