RegularOrientedSplit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The regularity gain for one oriented change interval

theorem OAI.JointDickman.regular_oriented_split_bound line 16

Source documentation

The manuscript's conditional O_C((Y/B)^alpha/Y) estimate for a recipient at one dyadic scale, in the actual remaining-prime law.

theorem regular_oriented_split_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) (κ : ℝ) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
      ∀ (A D : Finset ℕ) (L i : ℕ) (τ C T : ℝ),
      A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B →
      (∏ p ∈ A, p : ℕ) ≤ Real.exp (κ * B) →
      RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D →
      0 < primeTailEndpoint B i →
      Real.log (auxiliaryCutoff B) ≤ primeTailEndpoint B i →
      primeTailEndpoint B i ≤ 8 * B → 0 < T →
      orientedSplitMass B A D (primeTailEndpoint B i) C T ≤
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.primeTailEndpoint, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.orientedSplitMass

theorem OAI.JointDickman.regular_oriented_scale_sum line 65

Source documentation

All dyadic change intervals together cost O_C(1/B), uniformly in the first coefficient sets satisfying the stated regularity conditions.

theorem regular_oriented_scale_sum
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) (κ : ℝ) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
      ∀ (A D : Finset ℕ) (L : ℕ) (S : Finset ℕ) (τ C T : ℝ),
      A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B →
      (∏ p ∈ A, p : ℕ) ≤ Real.exp (κ * B) →
      RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D →
      (∀ i ∈ S, primeTailEndpoint B i ≤ 8 * B) → 0 < T →
      (∑ i ∈ S, orientedSplitMass B A D (primeTailEndpoint B i) C T) ≤ K * (2 : ℝ)^(4 * C) / B := by
…