QuadraticSplitSupply.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform split-prime supply outside the explicit exceptional family

theorem OAI.Ostmann.quadratic_split_supply line 13

Source documentation

All analytic error conditions are discharged by fixed constants and explicit integer cutoffs. Here L=log X, and the Page threshold is L^100.

theorem quadratic_split_supply (P : PublishedProgressionInput)
    (H : PublishedRealZeroInput P) (hSiegel : PublishedSiegelBound) :
    ∃ η L₀ : ℝ, 0 < η ∧ η ≤ 1 / 1000 ∧ 0 < L₀ ∧
      ∀ L : ℝ, L₀ ≤ L → ∀ (d : ℤ) (D : ℕ),
        Squarefree d.natAbs → d ≠ 0 →
        (d.natAbs : ℝ) ≤ Real.exp (2 * η * L) →
        0 < D → d.natAbs ∣ D → Real.log D ≤ L →
        d ∉ pageKernelExclusion P (kernelConductorCutoff η L) (L ^ (100 : ℕ)) →
        (3 / 100 : ℝ) * L ≤
          ∑ p ∈ (Nat.primesLE (kernelSplitCutoff η L)).filter
            (fun p => ¬p ∣ D ∧ jacobiSym d p = 1), Real.log p / (p : ℝ) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.pageKernelExclusion, OAI.Ostmann.kernelConductorCutoff, OAI.Ostmann.kernelSplitCutoff