OAI/Geometry/RCD/Metric/UniformInteriorLocalMass.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Scale-uniform transport bounds by a localized image-energy mass
- theorem
OAI.RegularPointCoordinates.MeasuredTransportData.uniform_interior_local_image_massline 18