OAI/Geometry/PrescribedPotential/UniformPathSobolev.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform Path Sobolev.

  1. lemma OAI.GlobalElliptic.GluingData.pointPoissonOrder_laplacian line 24
  2. lemma OAI.GlobalElliptic.GluingData.normalized_sobolev_laplacian_estimate line 38
  3. theorem OAI.GlobalElliptic.GluingData.pathSobolevBounds line 61