OAI/Geometry/RCD/Sobolev/WeakLaplacianSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Support of the actual weak Laplacian

Locality against cutoff multiples and density of the Sobolev domain show that a compactly supported function has no Laplacian outside its support.

  1. theorem OAI.RegularPointCoordinates.IsWeakLaplacian.cutoff_mul_eq_zero line 19
  2. theorem OAI.RegularPointCoordinates.IsWeakLaplacian.zero_off_closedBall line 65