OAI/Geometry/RCD/Sobolev/WeakEndpointWeights.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Weak convergence with a fixed integrable endpoint weight
- theorem
OAI.RegularPointCoordinates.weak_endpoint_weight_integralline 14