HeatMeasureMassContinuity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the total mass of the constructed heat measures

def OAI.RegularPointCoordinates.radialCompactTest line 16
Source documentation
The standard radial plateau, viewed as a compact continuous test.
```
def radialCompactTest (p : X) (R : ℝ) (hR : 0 < R) : C_c(X, ℝ) :=
…
```

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_mass_limit line 27

Source documentation

Radial compact tests recover the whole mass by dominated convergence.

theorem heatRadonMeasure_mass_limit (t : ℝ) (ht : 0 < t) (x : X) :
    Tendsto (fun i : ℕ => hX.compactHeatEval hn p t ht x
      (radialCompactTest p ((i : ℝ) + 1) (by positivity))) atTop
      (𝓝 ((hX.heatRadonMeasure hn p t ht x).real univ)) := by
…

Mentions: OAI.RegularPointCoordinates.radialCompactTest

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_mass_lipschitz line 41
Source documentation
Uniform bounded-data smoothing persists in the limit of compact cutoffs, so total mass is a Lipschitz function of the initial center.
```
theorem heatRadonMeasure_mass_lipschitz (t : ℝ) (ht : 0 < t) :
    LipschitzWith ⟨Real.sqrt (1 / (2 * t * Real.exp (-2 * |K| * t))), Real.sqrt_nonneg _⟩
      (fun x => (hX.heatRadonMeasure hn p t ht x).real univ) := by
…
```