Metric balls and spheres in normed spaces

This file records how the affine map y ↦ c • y +ᵥ x pulls metric balls, closed balls, and spheres back to their corresponding sets centered at zero.

The preimage formulas need only [Norm 𝕜] [SMul 𝕜 E] [NormSMulClass 𝕜 E] on the scalars and their action. Balls and closed balls require 0 < ‖c‖; spheres only require ‖c‖ ≠ 0. Over a normed division ring these conditions are equivalent to c ≠ 0, via norm_pos_iff and norm_ne_zero_iff respectively.

The range formula identifies a positive real scaling of the unit sphere with the sphere of that radius in a seminormed real vector space. Two points on a sphere of nonzero radius centered at zero lie on the same line exactly when they are equal or antipodal.

@[simp]

theorem TauCeti.preimage_smul_vadd_ball_norm {𝕜 : Type u_1} {E : Type u_2} {P : Type u_3} [Norm 𝕜] [SeminormedAddCommGroup E] [SMul 𝕜 E] [NormSMulClass 𝕜 E] [PseudoMetricSpace P] [NormedAddTorsor E P] (x : P) {c : 𝕜} (hc : 0 < ‖c‖) (r : ℝ) : (fun (y : E) => c • y +ᵥ x) ⁻¹' Metric.ball x (‖c‖ * r) = Metric.ball 0 r

The affine normalization map y ↦ c • y +ᵥ x pulls the ball Metric.ball x (‖c‖ * r) back to Metric.ball 0 r, for a scale c of positive norm.

@[simp]

theorem TauCeti.preimage_smul_vadd_closedBall {𝕜 : Type u_1} {E : Type u_2} {P : Type u_3} [Norm 𝕜] [SeminormedAddCommGroup E] [SMul 𝕜 E] [NormSMulClass 𝕜 E] [PseudoMetricSpace P] [NormedAddTorsor E P] (x : P) {c : 𝕜} (hc : 0 < ‖c‖) (r : ℝ) : (fun (y : E) => c • y +ᵥ x) ⁻¹' Metric.closedBall x (‖c‖ * r) = Metric.closedBall 0 r

The affine map y ↦ c • y +ᵥ x pulls the closed ball of radius ‖c‖ * r about x back to the closed ball of radius r about 0.

@[simp]

theorem TauCeti.preimage_smul_vadd_sphere {𝕜 : Type u_1} {E : Type u_2} {P : Type u_3} [Norm 𝕜] [SeminormedAddCommGroup E] [SMul 𝕜 E] [NormSMulClass 𝕜 E] [PseudoMetricSpace P] [NormedAddTorsor E P] (x : P) {c : 𝕜} (hc : ‖c‖ ≠ 0) (r : ℝ) : (fun (y : E) => c • y +ᵥ x) ⁻¹' Metric.sphere x (‖c‖ * r) = Metric.sphere 0 r

The affine map y ↦ c • y +ᵥ x pulls the sphere of radius ‖c‖ * r about x back to the sphere of radius r about 0, provided ‖c‖ ≠ 0.

@[simp]

theorem TauCeti.range_smul_coe_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) : (Set.range fun (u : ↑(Metric.sphere 0 1)) => c • ↑u) = Metric.sphere 0 c

The image of the unit sphere under scaling by a positive real c is the sphere of radius c.

@[simp]

theorem TauCeti.coe_mem_span_singleton_iff {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : r ≠ 0) {x p : ↑(Metric.sphere 0 r)} : ↑x ∈ ℝ ∙ ↑p ↔ x = p ∨ x = -p

Two points of a sphere of nonzero radius centered at zero in a real seminormed space lie on the same line exactly when they are equal or antipodal.

theorem TauCeti.compl_singleton_inter_compl_singleton_neg_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : {p}ᶜ ∩ {-p}ᶜ = {x : ↑(Metric.sphere 0 1) | ↑x ∉ ℝ ∙ ↑p}

The unit sphere minus p and -p is the set of its points off the line through p.

theorem TauCeti.norm_inv_smul_sub_lt_one {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {c z : E} {R : ℝ} (hR : 0 < R) (hz : ‖z - c‖ < R) : ‖R⁻¹ • (z - c)‖ < 1

A point inside a ball of positive radius has normalized coordinate in the unit ball.

theorem TauCeti.norm_inv_smul_sub_eq_one_of_norm_sub_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {c z : E} {R : ℝ} (hR : 0 < R) (hz : ‖z - c‖ = R) : ‖R⁻¹ • (z - c)‖ = 1

A boundary point of a ball of positive radius has unit norm in normalized coordinates.