ActualHeatMass.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Heat averages of full local mass measures

The weight is the same actual heat kernel and compact cutoff used in the Gram matrices. The mass can have a singular part and is identified locally with the Bochner measure.

def OAI.RegularPointCoordinates.cutoffHeatWeight line 27
Source documentation
The actual cutoff heat weight, as a bounded continuous function.
```
def cutoffHeatWeight {t : ℝ} (ht : 0 < t) (x : X) : X →ᵇ ℝ :=
…
```
theorem OAI.RegularPointCoordinates.cutoffHeatWeight_apply line 33
def OAI.RegularPointCoordinates.cutoffHeatMass line 40
Source documentation
Heat integration of the full mass measure on a finite coordinate span.
```
def cutoffHeatMass {t : ℝ} (ht : 0 < t) (x : X) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.cutoffHeatMass_energy line 43
theorem OAI.RegularPointCoordinates.cutoffHeatMass_isPositive line 48
theorem OAI.RegularPointCoordinates.cutoffHeatMass_comap line 54

theorem OAI.RegularPointCoordinates.cutoffHeatMass_lower_mass line 61

Source documentation

Kernel lower estimates turn directly into estimates for singular or absolutely continuous mass on the testing ball.

theorem cutoffHeatMass_lower_mass (hχpos : ∀ y, 0 ≤ χ y)
    {t : ℝ} (ht : 0 < t) (x : X) (s : Set X) (hs : MeasurableSet s)
    (hχone : ∀ y ∈ s, χ y = 1) (c : ℝ) (hc : ∀ y ∈ s, c ≤ p t x y) (v : E) :
    c * ⟪v, M.massOperator s v⟫_ℝ ≤
      ⟪v, cutoffHeatMass μ hQ hp hχ hsχ M ht x v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.cutoffHeatMass

theorem OAI.RegularPointCoordinates.cutoffHeatMass_energy_mono line 74

Source documentation

Spatial comparisons of the kernel also compare heat mass matrices, without needing pointwise representatives of a mass density.

theorem cutoffHeatMass_energy_mono (hχpos : ∀ y, 0 ≤ χ y)
    {t s : ℝ} (ht : 0 < t) (hs : 0 < s) (x z : X)
    (hkernel : ∀ y, p t x y ≤ p s z y) (v : E) :
    ⟪v, cutoffHeatMass μ hQ hp hχ hsχ M ht x v⟫_ℝ ≤
      ⟪v, cutoffHeatMass μ hQ hp hχ hsχ M hs z v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.cutoffHeatMass