OAI/Geometry/PrescribedPotential/PointPoisson.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Point Poisson.

  1. def OAI.GlobalElliptic.GluingData.pointEvaluation line 26
  2. lemma OAI.GlobalElliptic.GluingData.pointEvaluation_embed line 30
  3. lemma OAI.GlobalElliptic.GluingData.completedLOrder_constants line 37
  4. lemma OAI.GlobalElliptic.GluingData.constantsOrder_lower line 42
  5. lemma OAI.GlobalElliptic.GluingData.completedLOrder_to_constant line 50
  6. lemma OAI.GlobalElliptic.GluingData.completedLOrder_constant_kernel line 57
  7. def OAI.GlobalElliptic.GluingData.rawPoissonOrder line 69
  8. lemma OAI.GlobalElliptic.GluingData.rawPoissonOrder_equation line 72
  9. def OAI.GlobalElliptic.GluingData.pointPoissonOrder line 83
  10. lemma OAI.GlobalElliptic.GluingData.pointPoissonOrder_equation line 89
  11. lemma OAI.GlobalElliptic.GluingData.pointPoissonOrder_normalized line 98
  12. lemma OAI.GlobalElliptic.GluingData.pointPoissonOrder_unique line 107