OAI/Combinatorics/ContingencyTables/Rooted/RootedOffsetProgram.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Computing the forest affine offset from the stored cell values

Every summand uses the executed cut flags and coefficient. The input contains the baseline and the two stored views, rather than an affine offset supplied by an oracle.

  1. abbrev OAI.ContingencyTables.RootedOffsetProgram.WeightedInput line 17
  2. abbrev OAI.ContingencyTables.RootedOffsetProgram.Entry line 18
  3. abbrev OAI.ContingencyTables.RootedOffsetProgram.Input line 19
  4. def OAI.ContingencyTables.RootedOffsetProgram.weightedDifference line 21
  5. def OAI.ContingencyTables.RootedOffsetProgram.weightedDifferenceRealizer line 24
  6. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_weightedDifference line 31
  7. lemma OAI.ContingencyTables.RootedOffsetProgram.value_weightedDifference line 43
  8. lemma OAI.ContingencyTables.RootedOffsetProgram.value_parts line 48
  9. def OAI.ContingencyTables.RootedOffsetProgram.cellInput line 51
  10. def OAI.ContingencyTables.RootedOffsetProgram.cellInputRealizer line 52
  11. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_cellInput line 53
  12. def OAI.ContingencyTables.RootedOffsetProgram.shifted line 56
  13. def OAI.ContingencyTables.RootedOffsetProgram.shiftedRealizer line 58
  14. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_shifted line 64
  15. def OAI.ContingencyTables.RootedOffsetProgram.cutTerm line 73
  16. def OAI.ContingencyTables.RootedOffsetProgram.cutTermRealizer line 75
  17. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_cutTerm line 78
  18. def OAI.ContingencyTables.RootedOffsetProgram.smallTest line 83
  19. def OAI.ContingencyTables.RootedOffsetProgram.smallTestRealizer line 84
  20. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_smallTest line 86
  21. def OAI.ContingencyTables.RootedOffsetProgram.smallTerm line 91
  22. def OAI.ContingencyTables.RootedOffsetProgram.smallTermRealizer line 92
  23. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_smallTerm line 94
  24. def OAI.ContingencyTables.RootedOffsetProgram.summand line 97
  25. def OAI.ContingencyTables.RootedOffsetProgram.summandRealizer line 100
  26. lemma OAI.ContingencyTables.RootedOffsetProgram.polynomial_summand line 107
  27. def OAI.ContingencyTables.RootedOffsetProgram.offset line 117
  28. def OAI.ContingencyTables.RootedOffsetProgram.offsetRealizer line 119
  29. theorem OAI.ContingencyTables.RootedOffsetProgram.polynomial_offset line 125
  30. lemma OAI.ContingencyTables.RootedOffsetProgram.value_offset line 131
  31. def OAI.ContingencyTables.RootedOffsetProgram.entry line 138
  32. lemma OAI.ContingencyTables.RootedOffsetProgram.smallTest_entry line 145
  33. lemma OAI.ContingencyTables.RootedOffsetProgram.cutTerm_entry line 153
  34. lemma OAI.ContingencyTables.RootedOffsetProgram.summand_entry line 168
  35. def OAI.ContingencyTables.RootedOffsetProgram.data line 193
  36. theorem OAI.ContingencyTables.RootedOffsetProgram.offset_data line 200

    Source documentation

    The executed normalized pair is the exact manuscript affine offset.

    theorem offset_data {m n N : ℕ} (A : Instance (Fin m) (Fin n))
    (t : GraphCompletionCounts.TreeCell A.T) (x q : Fin m → Fin n → ℤ)
    (e : Fin N ≃ Fin m×Fin n) :
    offset (data A t x q e)=ForestAffineProgram.signedParts
      (RootedIntegerEvaluation.offset A (rowColumn A.T) t x q) := by
…

    Mentions: OAI.ContingencyTables.GraphCompletionCounts.TreeCell, OAI.ContingencyTables.RootedOffsetProgram.offset, OAI.ContingencyTables.RootedOffsetProgram.data, OAI.ContingencyTables.ForestAffineProgram.signedParts, OAI.ContingencyTables.RootedIntegerEvaluation.offset