EventualTailGiant.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The initial giant for the actual large summand tails

theorem OAI.Ostmann.EventuallyPrimeSumset.eventual_giant_from_favorable_blocks line 16

Source documentation

Only the favorable block supply remains as a combinatorial input here. The endpoint law, collision budget, block margins and normalizer are all constructed from the actual summands and the cited published inputs.

theorem EventuallyPrimeSumset.eventual_giant_from_favorable_blocks
    (P0 : PublishedProgressionInput) (hsize : PublishedSummandSizeBound)
    {A B : Set ℕ} (h : EventuallyPrimeSumset A B) (hA : A.Infinite) (hB : B.Infinite)
    (N : ℕ) (hN : ∀ p, p.Prime → Disjoint (tailResidues A N p) (negTailResidues B N p))
    (C γ c : ℝ) (hM : MertensEstimate C) (hγ : 0 < γ) (hc : 0 < c) :
    ∃ a : ℝ, 0 < a ∧ ∀ᶠ L : ℝ in atTop,
      ∀ X : ℝ, Real.exp ((4 / 100 : ℝ) * L) ≤ X → X ≤ Real.exp L →
      ∀ hi : ℕ, (hi : ℝ) = Real.exp X →
      ∀ lo : ℝ, Real.exp ((5 / 100 : ℝ) * L) ≤ lo → lo ≤ Real.exp ((9 / 10 : ℝ) * L) →
      ⌈Real.exp (lo + 10 * Real.exp ((1 / 100 : ℝ) * L) + 3)⌉₊ ≤ tailCollisionCutoff X →
      ∀ (F : Finset ℕ) (hF : ∀ p ∈ F, p.Prime ∧ lo ≤ Real.log p ∧
        Real.log p ≤ lo + 10 * Real.exp ((1 / 100 : ℝ) * L)),
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.MertensEstimate, OAI.Ostmann.tailCollisionCutoff