OAI/Geometry/PrescribedPotential/RealPoisson.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Real Poisson.

  1. lemma OAI.GlobalElliptic.GluingData.pointPoissonOrder_realCore line 23
  2. def OAI.GlobalElliptic.GluingData.realLOrder line 40
  3. def OAI.GlobalElliptic.GluingData.realConstants line 47
  4. def OAI.GlobalElliptic.GluingData.realEvaluation line 51
  5. def OAI.GlobalElliptic.GluingData.realPointPoisson line 54
  6. lemma OAI.GlobalElliptic.GluingData.residue_real line 64
  7. def OAI.GlobalElliptic.GluingData.realResidue line 79
  8. lemma OAI.GlobalElliptic.GluingData.realPointPoisson_equation line 84
  9. lemma OAI.GlobalElliptic.GluingData.realPointPoisson_normalized line 98
  10. lemma OAI.GlobalElliptic.GluingData.realLOrder_constants line 109
  11. lemma OAI.GlobalElliptic.GluingData.realEvaluation_constants line 114