OAI/Geometry/RCD/Heat/KernelScalingFixedPoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed point for compact positive kernel scaling

Alternating the two negative logarithmic transforms is a strict contraction on continuous functions modulo constants.

  1. def OAI.RegularPointCoordinates.transposeContinuousKernel line 20
  2. theorem OAI.RegularPointCoordinates.positive_kernel_difference_fixedPoint line 23