OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The normalized Fourier energy is the literal squared modulus integrated over the physical level-three horizontal cell, with its exact area.

  1. lemma OAI.CubicFirstMoment.cubicThetaTorus_norm_square_integral line 16
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModel_horizontal_energy line 27