OAI/NumberTheory/JointDickman/Probability/MajorArcHistogramBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.logOscillatoryTest_continuous line 10
2. theorem OAI.JointDickman.majorArc_histogram_bound line 18

   Source documentation

   The bound for (38) now applies directly to the major-arc test, with its logarithmic derivative loss and the local window length both explicit.

   theorem majorArc_histogram_bound {m B q : ℕ} [NeZero q]
       (hm : 0 < m) (hB : 1 ≤ B) {a b N M D ω : ℝ}
       (ha : 0 < a) (hab : a ≤ b) (hN : 0 < N) (hM : 0 ≤ M) (hD : 0 ≤ D)
       (g : (auxiliaryPrimes B → Bool) → ℝ) (hg : ∀ x, |g x| ≤ 1)
       (w w' : ℝ → ℝ) (hw : ∀ t, HasDerivAt w (w' t) t)
       (hwb : ∀ t, |w t| ≤ M) (hw'b : ∀ t, |w' t| ≤ D) :
       let J := histogramWindowCells (channelFineCount m B) (Real.log (a*N)/B) (Real.log (b*N)/B)
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.histogramWindowCells, OAI.JointDickman.channelFineCount