OAI/Geometry/RCD/Sobolev/BochnerMeasureFromSource.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The full measure Laplacian from the continuous Bochner test identity
- theorem
OAI.RegularPointCoordinates.bochner_measure_laplacian_of_sourceline 15