OAI/Geometry/RCD/Transport/SobolevPlanDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Derivative bounds for actual Sobolev representatives along test plans

Gram coefficients need not be continuous on the space. Their absolutely continuous representatives along almost every path retain both endpoints and the relaxed-slope derivative bound.

  1. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_sobolev_derivative line 19