OAI/Combinatorics/ContingencyTables/Counting/CountingPositiveWordLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Flattening the positive run while preserving its complete output law

  1. def OAI.ContingencyTables.CountingPositiveProgram.independentOutput line 12
  2. theorem OAI.ContingencyTables.CountingPositiveProgram.output_sameLaw line 18
  3. theorem OAI.ContingencyTables.CountingPositiveProgram.value_sameLaw line 33