OAI/Geometry/RCD/Sobolev/EndpointLIntegralLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative endpoint-weighted integrals under weak convergence

  1. theorem OAI.RegularPointCoordinates.endpoint_weight_lintegral_eq line 14
  2. theorem OAI.RegularPointCoordinates.weak_endpoint_weight_lintegral line 33