OAI/NumberTheory/CubicMoment/Estimates/CubicWhittakerMellin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact archimedean factor of the cubic theta Fourier expansion, using the fixed Schläfli kernel and the normalization 4*pi*v.

  1. def OAI.CubicFirstMoment.cubicThetaWhittaker line 12

    Source documentation

    The heat-integral realization of v*K_(1/3)(4*pi*v).

    def cubicThetaWhittaker (v : ℝ) : ℂ :=
…
  2. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_mellin line 15