OAI/Combinatorics/ContingencyTables/Rooted/RootedLabelWeightProgram.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

The executed weight oracle at a current paired state

The immutable schedule and graph are shared. Each call reconstructs the two small-cell views from its actual state, runs the independent median estimator, and multiplies by the exact factorial ratio.

  1. abbrev OAI.ContingencyTables.RootedLabelWeightProgram.Config line 20
  2. abbrev OAI.ContingencyTables.RootedLabelWeightProgram.Input line 21
  3. def OAI.ContingencyTables.RootedLabelWeightProgram.replaceState line 23
  4. def OAI.ContingencyTables.RootedLabelWeightProgram.replaceStateRealizer line 25
  5. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_replaceState line 37
  6. def OAI.ContingencyTables.RootedLabelWeightProgram.stateInput line 51
  7. def OAI.ContingencyTables.RootedLabelWeightProgram.stateInputRealizer line 53
  8. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_stateInput line 56
  9. def OAI.ContingencyTables.RootedLabelWeightProgram.context line 62
  10. def OAI.ContingencyTables.RootedLabelWeightProgram.contextRealizer line 64
  11. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_context line 67
  12. def OAI.ContingencyTables.RootedLabelWeightProgram.medianInput line 72
  13. def OAI.ContingencyTables.RootedLabelWeightProgram.medianInputRealizer line 74
  14. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_medianInput line 77
  15. def OAI.ContingencyTables.RootedLabelWeightProgram.demandInput line 83
  16. def OAI.ContingencyTables.RootedLabelWeightProgram.demandInputRealizer line 85
  17. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_demandInput line 90
  18. def OAI.ContingencyTables.RootedLabelWeightProgram.factorialInput line 96
  19. def OAI.ContingencyTables.RootedLabelWeightProgram.factorialInputRealizer line 98
  20. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_factorialInput line 104
  21. def OAI.ContingencyTables.RootedLabelWeightProgram.medianResult line 111
  22. def OAI.ContingencyTables.RootedLabelWeightProgram.medianResultRealizer line 112
  23. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_medianResult line 115
  24. def OAI.ContingencyTables.RootedLabelWeightProgram.factorialResult line 118
  25. def OAI.ContingencyTables.RootedLabelWeightProgram.factorialResultRealizer line 119
  26. lemma OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_factorialResult line 122
  27. def OAI.ContingencyTables.RootedLabelWeightProgram.output line 127
  28. def OAI.ContingencyTables.RootedLabelWeightProgram.outputRealizer line 128
  29. theorem OAI.ContingencyTables.RootedLabelWeightProgram.polynomial_output line 131
  30. def OAI.ContingencyTables.RootedLabelWeightProgram.config line 140
  31. lemma OAI.ContingencyTables.RootedLabelWeightProgram.replaceState_data line 145
  32. lemma OAI.ContingencyTables.RootedLabelWeightProgram.context_data line 153
  33. lemma OAI.ContingencyTables.RootedLabelWeightProgram.output_value line 163
  34. theorem OAI.ContingencyTables.RootedLabelWeightProgram.sameLaw_weight line 189