OAI/Geometry/PrescribedPotential/QuantitativeResolvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Resolvent.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.positive_eigenfunction_nonpos line 21
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.positive_eigenfunction_zero line 37
  3. lemma OAI.GlobalElliptic.shifted_complex_kernel line 58
  4. lemma OAI.GlobalElliptic.GluingData.shiftedOperator_embed line 79
  5. lemma OAI.GlobalElliptic.GluingData.completedResolvent_left line 86
  6. lemma OAI.GlobalElliptic.GluingData.shiftedOperator_bijective line 115
  7. theorem OAI.GlobalElliptic.GluingData.elliptic_estimate line 121