OAI/Geometry/RCD/Transport/ExponentialTiltVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact first variations of compact exponential density perturbations

  1. theorem OAI.RegularPointCoordinates.exponential_tilt_integral_hasDerivAt_zero line 14
  2. theorem OAI.RegularPointCoordinates.normalized_tilt_hasDerivAt_zero line 49