OAI/Combinatorics/ContingencyTables/Counting/CountingDirectLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact law of the executed direct counting estimator

  1. def OAI.ContingencyTables.CountingDirectProgram.modelContext line 15
  2. def OAI.ContingencyTables.CountingDirectProgram.modelWidth line 26
  3. def OAI.ContingencyTables.CountingDirectProgram.modelValue line 31
  4. lemma OAI.ContingencyTables.CountingDirectProgram.modelWidth_eq line 44
  5. def OAI.ContingencyTables.CountingDirectProgram.referenceBits line 53
  6. def OAI.ContingencyTables.CountingDirectProgram.reference line 60
  7. lemma OAI.ContingencyTables.CountingDirectProgram.native_sameLaw line 74
  8. lemma OAI.ContingencyTables.CountingDirectProgram.reference_sameLaw line 100
  9. lemma OAI.ContingencyTables.CountingDirectProgram.model_sameLaw line 110
  10. lemma OAI.ContingencyTables.CountingDirectProgram.output_model line 120
  11. lemma OAI.ContingencyTables.CountingDirectProgram.sameLaw line 145