OAI/Geometry/RCD/Sobolev/PoissonSpanLift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Isometric inclusion of all coordinate covectors in the Poisson span

  1. def OAI.RegularPointCoordinates.poissonCoordinateLift line 12
  2. theorem OAI.RegularPointCoordinates.poissonCoordinateLift_norm line 15
  3. theorem OAI.RegularPointCoordinates.poissonSpanMap_lift line 23
  4. theorem OAI.RegularPointCoordinates.poissonSpanLaplacian_lift line 30