OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseSize.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Phase query sizes do not depend on the heights of old multipliers

  1. lemma OAI.ContingencyTables.CompanionPhaseSize.list_weight_bound line 11
  2. lemma OAI.ContingencyTables.CompanionPhaseSize.initialInput_bound line 16
  3. lemma OAI.ContingencyTables.CompanionPhaseSize.start_bound line 25
  4. lemma OAI.ContingencyTables.CompanionPhaseSize.config_bound line 39
  5. lemma OAI.ContingencyTables.CompanionPhaseSize.trajectory_bounds line 70
  6. lemma OAI.ContingencyTables.CompanionPhaseSize.query_bound line 102
  7. lemma OAI.ContingencyTables.CompanionPhaseSize.phase_bounds line 141

    Source documentation

    A uniform additive increment and dimension bound for an entire phase. The polynomial depends only on immutable data, word length and phase number.

    lemma phase_bounds : ∃ p : Polynomial ℕ,∀ (z : Input) (S M R : ℕ),
    weight z.1.1.1 ≤ S → weight z.2 ≤ S → (history z).length ≤ S → 1 ≤ M →
    StoredHeight M (old z) → StoredShape R (old z) → p.eval S ≤ R →
      StoredHeight (M+p.eval S) (output z) ∧ StoredShape R (output z) := by
…