OAI/NumberTheory/JointDickman/Probability/ManuscriptHistogramFourier.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.manuscriptCellSum line 11
2. def OAI.JointDickman.manuscriptCellApprox line 20
3. theorem OAI.JointDickman.manuscript_histogram_fourier_error line 29

   Source documentation

   A local collection of fine cells incurs exactly the square of its oscillation scale; no number-of-boxes loss appears.

   theorem manuscript_histogram_fourier_error {m B q : ℕ} [NeZero q]
       (hm : 0 < m) (hB : 0 < B)
       (J : Finset (Fin (channelFineCount m B)))
       (g : (auxiliaryPrimes B → Bool) → ℝ) (hg : ∀ x, |g x| ≤ 1)
       (F : ℝ → ℂ) {L : ℝ} (hL : 0 ≤ L)
       (hF : ∀ i ∈ J, IntervalIntegrable F volume
         (channelLower (channelFineCount m B) i) (channelUpper (channelFineCount m B) i))
       (hLip : ∀ i ∈ J, ∀ u ∈ Set.Icc (channelLower (channelFineCount m B) i)
           (channelUpper (channelFineCount m B) i),
         ∀ v ∈ Set.Icc (channelLower (channelFineCount m B) i)
           (channelUpper (channelFineCount m B) i), ‖F u-F v‖ ≤ L*|u-v|) :
       (∑ h : ZMod q, ‖unitResidueFourier
   …

   Mentions: OAI.JointDickman.channelFineCount, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.channelLower, OAI.JointDickman.channelUpper, OAI.JointDickman.unitResidueFourier