OAI/Geometry/RCD/Coordinates/KernelBridgeNormalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of an intermediate kernel bridge

The composed kernel and one endpoint marginal fix the intermediate mass. This is the normalization identity for the entropic interpolation.

  1. theorem OAI.RegularPointCoordinates.kernel_bridge_normalized line 21
  2. theorem OAI.RegularPointCoordinates.kernel_bridge_probability line 54