OAI/Geometry/RCD/Sobolev/ExponentialSobolev.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual positive Sobolev densities with a controlled logarithm

  1. theorem OAI.RegularPointCoordinates.exponential_sobolev line 16
  2. theorem OAI.RegularPointCoordinates.exponential_log_lipschitz line 32
  3. theorem OAI.RegularPointCoordinates.exponential_bounded line 50