OAI/Geometry/RCD/Coordinates/ShiftedLogarithmRegularData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sobolev source and Gram data of the actual shifted logarithm

The source is formed from bounded Lipschitz multipliers of the original Sobolev source and Gram function. It need not be bounded globally.

  1. theorem OAI.RegularPointCoordinates.shifted_logarithm_regular_data line 20