OAI/Geometry/RCD/Heat/HeatDensityL1Continuity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_integral_abs_sub_le line 20

   Source documentation

   Duality against the measurable sign of a density difference gives quantitative L¹ continuity without assuming any pointwise density bound.

   theorem heatRadonDensity_integral_abs_sub_le (t : ℝ) (ht : 0 < t) (x y : X) :
       (∫ z, |hX.heatRadonDensity hn p t ht x z - hX.heatRadonDensity hn p t ht y z|
         ∂hausdorff n X) ≤
         Real.sqrt (1 / (2 * t * Real.exp (-2 * |K| * t))) * dist x y := by
   …

   Mentions: OAI.RegularPointCoordinates.hausdorff

2. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatL1Density line 53

   Source documentation

   The density as an element of the actual L¹ space.

   def heatL1Density (t : ℝ) (ht : 0 < t) (x : X) : Lp ℝ 1 (hausdorff n X) :=
   …

   Mentions: OAI.RegularPointCoordinates.hausdorff

3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatL1Density_coe line 57
4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatL1Density_lipschitz line 61