Local affine-isometry chart on a smaller ball

MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball

Constructs the local ambient affine chart used in the gluing proof for open connected domains.

Statement

Suppose a set isometry f:s≃ᵢt is defined on subsets containing the ambient balls ball(c,R) and ball(f(c),R), with R>0. Then there is an ambient real affine isometry equivalence A that agrees with f at every source point lying in the smaller ball ball(c,R/8).

Assumptions

Real normed vector spaces; f is an isometry equivalence s to t; R > 0; radius-R balls about c and f(c) are contained in s and t.

Conclusion

An ambient affine isometry equivalence agrees with f on the ball about c of radius R/8.

Proof route

A radial extension centered at c is built from values of f on the sphere of radius R/8. Local midpoint preservation and positive homogeneity make the radial map globally midpoint-preserving; norm preservation then turns it into a real linear isometry. Its range contains an open ball, so it is surjective. Translating this linear equivalence produces the required affine chart, and the local radial formula proves agreement with f.

Main citations

• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.midpointLinearIsometry - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “Linear isometry induced by midpoint and norm preservation” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.radialMap_midpoint_of_norm_lt - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “Local midpoint preservation of the radial map” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.map_midpoint_of_local_of_smul_pos - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “Positive homogeneity globalizes local midpoint preservation” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.radialMap_smul_of_pos - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “Positive homogeneity of the radial map” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.radialMap - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “Radial extension map” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.radialMap_eq_sub_of_norm_lt - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “The radial map agrees locally with translated f” at the indicated step.
• _private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.norm_radialMap - The proof or construction of Local affine-isometry chart on a smaller ball uses the project declaration “The radial map preserves norms” at the indicated step.

Lean source signature (exact)

theorem exists_affineExtension_eqOn_ball
    {s : Set E} {t : Set F} (f : s ≃ᵢ t) (c : s) {R : ℝ} (hR : 0 < R)
    (hsball : ball (c : E) R ⊆ s)
    (htball : ball ((f c : t) : F) R ⊆ t) :
    ∃ A : E ≃ᵃⁱ[ℝ] F, ∀ x : s,
      (x : E) ∈ ball (c : E) (R / 8) → A (x : E) = ((f x : t) : F)

Read exact source with highlighted declaration