OAI/Geometry/RCD/Sobolev/LocalSourceStrongGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strong local gradients from uniform values and bounded source mass

The source representatives may differ outside the working set from the bounded Sobolev sequence used for weak compactness.

  1. theorem OAI.RegularPointCoordinates.local_source_strong_gradient line 20