RetainedKernelPrimeBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The retained prime lower bound for actual signed squarefree kernels

theorem OAI.Ostmann.retained_signed_kernel_prime_lower line 15

Source documentation

The primitive character is constructed from d. The only remaining analytic hypotheses are the cited published zero inputs; the Page-retention condition says precisely which already-selected exception is allowed.

theorem retained_signed_kernel_prime_lower (P : PublishedProgressionInput)
    (H : PublishedRealZeroInput P) (hSiegel : PublishedSiegelBound)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ A K : ℝ, 0 < A ∧ 0 < K ∧
      ∀ 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 : ℕ) (R s : ℝ), 2 ≤ Q → 4 * d.natAbs ≤ Q → 0 ≤ R →
            2 * (A + H.errorConstant) ≤ Real.log (4 * (Q : ℝ)) →
            1 < s → s ≤ 1 + 1 / Real.log (4 * (Q : ℝ)) →
…

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