OAI/NumberTheory/Ostmann/Construction/TailGiantBlockSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.tail_giant_of_favorable_block line 13

   Source documentation

   The favorable set affects only the test. The chosen prior contains every prime of the complete selected cell, and its lower mean is absolute.

   theorem tail_giant_of_favorable_block {A B : Set ℕ}
       (hA : A.Infinite) (hB : B.Infinite) (N : ℕ)
       (F E D : Finset ℕ) (ν : ℕ → ℝ) (lo h γ c B₀ C : ℝ)
       (hM : MertensEstimate C) (hlo : 5 ≤ lo) (hh : 0 < h)
       (hγ : 0 < γ) (hc : 0 < c) (hB0 : 0 ≤ B₀)
       (hwidth : 8 + Real.log 2 + 2 * C ≤ h)
       (hupper : lo + h ≤ 2 * (lo - 4))
       (hdisjoint : ∀ p ∈ smoothGiantPrimeRange (lo + h + 2),
         Disjoint (tailResidues A N p) (negTailResidues B N p))
       (hF : ∀ p ∈ F, p.Prime ∧ lo ≤ Real.log p ∧ Real.log p ≤ lo + h)
       (hFbal : ∀ p ∈ F, ((tailSupport A N p).card : ℝ) ≤ 2 * p / 3)
       (hFγ : ∀ p (hp : p ∈ F), let _ : Fact p.Prime := ⟨(hF p hp).1⟩;
   …

   Mentions: OAI.Ostmann.MertensEstimate, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.tailSupport