OAI/Combinatorics/ContingencyTables/Counting/CountingAdaptiveReserve.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The initializer uses only the length of its reserved word

  1. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.zeroCode_eq_of_length_eq line 9
  2. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.initialInput_eq_of_length_eq line 13
  3. theorem OAI.ContingencyTables.CountingAdaptiveInputProgram.output_eq_of_length_eq line 20
  4. theorem OAI.ContingencyTables.CountingAdaptiveInputProgram.output_ofFn line 27