OAI/Geometry/RCD/Heat/HeatKernelSemigroup.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Chapman--Kolmogorov for the constructed Markov kernel

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral_compact_semigroup line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatMarkovKernel_comp line 37

    Source documentation

    The Radon probability family satisfies the measure-valued Chapman--Kolmogorov law at every starting point.

    theorem heatMarkovKernel_comp (s t : ℝ) (hs : 0 < s) (ht : 0 < t) :
    hX.heatMarkovKernel hn p t ht ∘ₖ hX.heatMarkovKernel hn p s hs =
      hX.heatMarkovKernel hn p (s + t) (add_pos hs ht) := by
…