OAI/NumberTheory/CubicMoment/Estimates/HarmonicGaussian.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic polynomial Gaussians and the anti-holomorphic raising operator used for the fixed angular Fourier transform.

  1. def OAI.CubicFirstMoment.harmonicGaussian line 13
  2. lemma OAI.CubicFirstMoment.harmonicGaussian_apply line 16
  3. lemma OAI.CubicFirstMoment.gaussianComplex_fderiv line 21
  4. lemma OAI.CubicFirstMoment.harmonicGaussian_fderiv line 34
  5. lemma OAI.CubicFirstMoment.harmonicGaussian_raising line 48