OAI/Geometry/RCD/Sobolev/LocalLipschitzGreenTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local Green trace identity on the full open Euclidean ball

  1. theorem OAI.RegularPointCoordinates.laplacian_zero_off_tsupport line 13
  2. theorem OAI.RegularPointCoordinates.local_lipschitz_green_trace line 23