TypicalCharacterShells.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite test family covers precisely the needed character shells

abbrev OAI.Ostmann.CharacterShellTestIndex line 11
def OAI.Ostmann.characterShellTests line 13

theorem OAI.Ostmann.eventual_typical_character_shells line 24

Source documentation

Ineligible grid shells are represented by the bulk test. Thus the index set is fixed before L, without asking for mass in empty or unusable shells.

theorem eventual_typical_character_shells
    (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))
    (k : ℕ) (α β 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 Ubulk T₀ : Finset ℕ) (Ulate : ℝ) (u : Fin k × Bool → ℝ)
        (χ : ∀ p : ℕ, DirichletCharacter ℂ p) (center : ∀ p : ℕ, ZMod p) (ζ : ℂ),
      ‖ζ‖ = 1 → (∀ p ∈ P, p.Prime) →
      (∀ p ∈ P, Real.exp (α * L) ≤ Real.log (p : ℝ)) →
      Ubulk ⊆ P → T₀ ⊆ P →
…

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