OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFiniteEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The literal cubed-prime Hecke operator preserves actual finite-energy C1 sections. Both its value and gradient bounds are inherited from the proved domain integral identities.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFinite_mass_domain line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFinite_energy_domain line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeSection_memLp_of_domain line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeGradient_memLp_of_domain line 38
  5. def OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeFinite line 50
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeFinite_value_bound line 60
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHeckeFinite_gradient_bound line 67