OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialGreen.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The bounded positive Green operator of the radial Dirichlet form and its actual local resolvent. This is constructed from the energy space.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadialWeakSolution_eq_adjoint line 14
  2. def OAI.CubicFirstMoment.cubicThetaRadialGreen line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialGreen_apply line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaRadialGreen_norm line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaRadialGreen_selfAdjoint line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialGreen_energy line 41
  7. lemma OAI.CubicFirstMoment.cubicThetaRadialGreen_one_sub_unit line 46
  8. def OAI.CubicFirstMoment.cubicThetaRadialResolvent line 53
  9. lemma OAI.CubicFirstMoment.cubicThetaRadialResolvent_analytic line 57
  10. lemma OAI.CubicFirstMoment.cubicThetaRadialResolvent_identity line 67