Affine-segment preservation on a quarter ball

MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

Upgrades local midpoint preservation to preservation of every affine segment parameter inside the quarter-ball chart.

Statement

Under the same ambient-ball hypotheses as the local midpoint theorem, if x and y lie in ball(c,R/4), then for every a in [0,1], f sends the affine point lineMap(x,y,a) to lineMap(f(x),f(y),a).

Assumptions

Real normed vector spaces; radius-R balls about c and f(c) lie in the source and target; R > 0; x,y lie in the radius-R/4 source ball; a lies in [0,1].

Conclusion

f preserves the affine combination (1-a)x + ay, with the exact subtype membership witnesses supplied in Lean.

Proof route

Restrict the domain to the convex quarter ball and view f there as a continuous map into the ambient target space. The preceding local midpoint theorem supplies midpoint preservation on that convex set. A general midpoint-to-line-map lemma then gives preservation of every segment parameter.

Proof steps

Define the inclusion of the quarter ball into s and the ambient-valued restriction g of f.
Use continuity of the inclusion and of the isometry to prove continuity of g.
Apply the quarter-ball midpoint theorem to obtain midpoint preservation for every pair of points in the restricted ball.
Invoke the continuous convex-set lemma that upgrades midpoint preservation to affine-line-map preservation on [0,1].
Unfold the local definitions to obtain the stated equality for f.

Main citations

_private.MathlibAnnex.Analysis.Normed.Affine.IsometryExtension.Local.0.MathlibAnnex.IsometryEquiv.map_lineMap_of_map_midpoint - The proof or construction of Affine-segment preservation on a quarter ball uses the project declaration “Continuous midpoint maps preserve affine segments” at the indicated step.
MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball - The proof or construction of Affine-segment preservation on a quarter ball uses the project declaration “Midpoint preservation on a quarter ball” at the indicated step.

Lean source signature (exact)

theorem map_lineMap_of_mem_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)
    (x y : s) (hx : (x : E) ∈ ball (c : E) (R / 4))
    (hy : (y : E) ∈ ball (c : E) (R / 4))
    (a : ℝ) (ha : a ∈ Icc (0 : ℝ) 1) :
    ((f ⟨AffineMap.lineMap (x : E) (y : E) a,
          hsball (ball_subset_ball (by linarith : R / 4 ≤ R)
            ((convex_ball (c : E) (R / 4)).lineMap_mem hx hy ha))⟩ : t) : F) =
      AffineMap.lineMap ((f x : t) : F) ((f y : t) : F) a

Read exact source with highlighted declaration

Exact Card identity

Stable Card ID: 0cfc0bfe5c6e6e9641207ba94e1890139d7e6a138ab41f3ea638d101cd0bfb04

Card revision: 1

Card SHA-256: 4efc62d8a56c8dfa3372c385987153dc2be7eb7c3e7d7266df28cec985605db0

Exact public projection