OAI/Geometry/RCD/Sobolev/CompactBochnerSobolevMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full Bochner measure on continuous Sobolev tests

Positivity on continuous compact Sobolev tests gives a finite measure on each interior ball. The formula retains the square of the L² Laplacian and the gradient pairing, and hence needs no derivative of that Laplacian.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_bochner_sobolev_measure line 22