OAI/Geometry/RCD/Heat/ContinuousKernelBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous intermediate densities from compact endpoint factors

The only composition identity is the actual integral of the two kernels. For the heat kernel it is the already proved semigroup identity.

  1. theorem OAI.RegularPointCoordinates.continuous_kernel_bridge_probability line 22