OAI/Geometry/RCD/Heat/HeatJointDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Jointly measurable densities for the constructed heat family

A finite measure equivalent to Hausdorff measure permits use of the kernel Radon--Nikodym theorem even when the space has infinite volume. The chain rule returns a density relative to the original Hausdorff measure.

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity line 26

    Source documentation

    A jointly measurable version of the actual heat densities.

    def heatJointDensity (t : ℝ) (ht : 0 < t) (x y : X) : ℝ :=
…
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_measurable line 31
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_nonneg line 36
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_ae line 39
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_integrable line 56
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_mass_one line 60
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_integral_bounded line 65