OAI/Combinatorics/ContingencyTables/Machines/EnumerationPointBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Individual enumeration points have polynomial binary size

  1. lemma OAI.ContingencyTables.ProfilePrograms.gridCoordinates_weight line 11
  2. lemma OAI.ContingencyTables.ProfilePrograms.gridWords_point_weight line 18
  3. lemma OAI.ContingencyTables.ProfilePrograms.splitViews_weight line 25
  4. lemma OAI.ContingencyTables.ProfilePrograms.profileBoxViews_length line 31
  5. lemma OAI.ContingencyTables.ProfilePrograms.profileBoxViews_point_weight line 35
  6. theorem OAI.ContingencyTables.ProfilePrograms.profileBoxViews_point_polynomial line 50

    Source documentation

    Exponentially many enumerated points do not make any one point's binary representation exponentially large.

    theorem profileBoxViews_point_polynomial : ∃ p : Polynomial ℕ,
    ∀ z v,v∈profileBoxViews z → weight v ≤ p.eval (weight z) := by
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.profileBoxViews