RegularFinitePatchCover.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual finite heat-coordinate covers on the working region

theorem OAI.RegularPointCoordinates.regular_finite_patch_cover line 18

Source documentation

Maximal metric nets and a fixed Euclidean cutoff produce localized finite covers with one dimensional overlap constant at every scale.

theorem regular_finite_patch_cover {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)
    (hzeta : zeta ≤ 1 / 64) (i : ℕ) (psi : Euclidean n → ℝ)
    (hsmooth : ContDiff ℝ ∞ psi) (hzero : ∀ z, 0 ≤ psi z) (hone : ∀ z, psi z ≤ 1)
    (hcore : ∀ z, ‖z‖ ≤ 2 → psi z = 1) (hsupport : tsupport psi ⊆ closedBall 0 3) :
    let region := regularPatchRegion base e.heat.radius e.heat.shift
…

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

theorem OAI.RegularPointCoordinates.regular_net_diameter_le line 71
Source documentation
Every pair of active points is close enough for both directional pinching and the reverse central mass-ball containment.
```
theorem regular_net_diameter_le {R : ℝ} (hR : 0 < R) (shift i : ℕ) :
    2 * 144 * regularNetRadius R shift i ≤ (R / (2 : ℝ) ^ (shift + i + 15)) / 12 := by
…
```
Mentions: OAI.RegularPointCoordinates.regularNetRadius