OAI/NumberTheory/Ostmann/Construction/ConstituentPairComplexity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Concrete word and support counts for the actual two histories

  1. theorem OAI.Ostmann.WordTransferTemplate.wordsBounded_mono line 12
  2. theorem OAI.Ostmann.constituent_pair_word_bounds line 25

    Source documentation

    One linear word budget covers both exact templates, all inherited units, and every supplied range involving at most A current atoms.

    theorem constituent_pair_word_bounds
    (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
    (S A : ℕ) (hS : 1 ≤ S) (hsize : ∀ i, size i ≤ S)
    (hA : ∀ j ≤ n, ∀ r ∈ ranges j, r.atoms.length ≤ A) :
    let B := 2 * 3 ^ n * Fintype.card I * S + A * S + 4
…

    Mentions: OAI.Ostmann.ScheduleAtomRange

  3. theorem OAI.Ostmann.constituent_pair_prime_count line 55
  4. theorem OAI.Ostmann.constituent_pair_top_count line 65