RegularNetGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The metric geometry of the actual fine heat-coordinate patches

def OAI.RegularPointCoordinates.regularNetRadius line 17
Source documentation
The net is substantially finer than the pinching mean radius, so that all active energy centers satisfy the reverse mass-covering condition.
```
def regularNetRadius (R : ℝ) (shift i : ℕ) : ℝ := R / (2 : ℝ) ^ (shift + i + 28)
```
def OAI.RegularPointCoordinates.regularPatchRegion line 21
Source documentation
The region is small enough that all pair comparison scales follow the common heat comparison index.
```
def regularPatchRegion {X : Type*} [MetricSpace X] (p : X) (R : ℝ) (shift : ℕ) : Set X :=
…
```

theorem OAI.RegularPointCoordinates.RegularBilinearData.exact_frame_pair_error line 34

Source documentation

Return the published coordinate approximation to physical distance.

theorem exact_frame_pair_error {q z : X} (hq : q ∈ ball base (d.radius / 32))
    (j : ℕ) (hroom : dist z q ≤ 4 * ((d.radius / (2 : ℝ) ^ j) / 128)) :
    |‖coordinateFrame (d.frameAt q hq j) (d.values z - d.values q)‖ - dist q z| ≤
      zeta * ((d.radius / (2 : ℝ) ^ j) / 128) := by
…

Mentions: OAI.RegularPointCoordinates.coordinateFrame

theorem OAI.RegularPointCoordinates.RegularBilinearData.net_near_pair_bound line 44

Source documentation

Every net neighbor lies in the core of the cutoff expressed in the actual frozen heat coordinates.

theorem net_near_pair_bound {q z : X} (hq : q ∈ ball base (d.radius / 32))
    (hzeta : zeta ≤ 1 / 64) (i : ℕ)
    (hroom : dist z q ≤ regularNetRadius d.radius d.shift i) :
    ‖d.frozenAt q i (d.values z - d.values q)‖ ≤ 2 * regularNetRadius d.radius d.shift i := by
…

Mentions: OAI.RegularPointCoordinates.regularNetRadius