OAI/Geometry/RCD/Heat/HeatMarkovKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The measurable Markov family associated to the RCD heat flow

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.radonHeatProbability line 22

    Source documentation

    Heat evaluation as a probability measure, constructed from the actual semigroup on compact continuous tests.

    def radonHeatProbability (t : ℝ) (ht : 0 < t) (x : X) : ProbabilityMeasure X :=
…
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radonHeatProbability_continuous line 25
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_measurable line 33

    Source documentation

    Closed-set approximation converts continuity on bounded tests into measurability of the entire measure-valued family.

    theorem heatRadonMeasure_measurable (t : ℝ) (ht : 0 < t) :
    Measurable (hX.heatRadonMeasure hn p t ht) := by
…
  4. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatMarkovKernel line 59

    Source documentation

    The canonical heat family is an actual measurable Markov kernel.

    def heatMarkovKernel (t : ℝ) (ht : 0 < t) : ProbabilityTheory.Kernel X X where
…
  5. instance OAI.RegularPointCoordinates.NoncollapsedRCD.heatMarkovKernel_isMarkov line 63