OAI/Geometry/RCD/Sobolev/DistanceLaplacian.lean

The local squared-distance input from the RCD condition

The radial first variation gives positivity. A larger-radius cutoff gives finite mass, and positive extension followed by Riesz--Markov constructs the defect measure used by the coordinate argument.