OAI/NumberTheory/JointDickman/Amplification/LatentEdgeSquareBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.candidateSquareMoment_bound line 13

   Source documentation

   The full edge square has the manuscript's power saving. Both cited inputs remain explicit; all representation and remainder steps are proved.

   theorem candidateSquareMoment_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) →
           ∀ (χ : BlockCandidateIndex M → ℝ), (∀ e, 0 ≤ χ e ∧ χ e ≤ 1) →
           ∀ (i t : Fin M), i < t → t.val-i.val ≤ auxiliaryCutoff B →
             ((t.val-i.val : ℕ) : ℝ) ≤ (B : ℝ)^2 →
             η*(B : ℝ)^(32/100 : ℝ) ≤ ((t.val-i.val : ℕ) : ℝ) →
             candidateSquareMoment B L T H τ C χ i t ≤
   …

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