OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialRiesz.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The weak inverse of the positive radial energy form, constructed by Riesz representation on the closed graph space. This is not a postulated spectral or automorphic continuation.

  1. abbrev OAI.CubicFirstMoment.CubicThetaRadialL2 line 12
  2. def OAI.CubicFirstMoment.cubicThetaRadialProjection line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialProjection_norm line 17
  4. def OAI.CubicFirstMoment.cubicThetaRadialCoordinate line 22
  5. abbrev OAI.CubicFirstMoment.cubicThetaRadialInclusion line 27
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialCoordinate_bound line 29
  7. lemma OAI.CubicFirstMoment.cubicThetaRadialInclusion_norm line 37
  8. lemma OAI.CubicFirstMoment.cubicThetaRadialCoordinate_test line 42
  9. lemma OAI.CubicFirstMoment.cubicThetaRadialInclusion_test line 54
  10. def OAI.CubicFirstMoment.cubicThetaRadialWeakSolution line 58
  11. lemma OAI.CubicFirstMoment.cubicThetaRadialWeakSolution_equation line 63
  12. lemma OAI.CubicFirstMoment.cubicThetaRadialWeakSolution_unique line 69
  13. lemma OAI.CubicFirstMoment.cubicThetaRadialWeakSolution_bound line 77