OAI/NumberTheory/CubicMoment/Estimates/FarMellinKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Angular-frequency normalization of the far-cutoff Fourier kernel. It has exactly the same L1 mass for every positive cell scale.

  1. def OAI.CubicFirstMoment.farMellinKernel line 12
  2. lemma OAI.CubicFirstMoment.farFourierKernel_continuous line 15
  3. lemma OAI.CubicFirstMoment.farMellinKernel_continuous line 20
  4. lemma OAI.CubicFirstMoment.farMellinKernel_integrable line 25
  5. lemma OAI.CubicFirstMoment.farMellinKernel_mass line 29
  6. lemma OAI.CubicFirstMoment.farMellinKernel_reparametrize line 40

    Source documentation

    Reparametrization to the convention exp(i*v*log n) used by normTwist.

    lemma farMellinKernel_reparametrize (J : ℝ) (g : ℝ → ℂ) :
    (∫ v : ℝ, farMellinKernel J v*g v) =
      ∫ u : ℝ, farFourierKernel J u*g (2*Real.pi*u) := by
…

    Mentions: OAI.CubicFirstMoment.farMellinKernel, OAI.CubicFirstMoment.farFourierKernel

  7. theorem OAI.CubicFirstMoment.far_norm_sum_mellin line 55
  8. theorem OAI.CubicFirstMoment.far_gauss_sum_mellin line 79