RegularPinchingSmallness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smallness in the inverse mean metric of the actual patch operators

def OAI.RegularPointCoordinates.pinchingMassUnitFactor line 14
Source documentation
The original pinching radius is a fixed multiple of the mean radius.
```
def pinchingMassUnitFactor (n : ℕ) : ℝ := (16384 : ℝ) ^ 2 / (16384 : ℝ) ^ n
…
```

theorem OAI.RegularPointCoordinates.regular_pinching_mass_small line 20

Source documentation

The actual conjugated full mass is small in its own inverse mean metric, with no lower eigenvalue bound or discarded singular part.

theorem regular_pinching_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 : ℕ) (xi : 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