Rays leaving the closed unit ball

Let x and y be distinct points of a real inner product space E, with x in the closed unit ball. The ray t ↦ x + t • (x - y), t ≥ 0, starts at x and points away from y; it meets the unit sphere at the time TauCeti.unitSphereRayTime y x, the larger root of the quadratic equation ‖x + t • (x - y)‖ ^ 2 = 1, which is nonnegative. That root is given by an explicit formula, so it depends continuously on x and y, and it vanishes when x already lies on the unit sphere and y lies in the closed ball.

For a self-map f of the closed unit ball without fixed points, following the ray from f x through x therefore gives a retraction of the ball onto its boundary sphere (ContinuousMap.closedBallRayRetraction). This is the geometric half of the classical deduction of Brouwer's fixed-point theorem from the no-retraction theorem.

Main definitions

• TauCeti.unitSphereRayTime y x: the time at which the ray from y through x meets the unit sphere, beyond x.
• ContinuousMap.closedBallRayRetraction f hf: the retraction of the closed unit ball onto the unit sphere along the rays from f x through x.

Main results

• TauCeti.norm_add_unitSphereRayTime_smul_sub: x + unitSphereRayTime y x • (x - y) lies on the unit sphere when ‖x‖ ≤ 1 and x ≠ y.
• TauCeti.unitSphereRayTime_eq_zero: the time vanishes when x lies on the unit sphere and ‖y‖ ≤ 1.
• ContinuousMap.closedBallRayRetraction_apply_of_mem_sphere: the retraction fixes the unit sphere.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Corollary 2.15.

noncomputable def TauCeti.unitSphereRayTime {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (y x : E) : ℝ

The time t ≥ 0 at which the ray t ↦ x + t • (x - y) from x, pointing away from y, meets the unit sphere: the larger root of ‖x + t • (x - y)‖ ^ 2 = 1, a root when ‖x‖ ≤ 1 and x ≠ y (TauCeti.norm_add_unitSphereRayTime_smul_sub).

theorem TauCeti.unitSphereRayTime_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (y x : E) : unitSphereRayTime y x = (√(inner ℝ x (x - y) ^ 2 + ‖x - y‖ ^ 2 * (1 - ‖x‖ ^ 2)) - inner ℝ x (x - y)) / ‖x - y‖ ^ 2

The quadratic formula for the time at which the ray from y through x meets the unit sphere.

theorem TauCeti.unitSphereRayTime_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (y : E) {x : E} (hx : ‖x‖ ≤ 1) : 0 ≤ unitSphereRayTime y x

The time at which a ray from a point of the closed unit ball meets the unit sphere is nonnegative.

@[simp]

theorem TauCeti.norm_add_unitSphereRayTime_smul_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y : E} (hxy : x ≠ y) (hx : ‖x‖ ≤ 1) : ‖x + unitSphereRayTime y x • (x - y)‖ = 1

The ray from y through a point x ≠ y of the closed unit ball meets the unit sphere at time TauCeti.unitSphereRayTime y x.

@[simp]

theorem TauCeti.unitSphereRayTime_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ ≤ 1) : unitSphereRayTime y x = 0

A ray from a point x of the unit sphere pointing away from a point y of the closed unit ball leaves the ball at once: when ‖x‖ = 1 and ‖y‖ ≤ 1, the time TauCeti.unitSphereRayTime y x vanishes.

theorem Continuous.unitSphereRayTime {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2} [TopologicalSpace X] {f g : X → E} (hf : Continuous f) (hg : Continuous g) (h : ∀ (z : X), g z ≠ f z) : Continuous fun (z : X) => TauCeti.unitSphereRayTime (f z) (g z)

The formula TauCeti.unitSphereRayTime (f z) (g z) depends continuously on z when f and g are continuous and g z ≠ f z everywhere. Where moreover ‖g z‖ ≤ 1, it is the time at which the ray from f z through g z meets the unit sphere.

noncomputable def ContinuousMap.closedBallRayRetraction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : C(↑(Metric.closedBall 0 1), ↑(Metric.closedBall 0 1))) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), f x ≠ x) : C(↑(Metric.closedBall 0 1), ↑(Metric.sphere 0 1))

The ray retraction of the closed unit ball onto the unit sphere determined by a self-map f of the ball without fixed points: a point x goes to the point where the ray from f x through x meets the unit sphere. It fixes the unit sphere (ContinuousMap.closedBallRayRetraction_apply_of_mem_sphere).

@[simp]

theorem ContinuousMap.coe_closedBallRayRetraction_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : C(↑(Metric.closedBall 0 1), ↑(Metric.closedBall 0 1))) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), f x ≠ x) (x : ↑(Metric.closedBall 0 1)) : ↑((f.closedBallRayRetraction hf) x) = ↑x + TauCeti.unitSphereRayTime ↑(f x) ↑x • (↑x - ↑(f x))

The ray retraction sends x to x + t • (x - f x), with t the time at which the ray from f x through x meets the unit sphere.

theorem ContinuousMap.closedBallRayRetraction_apply_of_mem_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : C(↑(Metric.closedBall 0 1), ↑(Metric.closedBall 0 1))) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), f x ≠ x) {x : ↑(Metric.closedBall 0 1)} (hx : ↑x ∈ Metric.sphere 0 1) : ↑((f.closedBallRayRetraction hf) x) = ↑x

The ray retraction of the closed unit ball fixes the points of the unit sphere.