OAI/Geometry/RCD/Transport/MeasuredTransportValues.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The endpoint means of actual Sobolev functions have the prescribed value limits
- theorem
OAI.RegularPointCoordinates.MeasuredTransportData.mean_difference_tendstoline 15