OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalFourierAlgebra.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linearity of the literal horizontal Fourier observation.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontalFourier_integrable_of_integrable line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaHorizontalFourier_add line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaHorizontalFourier_const_mul line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaHorizontalFourier_sum line 38