TypicalCharacterEndpoints.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual tail collision estimate supplies typical character endpoints

def OAI.Ostmann.realTranslatedCharacterTest line 11
theorem OAI.Ostmann.realTranslatedCharacterTest_bound line 15
theorem OAI.Ostmann.realTranslatedCharacterTest_mod line 23

theorem OAI.Ostmann.eventual_typical_character_tests line 31

Source documentation

This is the typical-endpoint step for every prescribed whole shell and bulk interval. The reference mean is a literal average on the fixed tail.

theorem eventual_typical_character_tests {ι : Type*} [DecidableEq ι]
    (hsize : PublishedSummandSizeBound) {C : ℝ} (hM : MertensLowerBound C)
    {A B : Set ℕ} (hA : A.Infinite) (hB : B.Infinite) (h : EventuallyPrimeSumset A B)
    (N : ℕ) (hN : ∀ p, p.Prime → Disjoint (tailResidues A N p) (negTailResidues B N p))
    (J : Finset ι) (α β D δ c : ℝ) (hα : 0 < α) (hδ : 0 < δ) (hc : 0 < c) :
    ∃ a : ℝ, 0 < a ∧ ∃ L₀ t₀ : ℝ, ∀ L T : ℝ, L₀ ≤ L → t₀ ≤ T →
      Real.log T ≤ β * L + D → ∀ X : ℕ, (X : ℝ) = Real.exp T →
      ∀ (P : Finset ℕ) (R : ι → Finset ℕ)
        (χ : ∀ p : ℕ, DirichletCharacter ℂ p) (t : ∀ p : ℕ, ZMod p) (ζ : ℂ),
      ‖ζ‖ = 1 → (∀ j ∈ J, R j ⊆ P) →
      (∀ j ∈ J, ∀ p ∈ R j, p.Prime ∧ (p : ℝ) ≤ Real.exp (T / 4) ∧
        Real.exp (α * L) ≤ Real.log (p : ℝ)) →
…

Mentions: OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.MertensLowerBound, OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues