OAI/Geometry/RCD/Metric/CompactFactorExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Zero extension of continuous weights on compact endpoint supports

The extension is bounded and measurable and belongs to L² for locally finite measures. Continuity across the support boundary is not needed.

  1. def OAI.RegularPointCoordinates.compactFactorExtension line 19
  2. theorem OAI.RegularPointCoordinates.compactFactorExtension_coe line 23
  3. theorem OAI.RegularPointCoordinates.compactFactorExtension_off line 27
  4. theorem OAI.RegularPointCoordinates.compactFactorExtension_measurable line 33
  5. theorem OAI.RegularPointCoordinates.compactFactorExtension_bounded line 38
  6. theorem OAI.RegularPointCoordinates.compactFactorExtension_memLp line 49