RetainedSplitPrimeMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative split-prime mass for a retained signed squarefree kernel

theorem OAI.Ostmann.retained_split_prime_mass line 14

Source documentation

Every term of the lower bound is derived: the main pole, the actual character zero sum, the prime tail, and the excluded-divisor weight.

theorem retained_split_prime_mass (P : PublishedProgressionInput)
    (H : PublishedRealZeroInput P) (hSiegel : PublishedSiegelBound)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ A K C : ℝ, 0 < A ∧ 0 < K ∧ 0 < C ∧
      ∀ d : ℤ, Squarefree d.natAbs → 2 < d.natAbs →
        ∃ (χ : PrimitiveRealCharacter) (N : ℕ),
          1 < N ∧ N ∣ χ.modulus ∧ χ.modulus ≤ 8 * N ∧
          (d.natAbs = N ∨ d.natAbs = 2 * N) ∧
          χ.modulus ≤ 4 * d.natAbs ∧ d.natAbs ≤ 2 * χ.modulus ∧
          ∀ (Q₀ Q D Y : ℕ) (R s : ℝ),
            2 ≤ Q₀ → 4 * d.natAbs ≤ Q₀ → 0 < Q → 0 < D → 0 < Y →
            d.natAbs ∣ D → 0 ≤ R →
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PrimitiveRealCharacter