OAI/Combinatorics/ContingencyTables/Sampling/ProfileVectorMeasureBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the executed nested trial-vector loops

  1. lemma OAI.ContingencyTables.ProfilePrograms.terminalColumnMeasure_le line 12
  2. lemma OAI.ContingencyTables.ProfilePrograms.unit_terminalColumnMeasure_le line 45
  3. lemma OAI.ContingencyTables.ProfilePrograms.unit_outerVectorMeasure_le line 55
  4. def OAI.ContingencyTables.ProfilePrograms.vectorMeasurePolynomial line 73
  5. theorem OAI.ContingencyTables.ProfilePrograms.outerVectorMeasure_bound line 78