OAI/NumberTheory/CubicMoment/Theta/CubicThetaGlobalGreen.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The positive global Green operator is constructed from the actual energy inclusion. Its resolvent is analytic off the nonnegative spectral axis; continuation across that axis is a separate step.

  1. lemma OAI.CubicFirstMoment.cubicThetaGlobalWeakSolution_eq_adjoint line 14
  2. def OAI.CubicFirstMoment.cubicThetaGlobalGreen line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaGlobalGreen_apply line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaGlobalGreen_norm line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaGlobalGreen_positive line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaGlobalGreen_energy line 39
  7. lemma OAI.CubicFirstMoment.cubicThetaGlobalGreen_unit line 44
  8. def OAI.CubicFirstMoment.cubicThetaGlobalResolvent line 49
  9. lemma OAI.CubicFirstMoment.cubicThetaGlobalResolvent_analytic line 52
  10. lemma OAI.CubicFirstMoment.cubicThetaGlobalResolvent_identity line 62
  11. lemma OAI.CubicFirstMoment.cubicThetaGlobalResolvent_range line 67