OAI/NumberTheory/CubicMoment/Estimates/FarFourierSeparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier separation of the far product cutoff. The kernel has uniform L1 norm, and its shifts act on the actual norm twists.

  1. def OAI.CubicFirstMoment.farFourierKernel line 13
  2. lemma OAI.CubicFirstMoment.farFourierKernel_integrable line 16
  3. lemma OAI.CubicFirstMoment.farFourierKernel_mass line 19
  4. lemma OAI.CubicFirstMoment.farFourierKernel_phase_integrable line 23
  5. lemma OAI.CubicFirstMoment.far_finite_fourier_separation line 31
  6. lemma OAI.CubicFirstMoment.normTwist_far_phase line 56
  7. theorem OAI.CubicFirstMoment.far_norm_sum_separation line 67

    Source documentation

    The finite Gauss sum with the far cutoff is an integral of the original polynomial at common shifted heights.

    theorem far_norm_sum_separation {ι : Type*} (S : Finset ι) (c : ι → ℂ)
    (n : ι → Eisenstein) (s x₀ : ℝ) {J : ℝ} (hJ : 0 < J) :
    (∑ a ∈ S, c a*normTwist s (n a)*
      farInverseSquare (J*(Real.log (norm (n a))-x₀))) =
      ∫ u : ℝ, farFourierKernel J u *
        Complex.exp ((-2*Real.pi*u*x₀:ℝ)*Complex.I) *
          ∑ a ∈ S, c a*normTwist (s+2*Real.pi*u) (n a) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.farInverseSquare, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.farFourierKernel

  8. theorem OAI.CubicFirstMoment.far_gauss_sum_separation line 86