OAI/Combinatorics/ContingencyTables/Machines/PairedDemandProgram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Replacing the oracle demand by the current encoded paired state

Only the retained-cell catalog and the supplied state are scanned. The large cells receive zero in each sparse view and hence retain their full capacity in the complemented column demand.

  1. abbrev OAI.ContingencyTables.PairedDemandProgram.Input line 19
  2. def OAI.ContingencyTables.PairedDemandProgram.cellInput line 21
  3. def OAI.ContingencyTables.PairedDemandProgram.cellInputRealizer line 23
  4. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_cellInput line 25
  5. def OAI.ContingencyTables.PairedDemandProgram.cells line 30
  6. def OAI.ContingencyTables.PairedDemandProgram.cellsRealizer line 31
  7. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_cells line 34
  8. def OAI.ContingencyTables.PairedDemandProgram.counts line 38
  9. def OAI.ContingencyTables.PairedDemandProgram.countsRealizer line 40
  10. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_counts line 46
  11. def OAI.ContingencyTables.PairedDemandProgram.sideEntry line 51
  12. def OAI.ContingencyTables.PairedDemandProgram.sideEntryRealizer line 52
  13. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_sideEntry line 54
  14. def OAI.ContingencyTables.PairedDemandProgram.values line 59
  15. def OAI.ContingencyTables.PairedDemandProgram.valuesRealizer line 60
  16. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_values line 65
  17. def OAI.ContingencyTables.PairedDemandProgram.viewInput line 70
  18. def OAI.ContingencyTables.PairedDemandProgram.viewInputRealizer line 72
  19. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_viewInput line 78
  20. def OAI.ContingencyTables.PairedDemandProgram.viewMatrix line 87
  21. def OAI.ContingencyTables.PairedDemandProgram.viewMatrixRealizer line 88
  22. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_viewMatrix line 91
  23. def OAI.ContingencyTables.PairedDemandProgram.complement line 94
  24. def OAI.ContingencyTables.PairedDemandProgram.complementRealizer line 96
  25. lemma OAI.ContingencyTables.PairedDemandProgram.polynomial_complement line 102
  26. def OAI.ContingencyTables.PairedDemandProgram.output line 109
  27. def OAI.ContingencyTables.PairedDemandProgram.outputRealizer line 111
  28. theorem OAI.ContingencyTables.PairedDemandProgram.polynomial_output line 116
  29. lemma OAI.ContingencyTables.PairedDemandProgram.cells_data line 130
  30. lemma OAI.ContingencyTables.PairedDemandProgram.catalog_eq line 133
  31. lemma OAI.ContingencyTables.PairedDemandProgram.values_data line 150
  32. lemma OAI.ContingencyTables.PairedDemandProgram.viewMatrix_data line 164
  33. theorem OAI.ContingencyTables.PairedDemandProgram.output_data line 190

    Source documentation

    The current code replaces both demand arrays; the old demand only provides the immutable graph, capacities, margins and baseline.

    theorem output_data (x q : Fin m → Fin n → ℕ) (S : Set (Labels A × Bool)) :
    output (RootedDemandProgram.data A x q,
      encodeSet (CompanionComputedInitial.coordinateOrder A) S)=
        RootedDemandProgram.data A
          (ForestCountIdentification.smallX A.small (CompanionWeightOracle.profile A S))
          (fun i j => A.b i j-
            ForestCountIdentification.smallY A.small (CompanionWeightOracle.profile A S) i j) := by
…

    Mentions: OAI.ContingencyTables.PairedDemandProgram.output, OAI.ContingencyTables.RootedDemandProgram.data, OAI.ContingencyTables.CompanionComputedInitial.coordinateOrder, OAI.ContingencyTables.ForestCountIdentification.smallX, OAI.ContingencyTables.CompanionWeightOracle.profile, OAI.ContingencyTables.ForestCountIdentification.smallY