OAI/Geometry/RCD/Metric/ExponentialDensityIntegrals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Power and transport moments of an exponential Sobolev density

  1. theorem OAI.RegularPointCoordinates.exponential_density_power_integrable line 14
  2. theorem OAI.RegularPointCoordinates.exponential_density_moment_integrable line 25
  3. theorem OAI.RegularPointCoordinates.exponential_density_second_moment line 46