RegularOpenCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Constructive openness of the actual harmonic coordinates

theorem OAI.RegularPointCoordinates.pointed_approximation_restrict_four line 16

Source documentation

A centered four-ball approximation restricts to the unit ball when the error is at most half the new tolerance.

theorem pointed_approximation_restrict_four {X E : Type*}
    [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]
    {x : X} {r epsilon : ℝ} {g : X → E} (hr : 0 < r)
    (hepsilon : epsilon ≤ 1 / 2048) (hzero : g x = 0)
    (hg : IsPointedApproximation x 0 r 4 epsilon g) :
    IsPointedApproximation x 0 r 1 (1 / 1024) g := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.regular_quarter_radius line 36
def OAI.RegularPointCoordinates.RegularBilinearData.quarterFrame line 54
Source documentation
Quarter-scale pointwise coordinate changes, extended outside the working neighborhood only to give the total function required by the open-map API.
```
def quarterFrame (i : ℕ) (q : X) : Euclidean n ≃L[ℝ] Euclidean n := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.RegularBilinearData.quarterFrame_eq line 59

def OAI.RegularPointCoordinates.regular_open_coordinate_data line 67

Source documentation

The actual regular-neighborhood harmonic coordinates satisfy every hypothesis of the constructive open-map argument.

def regular_open_coordinate_data {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 : 0 ≤ zeta) (hzetaSmall : zeta ≤ 1 / 2048)
    (hgramSmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 4 : ℝ) ^ n)⁻¹) * zeta) ≤ 3 / 4) :
    OpenCoordinateData (ball base (e.heat.radius / 1024)) e.heat.values
      (e.heat.radius / 128) (2 * (n : ℝ)) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.OpenCoordinateData