OpenCoordinates.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Constructive openness of approximate Euclidean coordinates

The hypotheses below are the scale-dependent approximation and nearby-metric estimates used in co:open-coordinates. Exact preimages and openness are proved by a convergent correction process; neither is an input.

theorem OAI.RegularPointCoordinates.exists_preimage_of_quarter_corrections line 29

Source documentation

A quarter-scale correction process stays strictly inside the working ball and converges to an exact preimage. The predicate records the current residual in a possibly changing norm.

theorem exists_preimage_of_quarter_corrections
    {f : X → Y} {x₀ : X} {P : Y} {r M : ℝ} (hr : 0 < r)
    (control : ℕ → X → Prop) (hzero : control 0 x₀)
    (hstep : ∀ n x, dist x x₀ < r / 2 → control n x →
      ∃ y, dist y x ≤ r * (1 / 4 : ℝ) ^ n / 8 ∧ control (n + 1) y)
    (hresidual : ∀ n x, dist x x₀ < r / 2 → control n x →
      dist (f x) P ≤ M * (r * (1 / 4 : ℝ) ^ n))
    (hcont : ContinuousOn f (Metric.ball x₀ (r / 2))) :
    ∃ y, dist y x₀ ≤ r / 6 ∧ f y = P := by
…

theorem OAI.RegularPointCoordinates.euclidean_correspondence_of_pointed_approximation line 104

Source documentation

Pointed metric approximation and uniform closeness of the normalized coordinate map supply the Euclidean correspondence needed below.

theorem euclidean_correspondence_of_pointed_approximation
    {f g : X → E} {x : X} {r : ℝ} (hr : 0 < r) (N : E ≃L[ℝ] E)
    (hg : IsPointedApproximation x 0 r 1 (1 / 1024) g)
    (hclose : ∀ y, dist y x ≤ r →
      ‖r⁻¹ • N (f y - f x) - g y‖ ≤ 1 / 1024) :
    ∀ a : E, ‖a‖ < r / 16 →
      ∃ y, dist y x ≤ ‖a‖ + r / 256 ∧ ‖N (f y - f x) - a‖ ≤ r / 256 := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.approximate_preimage_of_euclidean_correspondence line 143

Source documentation

The approximate correction hypothesis follows directly from a normalized Euclidean correspondence: test the correspondence at the normalized target. The displacement error and coordinate error are both explicit.

theorem approximate_preimage_of_euclidean_correspondence
    {f : X → E} {x : X} {R : ℝ} (N : E ≃L[ℝ] E)
    (hcorrespondence : ∀ a : E, ‖a‖ < R / 16 →
      ∃ y, dist y x ≤ ‖a‖ + R / 256 ∧ ‖N (f y - f x) - a‖ ≤ R / 256)
    {P : E} (hP : ‖N (P - f x)‖ < R / 16) :
    ∃ y, dist y x ≤ 17 / 256 * R ∧ ‖N (P - f y)‖ ≤ R / 256 := by
…

theorem OAI.RegularPointCoordinates.exists_preimage_of_normalized_approximation line 158

Source documentation

Concrete constants for the correction argument. N n x represents the inverse square root of the Gram matrix at the current scale and center.

theorem exists_preimage_of_normalized_approximation
    {f : X → E} {x₀ : X} {P : E} {r C : ℝ} (hr : 0 < r) (hC : 0 ≤ C)
    (N : ℕ → X → E ≃L[ℝ] E)
    (hzero : ‖N 0 x₀ (P - f x₀)‖ < r / 16)
    (happrox : ∀ n x, dist x x₀ < r / 2 →
      ‖N n x (P - f x)‖ < r * (1 / 4 : ℝ) ^ n / 16 →
      ∃ y, dist y x ≤ 17 / 256 * (r * (1 / 4 : ℝ) ^ n) ∧
        ‖N n x (P - f y)‖ ≤ r * (1 / 4 : ℝ) ^ n / 256)
    (hnear : ∀ n x y, dist x x₀ < r / 2 → dist y x ≤ r * (1 / 4 : ℝ) ^ n / 8 →
      ∀ w, ‖N (n + 1) y w‖ ≤ 2 * ‖N n x w‖)
    (hupper : ∀ n x, dist x x₀ < r / 2 → ∀ w, ‖w‖ ≤ C * ‖N n x w‖)
    (hcont : ContinuousOn f (Metric.ball x₀ (r / 2))) :
…

def OAI.RegularPointCoordinates.coordinateQuarterRadius line 198
Source documentation
The quarter scales used in the constructive surjectivity argument.
```
noncomputable def coordinateQuarterRadius (r : ℝ) (i : ℕ) : ℝ := r * (1 / 4 : ℝ) ^ i
```
theorem OAI.RegularPointCoordinates.coordinateQuarterRadius_add line 200
structure OAI.RegularPointCoordinates.OpenCoordinateData line 208
Source documentation
Raw approximation data: small normalized targets have approximate preimages, and changing the center and going down one quarter-scale costs at most two in the residual norm. All conditions are local to the open domain.
```
structure OpenCoordinateData (Ω : Set X) (f : X → E) (r C : ℝ) where
…
```

def OAI.RegularPointCoordinates.OpenCoordinateData.of_pointed_approximation line 223

Source documentation

Build the approximation data directly from pointed metric approximations and uniform closeness of the normalized coordinate functions.

def of_pointed_approximation {Ω : Set X} {f : X → E} {r C : ℝ} (hr : 0 < r)
    (N : ℕ → X → E ≃L[ℝ] E)
    (hcharts : ∀ i x, x ∈ Ω → Metric.closedBall x (coordinateQuarterRadius r i) ⊆ Ω →
      ∃ g : X → E,
        IsPointedApproximation x 0 (coordinateQuarterRadius r i) 1 (1 / 1024) g ∧
        ∀ y, dist y x ≤ coordinateQuarterRadius r i →
          ‖(coordinateQuarterRadius r i)⁻¹ • N i x (f y - f x) - g y‖ ≤ 1 / 1024)
    (hnear : ∀ i x y, x ∈ Ω → y ∈ Ω →
      dist y x ≤ coordinateQuarterRadius r i / 8 →
      ∀ w, ‖N (i + 1) y w‖ ≤ 2 * ‖N i x w‖)
    (hupper : ∀ i x, x ∈ Ω → ∀ w, ‖w‖ ≤ C * ‖N i x w‖) :
    OpenCoordinateData Ω f r C where
…

Mentions: OAI.RegularPointCoordinates.coordinateQuarterRadius, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.OpenCoordinateData

theorem OAI.RegularPointCoordinates.OpenCoordinateData.exists_preimage line 247

Source documentation

An exact ellipsoid is contained in the image of the interior ball. The stronger one-sixth radius records the margin left by the Cauchy construction.

theorem exists_preimage {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hcont : ContinuousOn f Ω) (i : ℕ) (x₀ : X)
    (hball : Metric.ball x₀ (2 * coordinateQuarterRadius r i) ⊆ Ω)
    {P : E} (hP : ‖d.normalization i x₀ (P - f x₀)‖ <
      coordinateQuarterRadius r i / 16) :
    ∃ y, dist y x₀ ≤ coordinateQuarterRadius r i / 6 ∧ f y = P := by
…

Mentions: OAI.RegularPointCoordinates.OpenCoordinateData, OAI.RegularPointCoordinates.coordinateQuarterRadius

theorem OAI.RegularPointCoordinates.OpenCoordinateData.localized_surjectivity line 291

Source documentation

Approximation on all quarter-scales gives arbitrarily localized exact preimages. The target neighborhood is an explicit frozen ellipsoid.

theorem localized_surjectivity {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hΩ : IsOpen Ω) (hcont : ContinuousOn f Ω) {x : X} (hx : x ∈ Ω)
    {δ : ℝ} (hδ : 0 < δ) :
    ∃ i, ∀ P, ‖d.normalization i x (P - f x)‖ < coordinateQuarterRadius r i / 16 →
      ∃ y ∈ Ω, dist y x < δ ∧ f y = P := by
…

Mentions: OAI.RegularPointCoordinates.OpenCoordinateData, OAI.RegularPointCoordinates.coordinateQuarterRadius

theorem OAI.RegularPointCoordinates.OpenCoordinateData.isOpenMap line 321
Source documentation
The restriction of the coordinates to the open working domain is an open map. This uses exact preimages, without any invariance-of-domain input.
```
theorem isOpenMap {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hΩ : IsOpen Ω) (hcont : ContinuousOn f Ω) :
    IsOpenMap (fun x : Ω => f x) := by
…
```
Mentions: OAI.RegularPointCoordinates.OpenCoordinateData
theorem OAI.RegularPointCoordinates.OpenCoordinateData.isOpenEmbedding line 345
Source documentation
Once separation has been proved, the constructive open map is an open embedding, hence a homeomorphism onto its open image.
```
theorem isOpenEmbedding {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hΩ : IsOpen Ω) (hcont : ContinuousOn f Ω) (hinj : Set.InjOn f Ω) :
    Topology.IsOpenEmbedding (fun x : Ω => f x) := by
…
```
Mentions: OAI.RegularPointCoordinates.OpenCoordinateData

def OAI.RegularPointCoordinates.OpenCoordinateData.homeomorph line 356

Source documentation

The resulting homeomorphism retains the original coordinate values.

noncomputable def homeomorph {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hΩ : IsOpen Ω) (hcont : ContinuousOn f Ω) (hinj : Set.InjOn f Ω) :
    Ω ≃ₜ Set.range (fun x : Ω => f x) :=
…

Mentions: OAI.RegularPointCoordinates.OpenCoordinateData

theorem OAI.RegularPointCoordinates.OpenCoordinateData.isOpen_range line 362

theorem OAI.RegularPointCoordinates.injOn_of_normalized_separation line 373

Source documentation

A normalized distance approximation with error at most half the pair's distance separates the pair. The scale may depend on both points.

theorem injOn_of_normalized_separation {Ω : Set X} {f : X → E}
    (N : ℕ → X → E ≃L[ℝ] E)
    (hsep : ∀ x ∈ Ω, ∀ z ∈ Ω, x ≠ z → ∃ i,
      |‖N i x (f z - f x)‖ - dist x z| ≤ dist x z / 2) : Set.InjOn f Ω := by
…

theorem OAI.RegularPointCoordinates.open_homeomorph_of_normalized_separation line 387

Source documentation

The complete constructive conclusion, with the homeomorphism equal to the given coordinate map and its image proved open.

theorem open_homeomorph_of_normalized_separation
    {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hΩ : IsOpen Ω) (hcont : ContinuousOn f Ω)
    (hsep : ∀ x ∈ Ω, ∀ z ∈ Ω, x ≠ z → ∃ i,
      |‖d.normalization i x (f z - f x)‖ - dist x z| ≤ dist x z / 2) :
    IsOpen (Set.range (fun x : Ω => f x)) ∧
      ∃ e : Ω ≃ₜ Set.range (fun x : Ω => f x), ∀ x, (e x).val = f x := by
…

Mentions: OAI.RegularPointCoordinates.OpenCoordinateData