OAI/Geometry/RCD/Sobolev/LocalWeakSourceUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local uniqueness of L2 weak Laplacians

Compact Lipschitz tests determine the source on each interior region. The functions and their sources need only agree on the working set.

  1. theorem OAI.RegularPointCoordinates.IsWeakLaplacian.local_source_eq line 22