OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowSampling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.halasz_character_window_inner line 12
2. theorem OAI.TwoPointCorrelations.halasz_window_sampling line 31

   Source documentation

   Finite Fourier sampling costs only the volume of the window times the number of pairs of centers whose translated windows can meet.

   theorem halasz_window_sampling {ι : Type*} {k : ℕ}
       (B : Finset ι) (S : Finset (Fin k → ℤ))
       (β : ι → Fin k → AddCircle (1:ℝ)) (a : ι → ℂ) (δ : Fin k → ℝ)
       (ha : ∀ b∈B,‖a b‖≤1) (hδ : ∀ j,0≤δ j) (hδhalf : ∀ j,δ j≤1/2)
       (hphase : ∀ m∈S,∀ j,2*Real.pi*|(m j:ℝ)| * δ j≤1) :
       (∏ j,δ j)^2*(∑ m∈S,‖∑ b∈B,a b*halaszVinogradovCharacter m (β b)‖^2)≤
         (∏ j,2*δ j)*
           (((B×ˢB).filter (fun p => HalaszWindowNear δ (β p.1) (β p.2))).card:ℝ) := by
   …

   Mentions: OAI.TwoPointCorrelations.halaszVinogradovCharacter, OAI.TwoPointCorrelations.HalaszWindowNear