OAI/Geometry/RCD/Heat/ContinuousKernelLog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous logarithmic transforms on compact endpoint supports

The endpoint measures are probabilities. A uniformly positive continuous kernel sends every continuous logarithmic weight to a continuous finite logarithmic weight. These are the maps used for the scaling fixed point.

  1. theorem OAI.RegularPointCoordinates.continuous_exp_integrable line 22
  2. theorem OAI.RegularPointCoordinates.continuous_exp_integral_pos line 27
  3. theorem OAI.RegularPointCoordinates.continuous_kernel_exp_integral_pos line 34
  4. def OAI.RegularPointCoordinates.continuousKernelLog line 47