OAI/NumberTheory/Ostmann/Characters/CharacterInitialProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.characterFillerTarget line 11
2. theorem OAI.Ostmann.character_log_center_sum line 15
3. theorem OAI.Ostmann.character_initial_center line 24
4. theorem OAI.Ostmann.character_initial_product_window line 34

   Source documentation

   Per-atom interval errors remain bounded after taking all positive and conjugate copies, independent of the number of primes in the word.

   theorem character_initial_product_window (k : ℕ) (logX Δ J c : ℝ)
       (T : Fin k → ℝ) (a : Fin k → Bool → ℝ)
       (lo hi : CharacterRole k → ℕ)
       (hlo : ∀ v, Real.exp (characterLogCenter J T a
         (characterFillerTarget logX Δ J T a) v - c) ≤ lo v)
       (hhi : ∀ v, (hi v : ℝ) ≤ Real.exp (characterLogCenter J T a
         (characterFillerTarget logX Δ J T a) v + c))
       (x : CopyScheduleAtoms (characterRole k) 0 → ℕ)
       (hx : ∀ r ∈ atomIntervalRanges (characterRole k) lo hi 0, r.Holds x) :
       let C := (Fintype.card (CharacterRole k) : ℝ) * c
   …

   Mentions: OAI.Ostmann.CharacterRole, OAI.Ostmann.characterLogCenter, OAI.Ostmann.characterFillerTarget, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.characterRole, OAI.Ostmann.atomIntervalRanges