OAI/Geometry/RCD/Heat/CompactLaplaceLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compact Laplace limit on the actual support of a probability law

No full-support hypothesis is imposed on the surrounding compact space. The maximum is taken on the measure support, which is nonempty and conull.

  1. theorem OAI.RegularPointCoordinates.compact_laplace_limit line 21