OAI/NumberTheory/CubicMoment/Estimates/GaussianTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Fourier kernels with the Eisenstein trace normalization.

  1. lemma OAI.CubicFirstMoment.traceFourier_eq_fourier line 13
  2. theorem OAI.CubicFirstMoment.traceFourier_gaussian line 27

    Source documentation

    The trace pairing doubles the usual Fourier frequency.

    theorem traceFourier_gaussian {t : ℝ} (ht : 0 < t) (w : ℂ) :
    traceFourier (fun z : ℂ => Complex.exp (-(t:ℂ)*‖z‖^2)) w =
      (Real.pi/t:ℝ) * Complex.exp ((-4*Real.pi^2/t*Complex.normSq w:ℝ):ℂ) := by
…

    Mentions: OAI.CubicFirstMoment.traceFourier