Euclidean coordinates on a closed ball in a finite-dimensional subspace

A finite-dimensional subspace V of a real inner product space carries an orthonormal basis, stdOrthonormalBasis, whose coordinate map is a linear isometry onto EuclideanSpace ℝ (Fin n) for n the dimension of V. Being an isometry it carries the closed ball of V about the origin onto the Euclidean closed ball of the same radius, so the two balls are homeomorphic.

The subspace is allowed to arrive as a set s known to equal V, which is how a range of a projection presents itself, and the ball is the subtype of s cut out by the norm bound rather than Metric.closedBall in the subtype, which is how a set truncated by a norm bound presents itself.

Main definitions

• TauCeti.euclideanClosedBallHomeomorph: the closed ball of radius rho in such a subspace is homeomorphic to the closed ball of radius rho in EuclideanSpace ℝ (Fin n).

noncomputable def TauCeti.euclideanClosedBallHomeomorph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {V : Submodule ℝ E} [FiniteDimensional ℝ ↥V] (hs : s = ↑V) {n : ℕ} (hn : Module.finrank ℝ ↥V = n) (rho : ℝ) : ↑{v : ↑s | ‖↑v‖ ≤ rho} ≃ₜ ↑(Metric.closedBall 0 rho)

The closed ball of radius rho in a subspace V of E, presented through a set s equal to that subspace, is homeomorphic to the closed ball of the same radius in the Euclidean space of the dimension of V.

Equations

• TauCeti.euclideanClosedBallHomeomorph hs hn rho = ((Homeomorph.setCongr hs).subtype ⋯).trans (((stdOrthonormalBasis ℝ ↥V).reindex (finCongr hn)).repr.toHomeomorph.subtype ⋯)