HessianDensityMassBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted Hessian bounds retaining the full positive mass

theorem OAI.RegularPointCoordinates.abs_le_factor_one_add_density line 12
Source documentation
A deliberately linear density bound, convenient for Gaussian tails.
```
theorem abs_le_factor_one_add_density {h j b : ℝ} (hj : 0 ≤ j) (hb : 0 ≤ b)
    (hh : h^2 ≤ j*b^2) : |h| ≤ b*(1+j) := by
…
```

theorem OAI.RegularPointCoordinates.weighted_abs_le_one_add_density line 21

Source documentation

The weighted mixed estimate uses only the product of the two energies.

theorem weighted_abs_le_one_add_density {w h j e f b : ℝ}
    (hw : 0 ≤ w) (hj : 0 ≤ j) (hb : 0 ≤ b)
    (hh : h^2 ≤ j*e*f) (he : w^2*e*f ≤ b^2) :
    w*|h| ≤ b*(1+j) := by
…

theorem OAI.RegularPointCoordinates.integral_abs_le_full_mass line 35

Source documentation

A pointwise density estimate integrates against the complete mass, including any singular part of the Bochner measure.

theorem integral_abs_le_full_mass (σ : Measure X) [IsFiniteMeasure σ]
    {S : Set X} (hS : μ S ≠ ⊤) {H : X → ℝ}
    (hH : AEStronglyMeasurable H (μ.restrict S)) {B : ℝ} (hB : 0 ≤ B)
    (hb : ∀ᵐ x ∂μ.restrict S, |H x| ≤ B*(1+(σ.rnDeriv μ x).toReal)) :
    Integrable H (μ.restrict S) ∧
      (∫ x in S, |H x| ∂μ) ≤ B*(μ.real S+σ.real S) := by
…