OAI/NumberTheory/JointDickman/Amplification/DiagonalRemoval.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.amplificationOuterWeight line 12
2. def OAI.JointDickman.amplificationInnerWeight line 15
3. theorem OAI.JointDickman.firstFormDiagonal_arithmetic_le line 18
4. theorem OAI.JointDickman.smooth_diagonal_negligible line 32

   Source documentation

   The limits are taken in the manuscript's order: first the counting scale N, then B. This statement is uniform over all bounded second labels.

   theorem smooth_diagonal_negligible
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L : ℕ} (hL : 1 ≤ L) {τ : ℝ} (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau)
       (C : ℝ) (J : ℕ → ℕ → ℂ) (hJ : ∀ N n, ‖J N n‖ ≤ 2) :
       ∀ ε : ℝ, 0 < ε → ∀ᶠ B : ℕ in atTop, ∀ᶠ N : ℕ in atTop,
         firstFormDiagonal B L τ C (amplificationOuterWeight B)
           (amplificationInnerWeight (amplificationMultiplier B)) (J N) N /
           ((B : ℝ)*amplificationMultiplier B) ≤ ε := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.samplingTau, OAI.JointDickman.firstFormDiagonal, OAI.JointDickman.amplificationOuterWeight, OAI.JointDickman.amplificationInnerWeight, OAI.JointDickman.amplificationMultiplier