RegularNetSeparation.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Global support separation for the actual heat-coordinate patches

theorem OAI.RegularPointCoordinates.RegularBilinearData.patch_region_subset line 23
Source documentation
The working region lies inside the common harmonic neighborhood.
```
theorem patch_region_subset : regularPatchRegion base d.radius d.shift ⊆ ball base (d.radius / 32) := by
…
```
Mentions: OAI.RegularPointCoordinates.regularPatchRegion
theorem OAI.RegularPointCoordinates.RegularBilinearData.patch_region_pair_bound line 32
Source documentation
Pair scales inside the working region follow the common heat index.
```
theorem patch_region_pair_bound {q z : X}
    (hq : q ∈ regularPatchRegion base d.radius d.shift)
    (hz : z ∈ regularPatchRegion base d.radius d.shift) :
    dist z q ≤ (d.radius / (2 : ℝ) ^ d.shift) / 128 := by
…
```
Mentions: OAI.RegularPointCoordinates.regularPatchRegion
theorem OAI.RegularPointCoordinates.RegularBilinearData.net_pair_lower_bound line 52
Source documentation
Beyond the net radius, the fine frozen norm separates every pair in the working region, including pairs outside its approximation ball.
```
theorem net_pair_lower_bound {q z : X}
    (hq : q ∈ regularPatchRegion base d.radius d.shift)
    (hz : z ∈ regularPatchRegion base d.radius d.shift)
    (hzeta : zeta ≤ 1 / 64) (i : ℕ)
    (hfar : regularNetRadius d.radius d.shift i ≤ dist z q) :
    dist z q ≤ 4 * ‖d.frozenAt q i (d.values z - d.values q)‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.regularPatchRegion, OAI.RegularPointCoordinates.regularNetRadius