CoordinateEllipsoids.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The quarter-scale open-map construction supplies dyadic ellipsoids

theorem OAI.RegularPointCoordinates.coordinateQuarterRadius_eq_even_iterationRadius line 15
theorem OAI.RegularPointCoordinates.quarter_half_index_bounds line 21

theorem OAI.RegularPointCoordinates.ellipsoid_preimages_of_comparable_normalizations line 43

Source documentation

Comparable normalizations transfer the exact preimages to a desired frozen ellipsoid. The dyadic radius may lie between consecutive quarter scales.

theorem ellipsoid_preimages_of_comparable_normalizations
    {Ω : Set X} {f : X → E} {r C ρ : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hcont : ContinuousOn f Ω) (j : ℕ) (x : X) (T : E ≃L[ℝ] E)
    (hρ : 0 < ρ)
    (hlower : ρ ≤ coordinateQuarterRadius r j)
    (hupper : coordinateQuarterRadius r j ≤ 2 * ρ)
    (hball : Metric.ball x (2 * coordinateQuarterRadius r j) ⊆ Ω)
    (hcompare : ∀ w, ‖d.normalization j x w‖ ≤ 2 * ‖T w‖) :
    ∀ P : E, ‖T (P - f x)‖ < ρ / 32 →
      ∃ y ∈ Ω, dist x y < ρ ∧ f y = P := by
…

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

theorem OAI.RegularPointCoordinates.even_iteration_ellipsoid_preimages line 70

Source documentation

Even dyadic scales are exactly the quarter scales used in the Cauchy correction argument. This version has no scale-comparability premise.

theorem even_iteration_ellipsoid_preimages
    {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hcont : ContinuousOn f Ω) (j : ℕ) (x : X) (T : E ≃L[ℝ] E)
    (hball : Metric.ball x (2 * iterationRadius r (2 * j)) ⊆ Ω)
    (hcompare : ∀ w, ‖d.normalization j x w‖ ≤ 2 * ‖T w‖) :
    ∀ P : E, ‖T (P - f x)‖ < iterationRadius r (2 * j) / 32 →
      ∃ y ∈ Ω, dist x y < iterationRadius r (2 * j) ∧ f y = P := by
…

Mentions: OAI.RegularPointCoordinates.OpenCoordinateData, OAI.RegularPointCoordinates.iterationRadius

theorem OAI.RegularPointCoordinates.dyadic_ellipsoid_preimages line 92

Source documentation

The working ball of radius 4 r_i suffices for every dyadic index, including the odd indices between successive quarter scales.

theorem dyadic_ellipsoid_preimages
    {Ω : Set X} {f : X → E} {r C : ℝ}
    (d : OpenCoordinateData Ω f r C) (hr : 0 < r) (hC : 0 ≤ C)
    (hcont : ContinuousOn f Ω) (i : ℕ) (x : X) (T : E ≃L[ℝ] E)
    (hball : Metric.ball x (4 * iterationRadius r i) ⊆ Ω)
    (hcompare : ∀ w, ‖d.normalization (i / 2) x w‖ ≤ 2 * ‖T w‖) :
    ∀ P : E, ‖T (P - f x)‖ < iterationRadius r i / 32 →
      ∃ y ∈ Ω, dist x y < iterationRadius r i ∧ f y = P := by
…

Mentions: OAI.RegularPointCoordinates.OpenCoordinateData, OAI.RegularPointCoordinates.iterationRadius