OAI/Geometry/RCD/Heat/PositiveKernelScaling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Scaling positive continuous kernels to prescribed endpoint laws

For compact endpoint spaces and probability laws, the two positive continuous factors satisfy both marginal equations exactly. This is the compact-support scaling step in Gigli--Tamanini, JEMS 23 (2021), Theorem 2.2. Only its existence conclusion is needed here.

  1. theorem OAI.RegularPointCoordinates.positive_kernel_scaling line 21
  2. theorem OAI.RegularPointCoordinates.continuous_positive_kernel_scaling line 46