OAI/NumberTheory/TwoPoint/Halasz/HalaszCircleWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A compact circle window with a lower bound for its small Fourier coefficients. This supplies the localizer for the double moment estimate.

  1. def OAI.TwoPointCorrelations.halaszCircleWindow line 15
  2. lemma OAI.TwoPointCorrelations.halasz_circle_window_memLp line 18
  3. lemma OAI.TwoPointCorrelations.halasz_circle_window_volume line 22
  4. lemma OAI.TwoPointCorrelations.halasz_circle_character_re line 29
  5. theorem OAI.TwoPointCorrelations.halasz_circle_window_coefficient line 61

    Source documentation

    The small Fourier coefficients of the indicator window cannot cancel.

    theorem halasz_circle_window_coefficient {δ : ℝ} {n : ℤ}
    (hδ : 0≤δ) (hδhalf : δ≤1/2) (hphase : 2*Real.pi*|(n:ℝ)| * δ≤1) :
    δ≤‖∫ x : AddCircle (1:ℝ), conj (fourier n x)*halaszCircleWindow δ x
      ∂AddCircle.haarAddCircle‖ := by
…

    Mentions: OAI.TwoPointCorrelations.halaszCircleWindow