OAI/Combinatorics/ContingencyTables/Rooted/RootedDemandProgram.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Computing the root-demand input from the actual cell arrays

The two natural entries at a vertex encode its signed small-cell discrepancy. They are formed by rectangular scans and then passed to the component/root program.

  1. abbrev OAI.ContingencyTables.RootedDemandProgram.Input line 19
  2. abbrev OAI.ContingencyTables.RootedDemandProgram.TermInput line 20
  3. def OAI.ContingencyTables.RootedDemandProgram.values line 22
  4. def OAI.ContingencyTables.RootedDemandProgram.valuesRealizer line 24
  5. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_values line 31
  6. def OAI.ContingencyTables.RootedDemandProgram.retainedTest line 43
  7. def OAI.ContingencyTables.RootedDemandProgram.retainedTestRealizer line 45
  8. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_retainedTest line 48
  9. def OAI.ContingencyTables.RootedDemandProgram.rowTest line 53
  10. def OAI.ContingencyTables.RootedDemandProgram.rowTestRealizer line 54
  11. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_rowTest line 56
  12. def OAI.ContingencyTables.RootedDemandProgram.columnTest line 60
  13. def OAI.ContingencyTables.RootedDemandProgram.columnTestRealizer line 62
  14. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_columnTest line 67
  15. def OAI.ContingencyTables.RootedDemandProgram.rowPair line 76
  16. def OAI.ContingencyTables.RootedDemandProgram.rowPairRealizer line 77
  17. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_rowPair line 83
  18. def OAI.ContingencyTables.RootedDemandProgram.columnPair line 88
  19. def OAI.ContingencyTables.RootedDemandProgram.columnPairRealizer line 89
  20. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_columnPair line 95
  21. def OAI.ContingencyTables.RootedDemandProgram.term line 100
  22. def OAI.ContingencyTables.RootedDemandProgram.termRealizer line 105
  23. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_term line 110
  24. def OAI.ContingencyTables.RootedDemandProgram.demand line 117
  25. def OAI.ContingencyTables.RootedDemandProgram.demandRealizer line 119
  26. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_demand line 123
  27. def OAI.ContingencyTables.RootedDemandProgram.vertexCount line 129
  28. def OAI.ContingencyTables.RootedDemandProgram.vertexCountRealizer line 130
  29. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_vertexCount line 134
  30. def OAI.ContingencyTables.RootedDemandProgram.vertices line 143
  31. def OAI.ContingencyTables.RootedDemandProgram.verticesRealizer line 144
  32. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_vertices line 145
  33. def OAI.ContingencyTables.RootedDemandProgram.demandList line 155
  34. def OAI.ContingencyTables.RootedDemandProgram.demandListRealizer line 156
  35. lemma OAI.ContingencyTables.RootedDemandProgram.polynomial_demandList line 158
  36. def OAI.ContingencyTables.RootedDemandProgram.rootCount line 162
  37. def OAI.ContingencyTables.RootedDemandProgram.rootCountRealizer line 163
  38. theorem OAI.ContingencyTables.RootedDemandProgram.polynomial_rootCount line 166
  39. def OAI.ContingencyTables.RootedDemandProgram.data line 174
  40. lemma OAI.ContingencyTables.RootedDemandProgram.values_data line 179
  41. lemma OAI.ContingencyTables.RootedDemandProgram.retainedTest_data line 185
  42. lemma OAI.ContingencyTables.RootedDemandProgram.rowTest_data line 194
  43. lemma OAI.ContingencyTables.RootedDemandProgram.columnTest_data line 207
  44. def OAI.ContingencyTables.RootedDemandProgram.contribution line 222
  45. lemma OAI.ContingencyTables.RootedDemandProgram.term_data line 229
  46. lemma OAI.ContingencyTables.RootedDemandProgram.contribution_sum line 239
  47. lemma OAI.ContingencyTables.RootedDemandProgram.demand_data line 262
  48. lemma OAI.ContingencyTables.RootedDemandProgram.demandList_data line 279
  49. theorem OAI.ContingencyTables.RootedDemandProgram.rootCount_data line 291

    Source documentation

    The actual binary root program has exactly the selected-root penalty value; no signed-demand representation assumption is supplied.

    theorem rootCount_data {m n : ℕ} (A : Instance (Fin m) (Fin n))
    (x q : Fin m → Fin n → ℕ) :
    rootCount (data A x q)=RootedPenaltyProgram.rootCount A (rowColumn A.T)
      (fun i j => (x i j:ℤ)) (fun i j => (q i j:ℤ)) := by
…

    Mentions: OAI.ContingencyTables.RootedDemandProgram.rootCount, OAI.ContingencyTables.RootedDemandProgram.data, OAI.ContingencyTables.RootedPenaltyProgram.rootCount