OAI/Geometry/RCD/Heat/HeatPairMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Symmetry of the measure on pairs induced by the heat flow

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_set_lintegral line 18
  2. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure line 41

    Source documentation

    The reference measure paired with its Markov transition.

    def heatPairMeasure (t : ℝ) (ht : 0 < t) : Measure (X × X) :=
…
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure_rectangle_balance line 44
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure_rectangle_le line 56
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure_restrict_symm line 64
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure_symm line 82

    Source documentation

    Detailed balance holds for the entire sigma-finite pair measure, not just for compactly supported tests.

    theorem heatPairMeasure_symm (t : ℝ) (ht : 0 < t) :
    hX.heatPairMeasure hn p t ht = (hX.heatPairMeasure hn p t ht).map Prod.swap := by
…
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatMarkovKernel_invariant line 95

    Source documentation

    The constructed heat kernel preserves the original Hausdorff measure.

    theorem heatMarkovKernel_invariant (t : ℝ) (ht : 0 < t) :
    hX.heatMarkovKernel hn p t ht ∘ₘ hausdorff n X = hausdorff n X := by
…

    Mentions: OAI.RegularPointCoordinates.hausdorff