OAI/NumberTheory/JointDickman/Arithmetic/NumericPrefixHarmonic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.numericAdditionSieveCutoff line 12
2. theorem OAI.JointDickman.numeric_prefix_harmonic_bound line 17

   Source documentation

   The prime cutoff and the Euler-product estimate are instantiated; only the concrete progression geometry is left for an application.

   theorem numeric_prefix_harmonic_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {κ g ε : ℝ} (hκ : 0 < κ) (hg : 0 < g) (hg1 : g < 1) (hε : 0 < ε) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ (E : Finset ℕ) (a b c d : ℤ) (q W : ℝ) (u v : ℕ),
           E ⊆ auxiliaryPrimes B → (∏ p ∈ E, p : ℕ) ≤ Real.exp (κ*B) →
           0 ≤ q → q ≤ 1 → 0 < W → u ≤ v →
           (∀ p ∈ primePrefix B g (auxiliaryPrimes B) \ E,
             (b : ZMod p) ≠ 0 ∧ (d : ZMod p) ≠ 0 ∧ (a : ZMod p)*d-c*b ≠ 0) →
           (∀ n ∈ Ico u v, W ≤ (a : ℝ)+(b : ℝ)*n) →
           (∑ n ∈ Ico u v, (∏ p ∈ primePrefix B g (auxiliaryPrimes B) \ E,
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primePrefix