RegularPatchSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A single total family of actual patch operators

structure OAI.RegularPointCoordinates.RegularPatchSelection line 17
Source documentation
Extending the selected net centers outside the net makes the operator family total without changing any active patch.
```
structure RegularPatchSelection {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    [(hausdorff n X).Regular] {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta : ℝ} (d : RegularBilinearData hX base hk enlargement zeta)
    (psi : Euclidean n → ℝ) {Cpin budget : ℝ} (f : RegularPinchingField d Cpin budget) where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularBilinearData, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.RegularPinchingField

def OAI.RegularPointCoordinates.regularPatchSelection line 35

Source documentation

The selector is constructed from the already proved finite covers and positive energy floors.

def regularPatchSelection {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base : X} {a κ B J C A Cχ enlargement zeta eta Cpin budget : ℝ}
    {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) (psi : EuclideanGevreyCutoff n)
    (f : RegularPinchingField e.heat Cpin budget) (hCpin : 0 ≤ Cpin) :
    RegularPatchSelection e.heat psi.value f := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.EuclideanGevreyCutoff, OAI.RegularPointCoordinates.RegularPinchingField, OAI.RegularPointCoordinates.RegularPatchSelection