OAI/Geometry/RCD/Transport/RenyiSmoothDual.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A smooth Sobolev primitive for localized power variations

The derivative is frozen below the positive density level. The primitive vanishes at zero, so it defines an actual Sobolev function even when the reference measure has infinite mass.

  1. def OAI.RegularPointCoordinates.renyiSmoothSlope line 17
  2. def OAI.RegularPointCoordinates.renyiSmoothDual line 19
  3. theorem OAI.RegularPointCoordinates.renyiSmoothSlope_continuous line 21
  4. theorem OAI.RegularPointCoordinates.renyiSmoothSlope_bound line 28
  5. theorem OAI.RegularPointCoordinates.renyiSmoothDual_hasDerivAt line 35
  6. theorem OAI.RegularPointCoordinates.renyiSmoothDual_lipschitz line 42
  7. theorem OAI.RegularPointCoordinates.renyiSmoothDual_zero line 50
  8. theorem OAI.RegularPointCoordinates.renyiSmoothDual_formula line 53
  9. def OAI.RegularPointCoordinates.SobolevSpace.renyiSmooth line 73
  10. theorem OAI.RegularPointCoordinates.localGamma_renyiSmooth line 79