OAI/Geometry/RCD/Heat/NonnegativeKernelBridgeMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The mass identity for forward and backward kernel factors

Tonelli identifies their product mass with the composed endpoint kernel. This form permits noncompact intermediate spaces and needs no integrability assumption before the endpoint normalization is applied.

  1. theorem OAI.RegularPointCoordinates.nonnegative_kernel_bridge_mass line 20