OAI/Combinatorics/ContingencyTables/Sampling/PaddedEnumerationBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Enumeration bounds uniform over all proposed small profiles

  1. lemma OAI.ContingencyTables.ProfilePrograms.list_getD_le_sum line 11
  2. lemma OAI.ContingencyTables.ProfilePrograms.list_sum_le_length_mul line 21
  3. lemma OAI.ContingencyTables.ProfilePrograms.largeCount_le_length line 31
  4. lemma OAI.ContingencyTables.ProfilePrograms.paddedMarginAt_le line 43

    Source documentation

    Rejected profiles can decrease residual margins but cannot enlarge them beyond the original margin and its deterministic padding.

    lemma paddedMarginAt_le (row : Bool) (z : PaddingData) (i : ℕ) :
    paddedMarginAt row (z,i) ≤
      (marginList row z.1).sum+(marginList (!row) z.1).length*z.2 := by
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.PaddingData, OAI.ContingencyTables.ProfilePrograms.paddedMarginAt, OAI.ContingencyTables.ProfilePrograms.marginList

  5. lemma OAI.ContingencyTables.ProfilePrograms.largePaddedMargins_length line 56
  6. lemma OAI.ContingencyTables.ProfilePrograms.largePaddedMargins_entry line 61
  7. lemma OAI.ContingencyTables.ProfilePrograms.largePaddedMargins_sum line 68