OAI/Combinatorics/ContingencyTables/Counting/CompanionStoredSize.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A phase adds a bounded amount to each stored fraction's binary height

  1. lemma OAI.ContingencyTables.CompanionStoredSize.getD_property line 10
  2. def OAI.ContingencyTables.CompanionStoredSize.MatrixHeight line 17
  3. def OAI.ContingencyTables.CompanionStoredSize.StoredHeight line 20
  4. lemma OAI.ContingencyTables.CompanionStoredSize.readEntry_height line 22
  5. lemma OAI.ContingencyTables.CompanionStoredSize.updateMatrix_height line 30
  6. lemma OAI.ContingencyTables.CompanionStoredSize.terms_length line 41
  7. lemma OAI.ContingencyTables.CompanionStoredSize.terms_height line 45
  8. lemma OAI.ContingencyTables.CompanionStoredSize.ratio_height line 57
  9. lemma OAI.ContingencyTables.CompanionStoredSize.next_height line 78

    Source documentation

    This bound is additive in the old stored height; iterating phases therefore preserves a polynomial representation size.

    lemma next_height (z : CompanionPhaseFinishProgram.Input) (M V : ℕ) (hM : 1 ≤ M) (hV : 1 ≤ V)
    (hw : MatrixHeight M z.1.1.2) (he : TreeFraction.height z.1.2 ≤ M)
    (hv : ∀ x∈z.2,TreeFraction.height x.1 ≤ V ∧ TreeFraction.height x.2 ≤ V) :
    StoredHeight (M+(trajectory z).2.length*(2*V+3)+(trajectory z).2.length+5) (next z) := by
…

    Mentions: OAI.ContingencyTables.CompanionPhaseFinishProgram.Input, OAI.ContingencyTables.CompanionStoredSize.MatrixHeight, OAI.ContingencyTables.CompanionStoredSize.StoredHeight