OAI/NumberTheory/TwoPoint/Bounds/FourierRegionBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.circle_integrable line 18
2. lemma OAI.TwoPointCorrelations.circle_integral_mul_norm_le line 23
3. lemma OAI.TwoPointCorrelations.fourier_pointwise_split line 36
4. lemma OAI.TwoPointCorrelations.norm_sum_circle_integral_le line 83
5. lemma OAI.TwoPointCorrelations.circle_integral_sum_mul_norm_le line 95
6. lemma OAI.TwoPointCorrelations.circle_integral_linear_bound line 105
7. lemma OAI.TwoPointCorrelations.circle_integrate_pointwise_split line 120
8. theorem OAI.TwoPointCorrelations.fourier_region_bound line 146

   Source documentation

   A finite-family version of the analytic split. The threshold term uses only Cauchy--Schwarz; the complementary term uses the fourth moment and our fixed-frequency sum over origins.

   theorem fourier_region_bound {ι : Type*} (S : Finset ι)
       (B : AddCircle (1 : ℝ) → ℂ) (F G : ι → AddCircle (1 : ℝ) → ℂ)
       (hB : Continuous B) (hF : ∀ v ∈ S, Continuous (F v))
       (hG : ∀ v ∈ S, Continuous (G v))
       (ε Bmax Gmax K : ℝ) (hε : 0 < ε)
       (hBmax : 0 ≤ Bmax) (hGmax : 0 ≤ Gmax) (hK : 0 ≤ K)
       (hBbound : ∀ θ, ‖B θ‖ ≤ Bmax)
       (hGbound : ∀ v ∈ S, ∀ θ, ‖G v θ‖ ≤ Gmax)
       (hFsum : ∀ θ, (∑ v ∈ S, ‖F v θ‖) ≤ K) :
       ‖∑ v ∈ S, ∫ θ, B θ * F v θ * G v θ ∂AddCircle.haarAddCircle‖ ≤
         ε * ∑ v ∈ S,
           Real.sqrt (∫ θ, ‖F v θ‖ ^ 2 ∂AddCircle.haarAddCircle) *
   …