OAI/Geometry/RCD/Sobolev/WeakSourceGradientBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A weak Laplacian tested where its potential has bounded gradient

Only the gradient on the nonzero set of the test is needed. The test's gradient vanishes on its zero level set by Sobolev locality.

  1. theorem OAI.RegularPointCoordinates.weak_source_test_gradient_bound line 17