EndpointCoefficientMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The half-prime coefficient mass at a fixed first endpoint

def OAI.JointDickman.endpointCoefficientMass line 13

theorem OAI.JointDickman.endpointCoefficientMass_bound line 19

Source documentation

After averaging the second endpoint, each fixed first coefficient costs O(Sigma(j)/(B T)); its fair-split prefactor later supplies B.

theorem endpointCoefficientMass_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {δ : ℝ} (hδ : 0 < δ) (κ : ℝ) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ T q j b : ℕ,
      0 < T → Real.exp (δ*B) ≤ (q : ℝ) → T*q ≤ b → j ≠ 0 →
      (b : ℝ) ≤ Real.exp (κ*B) →
      Disjoint b.primeFactors (Nat.primesLE (auxiliaryCutoff B)) →
      endpointCoefficientMass B b j q ≤ K/((B : ℝ)*T)*singularFactor 24 j := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.endpointCoefficientMass, OAI.JointDickman.singularFactor