OAI/Geometry/RCD/Heat/HeatRadonDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An actual L¹ density for every positive-time heat measure

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity line 20

    Source documentation

    The Radon--Nikodym density of the constructed heat measure.

    def heatRadonDensity (t : ℝ) (ht : 0 < t) (x y : X) : ℝ :=
…
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_nonneg line 24
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_measurable line 28
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_integrable line 33
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_integral_compact line 38
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_integral line 47
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_mass_one line 55

    Source documentation

    The actual positive-time density has probability mass.

    theorem heatRadonDensity_mass_one (t : ℝ) (ht : 0 < t) (x : X) :
    (∫ y, hX.heatRadonDensity hn p t ht x y ∂hausdorff n X) = 1 := by
…

    Mentions: OAI.RegularPointCoordinates.hausdorff