OAI/Geometry/RCD/Transport/PositiveExponentialTilt.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strict positivity of bounded exponential tilts

The lower bound retains the mass of the original integrable weight. It applies to the compact-support positive kernel rows without a pointwise positive lower bound on the endpoint density.

  1. theorem OAI.RegularPointCoordinates.exponential_tilt_mass_lower line 18
  2. theorem OAI.RegularPointCoordinates.exponential_tilt_mass_pos line 33