OAI/Geometry/RCD/Heat/HeatJointSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere symmetry of the jointly measurable heat density

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_withDensity line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatPairMeasure_withDensity line 32
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_symmetric_ae line 54

    Source documentation

    Self-adjointness gives genuine product-almost-everywhere symmetry of the constructed density.

    theorem heatJointDensity_symmetric_ae (t : ℝ) (ht : 0 < t) :
    ∀ᵐ xy ∂(hausdorff n X).prod (hausdorff n X),
      hX.heatJointDensity hn p t ht xy.1 xy.2 = hX.heatJointDensity hn p t ht xy.2 xy.1 := by
…

    Mentions: OAI.RegularPointCoordinates.hausdorff