OAI/NumberTheory/Ostmann/Construction/SelectedFinalPairDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_selected_final_pair_decay line 19

   Source documentation

   All distinct final parity arrangements satisfy the original-prior pair estimate. The one-sided character, word sizes, range counts and common modulus are derived from the actual schedule; only the explicit physical prime and frequency ranges remain.

   theorem eventual_selected_final_pair_decay {I : Type u} [Fintype I]
       (role : I → CopyScheduleRole) (n Aw Kr : ℕ) (s C S H z α β γ c : ℝ)
       (hs : 0 ≤ s) (hC : 0 ≤ C) (hS : 1 ≤ S) (hH : 0 ≤ H) (hz : 0 ≤ z)
       (hα : 0 < α) (hαβ : α < β) (hγβ : γ < β) (hc : 0 < c) :
       ∀ᶠ L : ℝ in atTop,
       ∀ (size : I → ℕ) (Smax : ℕ) (_hSmax : 1 ≤ Smax) (_hsize : ∀ i, size i ≤ Smax)
         (M : ℝ) (_hm : 0 ≤ M) (_hmL : M ≤ z * L) (_hSm : (Smax : ℝ) ≤ s * (1 + M))
         (χ : (Σ i, Fin (size i)) → ∀ p : ℕ, DirichletCharacter ℂ p)
         (κ : (Σ i, Fin (size i)) → ℕ → ℂ) (_hκ : ∀ i p, ‖κ i p‖ ≤ 1)
         (pivot : ℕ → (Σ i, Fin (size i)))
         (childBound pivotBound : ℕ → ℕ)
         (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
   …

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