OAI/Geometry/RCD/Heat/BoundedExponentialIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded exponential integrals for compact-support kernel scaling

Only a bounded measurable exponent and an integrable weight are needed. The logarithmic derivative is used for the positive heat-kernel scaling in the entropic approximation of bounded-support transport plans.

  1. theorem OAI.RegularPointCoordinates.bounded_exp_mul_integrable line 18
  2. theorem OAI.RegularPointCoordinates.exponential_tilt_integral_hasDerivAt line 32
  3. theorem OAI.RegularPointCoordinates.log_exponential_tilt_hasDerivAt line 53