RegularMassSmallness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smallness of the actual full mass at the pinching radius

def OAI.RegularPointCoordinates.regularSmallMassCoefficient line 15
Source documentation
All volume and cutoff losses in the local smallness estimate.
```
def regularSmallMassCoefficient (n : ℕ) (C : ℝ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.regular_local_mass_small line 24

Source documentation

The local Bochner cutoff calculation makes the full original mass small in its own mean metric. Its coefficient tends to zero with the splitting error and the rescaled curvature.

theorem regular_local_mass_small {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base : X} {a κ B J C A Cχ enlargement zeta eta : ℝ}
    {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    {q : X} (hq : q ∈ ball base (e.heat.radius / 32))
    (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1) (hCχ : 0 ≤ Cχ)
    (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 8 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 2)
    (i : ℕ) (v : Euclidean n) :
    let r := e.heat.radius / (2 : ℝ) ^ (i + 15)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.Euclidean