OAI/Geometry/RCD/Heat/ContinuousKernelContraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Contraction of continuous positive kernel transforms

The norm is the supremum of pairwise differences. Consequently the strict contraction factor has no loss from choosing a base point.

  1. theorem OAI.RegularPointCoordinates.kernel_tilt_one line 21
  2. theorem OAI.RegularPointCoordinates.kernel_tilt_zero line 37
  3. theorem OAI.RegularPointCoordinates.continuousKernelLog_oscillation line 45
  4. theorem OAI.RegularPointCoordinates.continuousKernelLog_pair_bound line 73