OAI/Geometry/RCD/Heat/HeatGeneralRepresentation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Heat density representation on the required L¹ ∩ L² class

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_ae_integrable line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_represents line 28

    Source documentation

    Clipping and invariance extend the pointwise bounded-data representation to the exact L¹ ∩ L² data class in the published input.

    theorem heatRadonMeasure_represents (t : ℝ) (ht : 0 < t)
    (f : Lp ℝ 2 (hausdorff n X)) (hf : Integrable f (hausdorff n X)) :
    (fun x => ∫ y, f y ∂hX.heatRadonMeasure hn p t ht x) =ᵐ[hausdorff n X]
      heatAt (hausdorff n X) hX.quadratic t f := by
…

    Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.heatAt

  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatJointDensity_represents line 65