OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorMedianProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Executing independent complete estimators and their rational median

  1. abbrev OAI.ContingencyTables.RootedEstimatorMedianProgram.Input line 13
  2. def OAI.ContingencyTables.RootedEstimatorMedianProgram.words line 15
  3. def OAI.ContingencyTables.RootedEstimatorMedianProgram.wordsRealizer line 17
  4. lemma OAI.ContingencyTables.RootedEstimatorMedianProgram.polynomial_words line 25
  5. def OAI.ContingencyTables.RootedEstimatorMedianProgram.sample line 34
  6. def OAI.ContingencyTables.RootedEstimatorMedianProgram.sampleRealizer line 36
  7. lemma OAI.ContingencyTables.RootedEstimatorMedianProgram.polynomial_sample line 42
  8. def OAI.ContingencyTables.RootedEstimatorMedianProgram.samples line 49
  9. def OAI.ContingencyTables.RootedEstimatorMedianProgram.samplesRealizer line 50
  10. lemma OAI.ContingencyTables.RootedEstimatorMedianProgram.polynomial_samples line 52
  11. def OAI.ContingencyTables.RootedEstimatorMedianProgram.output line 58
  12. def OAI.ContingencyTables.RootedEstimatorMedianProgram.outputRealizer line 59
  13. theorem OAI.ContingencyTables.RootedEstimatorMedianProgram.polynomial_output line 62
  14. theorem OAI.ContingencyTables.RootedEstimatorMedianProgram.output_ofFn line 68