OAI/Geometry/RCD/Sobolev/RadialSobolevTimeMeasurable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable Sobolev families from continuous compact local values

  1. theorem OAI.RegularPointCoordinates.radialLocalSobolev_toLp_continuous line 22
  2. theorem OAI.RegularPointCoordinates.radialLocalSobolev_stronglyMeasurable line 46
  3. theorem OAI.RegularPointCoordinates.sobolev_limit_aestronglyMeasurable line 59