FiniteHistogramFourier.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local histogram Fourier bound in finite-cell form

theorem OAI.JointDickman.finite_histogram_fourier_bound line 12

Source documentation

The local window length is card(J)*delta. It is retained explicitly, so summing boxes can use bounded overlap rather than their number.

theorem finite_histogram_fourier_bound {ι : Type*} [DecidableEq ι]
    {q : ℕ} [NeZero q] (J : Finset ι) {δ M : ℝ}
    (_hδ : 0 ≤ δ) (_hM : 0 ≤ M) (U : ι → (ZMod q)ˣ → ℝ)
    (v : (ZMod q)ˣ → ℂ)
    (hv : ∀ r, ‖v r‖ ≤ δ*M*(∑ i ∈ J, U i r)) :
    (∑ h : ZMod q, ‖unitResidueFourier v h/(q.totient : ℂ)‖^2) ≤
      ((q : ℝ)/(q.totient : ℝ))*((J.card : ℝ)*δ)*M^2*
        (∑ i ∈ J, ∑ r : (ZMod q)ˣ, (δ/(q.totient : ℝ))*U i r^2) := by
…

Mentions: OAI.JointDickman.unitResidueFourier