OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The radial energy form of the separated hyperbolic operator. Integration by parts and coercivity are proved on compactly supported complex test functions, including the actual nonzero-frequency potential.

  1. lemma OAI.CubicFirstMoment.cubicTheta_inner_compact line 13
  2. lemma OAI.CubicFirstMoment.cubicTheta_inner_integrable line 21
  3. lemma OAI.CubicFirstMoment.cubicTheta_test_integrationByParts line 25
  4. def OAI.CubicFirstMoment.cubicThetaRadialOperator line 42
  5. lemma OAI.CubicFirstMoment.cubicThetaRadialOperator_energy line 45
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialOperator_coercive line 76