OAI/NumberTheory/Ostmann/Construction/ConstituentRangeCounts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.expandedRootRanges_count_le line 13

   Source documentation

   The added root cutoff costs one test; all inherited tests are counted on their actual binary history tree.

   theorem expandedRootRanges_count_le {I σ : Type*}
       (role : I → CopyScheduleRole) (n K : ℕ)
       (words : CopyScheduleAtoms role n → List σ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (hK : ∀ j ≤ n, (ranges j).length ≤ K) :
       (expandedRootRanges role n words ranges).count ≤ K * (2 ^ (n + 1) - 1) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.expandedRootRanges

2. theorem OAI.Ostmann.expandedRootRanges_cutoff_count_le line 22
3. theorem OAI.Ostmann.expandedRootRanges_pair_linear_count line 35

   Source documentation

   Both histories, with the extra cutoff on the left, share one constant range-count bound and hence the linear bound used in the numerical estimate.

   theorem expandedRootRanges_pair_linear_count {I σ : Type*}
       (role : I → CopyScheduleRole) (n K : ℕ)
       (words words' : CopyScheduleAtoms role n → List σ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (hK : ∀ j ≤ n, (ranges j).length ≤ K)
       (r : WordRange (ExpandedScheduledVariable σ n)) (m : ℝ) (hm : 0 ≤ m) :
       (((expandedRootRanges role n words ranges).prependRoot r).count : ℝ) ≤
         (K * (2 ^ (n + 1) - 1) + 1 : ℕ) * (1 + m) ∧
       ((expandedRootRanges role n words' ranges).count : ℝ) ≤
         (K * (2 ^ (n + 1) - 1) + 1 : ℕ) * (1 + m) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.WordRange, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.expandedRootRanges

4. theorem OAI.Ostmann.constituent_word_budget_linear line 57

   Source documentation

   With linear atom sizes, the concrete word budget stays linear.

   theorem constituent_word_budget_linear {I : Type*} [Fintype I]
       (n A S : ℕ) (s m : ℝ) (hs : (S : ℝ) ≤ s * (1 + m)) (hm : 0 ≤ m) :
       ((2 * 3 ^ n * Fintype.card I * S + A * S + 4 : ℕ) : ℝ) ≤
         (((2 * 3 ^ n * Fintype.card I + A : ℕ) : ℝ) * s + 4) * (1 + m) := by
   …