FirstPairMassBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The uniform first-representation mass at a fixed lag

theorem OAI.JointDickman.halfPrimeSubsetMass_nonneg line 11

theorem OAI.JointDickman.supportedEndpointTest_half_mean_bound line 21

Source documentation

The coefficient test averaged under the exact half-prime law.

theorem supportedEndpointTest_half_mean_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (T b j : ℕ),
      0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → j ≠ 0 →
      Disjoint b.primeFactors (Nat.primesLE (auxiliaryCutoff B)) →
      (∑ A ∈ (auxiliaryPrimes B).powerset,
        bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1/2 : ℝ)/p) A*
        supportedEndpointTest B T b j (∏ p ∈ A, p)) ≤
        K/((B : ℝ)*T)*singularFactor 24 j := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.supportedEndpointTest, OAI.JointDickman.singularFactor

theorem OAI.JointDickman.candidateFirstPairMass_bound line 50

Source documentation

Summing all first pairs costs O(Sigma(j)/T). There is no dependence on the number of representations or on the endpoint regularity cutoffs.

theorem candidateFirstPairMass_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (L T H M : ℕ) (τ C : ℝ),
      0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) →
      ∀ (χ : BlockCandidateIndex M → ℝ), (∀ e, χ e ≤ 1) →
      ∀ (i t : Fin M), i < t →
        candidateFirstPairMass B L T H τ C χ i t ≤ K/(T : ℝ)*singularFactor 24 (t.val-i.val) := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.candidateFirstPairMass, OAI.JointDickman.singularFactor