OAI/NumberTheory/JointDickman/Amplification/LatentRowSquareBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.candidateSquareMoment_row_bound line 14

   Source documentation

   Manuscript equation (24), before rewriting the finite expectations in sampling notation. The short-lag cutoff supplies the separation needed by the multiplicity sieve, and the singular factors sum uniformly over a row.

   theorem candidateSquareMoment_row_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L : ℕ} (hL : 10000 ≤ L) {η cap : ℝ} (hη : 0 < η) (hcap : 0 < cap) :
       ∃ τ K : ℝ, 0 < τ ∧ τ ≤ cap ∧ τ ≤ samplingTau ∧ 0 < K ∧
         ∀ᶠ B : ℕ in atTop, ∀ (T H M : ℕ) (C : ℝ),
           0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) →
           T ≤ auxiliaryCutoff B → (T : ℝ) ≤ (B : ℝ)^2 →
           η*(B : ℝ)^(32/100 : ℝ) ≤ H →
           ∀ (χ : BlockCandidateIndex M → ℝ), (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
           ∀ i : Fin M, (∑ t : Fin M, candidateSquareMoment B L T H τ C χ i t) ≤
             K*(B : ℝ)^(-(21/100 : ℝ)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.samplingTau, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.candidateSquareMoment