PairGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Pair segments from harmonic-coordinate ellipsoids

The final analytic argument only needs a coordinate segment to stay in the larger working region, with comparable frozen metrics along it. Central ellipsoid containment and the nearby-center comparison imply precisely those facts. The source of the final chart may be a smaller open subset.

theorem OAI.RegularPointCoordinates.norm_frozen_sub_le_of_mem_segment line 20

theorem OAI.RegularPointCoordinates.segment_geometry_of_ellipsoid line 34

Source documentation

Every point of the short coordinate segment has a preimage in the nearby metric ball. Thus the nearby-center bound applies along the whole segment, without any differentiability of the frozen metrics.

theorem segment_geometry_of_ellipsoid
    {X : Type*} [MetricSpace X] (u : X → E) (frozen : E → E ≃L[ℝ] E)
    {Ω : Set E} {W : Set X} {x z : X} {r c G : ℝ}
    (hend : ‖frozen (u x) (u z - u x)‖ < c * r)
    (hball : ∀ P : E, ‖frozen (u x) (P - u x)‖ < c * r →
      P ∈ Ω ∧ ∃ y ∈ W, dist x y < r ∧ u y = P)
    (hnear : ∀ y ∈ W, dist x y < r → ∀ w : E,
      ‖frozen (u y) w‖ ≤ G * ‖frozen (u x) w‖) :
    segment ℝ (u x) (u z) ⊆ Ω ∧ ∀ P ∈ segment ℝ (u x) (u z),
      ‖frozen P (u z - u x)‖ ≤ G * ‖frozen (u x) (u z - u x)‖ := by
…

theorem OAI.RegularPointCoordinates.iterationPairGeometry_of_ellipsoids line 58

Source documentation

All ingredients of the final pair geometry follow from endpoint separation, ellipsoid containment, nearby metric comparison, and a diameter bound on the small source domain.

theorem iterationPairGeometry_of_ellipsoids
    {X : Type*} [MetricSpace X] (u : X → E) (D W : Set X)
    (Ω : Set E) (frozen : ℕ → E → E ≃L[ℝ] E)
    {r0 T B G c : ℝ} (hr0 : 0 < r0) (hT : 1 ≤ T) (hB : 1 ≤ B) (hG : 1 ≤ G)
    (hc : 0 < c) (hmargin : G < c * iterationPairMultiplier T B G)
    (hdiam : ∀ x ∈ D, ∀ z ∈ D, iterationPairMultiplier T B G * dist x z ≤ r0)
    (hend : ∀ i x, x ∈ D → ∀ z, z ∈ D → x ≠ z →
      iterationPairMultiplier T B G * dist x z ≤ iterationRadius r0 i →
      iterationRadius r0 i ≤ 2 * iterationPairMultiplier T B G * dist x z →
      G⁻¹ * dist x z ≤ ‖frozen i (u x) (u z - u x)‖ ∧
      ‖frozen i (u x) (u z - u x)‖ ≤ G * dist x z)
    (hball : ∀ i x, x ∈ D → ∀ P : E,
…

Mentions: OAI.RegularPointCoordinates.iterationPairMultiplier, OAI.RegularPointCoordinates.iterationRadius