FirstOrientedMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The first-recipient contribution to the amplification second moment

theorem OAI.JointDickman.first_oriented_probability_sum line 14

Source documentation

The first-recipient orientations, summed over all dyadic change scales, have probability O_C(B^{-2}) in the actual two-site split law.

theorem first_oriented_probability_sum
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
      ∀ (L T : ℕ) (τ C : ℝ) (S : Finset ℕ),
      0 < T → (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
      (∀ i ∈ S, primeTailEndpoint B i ≤ 8 * B) →
      (∑ i ∈ S, twoSiteSplitProbability (auxiliaryPrimes B)
        (splitOrientationEvent (bothAmplificationSplitsGood B L T τ C) (primeTailEndpoint B i) false)) ≤
      K * (2 : ℝ)^(4 * C) / (B : ℝ)^2 := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeTailEndpoint, OAI.JointDickman.twoSiteSplitProbability, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.splitOrientationEvent, OAI.JointDickman.bothAmplificationSplitsGood