OAI/NumberTheory/DukePrimeDegree/Dynamics/KernelVelocityDistance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurable distances to actual component velocity spaces

The lower semicontinuous distance on weak probabilities pulls back along any genuine probability kernel. The measurable conclusion uses neither a chosen tangent frame nor an added regularity assumption on the kernel.

  1. theorem OAI.DukePrimeDegree.measurable_kernel_velocityDistance line 21