OAI/NumberTheory/Ostmann/Characters/AllCharacterDecorrelation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.tailCharacterBias line 12
2. def OAI.Ostmann.tailCharacterBandMass line 15
3. theorem OAI.Ostmann.closedLogLogPrimeBand_eq_iterated line 18
4. theorem OAI.Ostmann.tailCharacterBandMass_eq line 23
5. theorem OAI.Ostmann.tailCharacterBias_nonneg line 30
6. theorem OAI.Ostmann.PublishedProgressionInput.all_character_decorrelation line 33
7. theorem OAI.Ostmann.eventual_bad_tail_character_mass line 47

   Source documentation

   Markov's bound is uniform in subsets of the whole closed band.

   theorem eventual_bad_tail_character_mass (A : Set ℕ) (N : ℕ) (α β δ ε : ℝ)
       (hδ : 0 < δ) (hε : 0 < ε)
       (hsmall : (fun L => tailCharacterBandMass A N α β L) =o[atTop] (fun L : ℝ => L)) :
       ∀ᶠ L : ℝ in atTop, ∀ P : Finset ℕ, P ⊆ closedLogLogPrimeBand α β L →
         (∑ p ∈ P.filter (fun p => δ < tailCharacterBias A N p), (p : ℝ)⁻¹) ≤ ε * L := by
   …

   Mentions: OAI.Ostmann.tailCharacterBandMass, OAI.Ostmann.closedLogLogPrimeBand, OAI.Ostmann.tailCharacterBias