Properties of pointwise scalar multiplication of sets in normed spaces.

We explore the relationships between scalar multiplication of sets in vector spaces, and the norm. Notably, we express arbitrary balls as rescaling of other balls, and we show that the multiplication of bounded sets remain bounded.

theorem ediam_smul_le {𝕜 : Type u_1} {E : Type u_2} [SeminormedAddCommGroup 𝕜] [SeminormedAddCommGroup E] [SMulZeroClass 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (s : Set E) : EMetric.diam (c • s) ≤ ‖c‖₊ • EMetric.diam s

theorem ediam_smul₀ {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (s : Set E) : EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s

theorem diam_smul₀ {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (x : Set E) : Metric.diam (c • x) = ‖c‖ * Metric.diam x

theorem infEdist_smul₀ {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (s : Set E) (x : E) : EMetric.infEdist (c • x) (c • s) = ‖c‖₊ • EMetric.infEdist x s

theorem infDist_smul₀ {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (s : Set E) (x : E) : Metric.infDist (c • x) (c • s) = ‖c‖ * Metric.infDist x s

theorem smul_ball {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • Metric.ball x r = Metric.ball (c • x) (‖c‖ * r)

theorem smul_unitBall {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : c ≠ 0) : c • Metric.ball 0 1 = Metric.ball 0 ‖c‖

theorem smul_sphere' {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)

theorem smul_closedBall' {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • Metric.closedBall x r = Metric.closedBall (c • x) (‖c‖ * r)

theorem set_smul_sphere_zero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set 𝕜} (hs : 0 ∉ s) (r : ℝ) : s • Metric.sphere 0 r = (fun (x : E) => ‖x‖) ⁻¹' ((fun (x : 𝕜) => ‖x‖ * r) '' s)

theorem Bornology.IsBounded.smul₀ {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (hs : Bornology.IsBounded s) (c : 𝕜) : Bornology.IsBounded (c • s)

Image of a bounded set in a normed space under scalar multiplication by a constant is bounded. See also Bornology.IsBounded.smul for a similar lemma about an isometric action.

theorem eventually_singleton_add_smul_subset {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} (hs : Bornology.IsBounded s) {u : Set E} (hu : u ∈ nhds x) : ∀ᶠ (r : 𝕜) in nhds 0, {x} + r • s ⊆ u

If s is a bounded set, then for small enough r, the set {x} + r • s is contained in any fixed neighborhood of x.

theorem smul_unitBall_of_pos {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) : r • Metric.ball 0 1 = Metric.ball 0 r

In a real normed space, the image of the unit ball under scalar multiplication by a positive constant r is the ball of radius r.

theorem Ioo_smul_sphere_zero {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {r : ℝ} (ha : 0 ≤ a) (hr : 0 < r) : Set.Ioo a b • Metric.sphere 0 r = Metric.ball 0 (b * r) \ Metric.closedBall 0 (a * r)

theorem exists_dist_eq {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (z : E) {a : ℝ} {b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : ∃ (y : E), dist x y = b * dist x z ∧ dist y z = a * dist x z

theorem exists_dist_le_le {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {z : E} {δ : ℝ} {ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (h : dist x z ≤ ε + δ) : ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε

theorem exists_dist_le_lt {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {z : E} {δ : ℝ} {ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 < ε) (h : dist x z < ε + δ) : ∃ (y : E), dist x y ≤ δ ∧ dist y z < ε

theorem exists_dist_lt_le {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {z : E} {δ : ℝ} {ε : ℝ} (hδ : 0 < δ) (hε : 0 ≤ ε) (h : dist x z < ε + δ) : ∃ (y : E), dist x y < δ ∧ dist y z ≤ ε

theorem exists_dist_lt_lt {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {z : E} {δ : ℝ} {ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) (h : dist x z < ε + δ) : ∃ (y : E), dist x y < δ ∧ dist y z < ε

theorem disjoint_ball_ball_iff {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {y : E} {δ : ℝ} {ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) : Disjoint (Metric.ball x δ) (Metric.ball y ε) ↔ δ + ε ≤ dist x y

theorem disjoint_ball_closedBall_iff {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {y : E} {δ : ℝ} {ε : ℝ} (hδ : 0 < δ) (hε : 0 ≤ ε) : Disjoint (Metric.ball x δ) (Metric.closedBall y ε) ↔ δ + ε ≤ dist x y

theorem disjoint_closedBall_ball_iff {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {y : E} {δ : ℝ} {ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 < ε) : Disjoint (Metric.closedBall x δ) (Metric.ball y ε) ↔ δ + ε ≤ dist x y

theorem disjoint_closedBall_closedBall_iff {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {y : E} {δ : ℝ} {ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) : Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε) ↔ δ + ε < dist x y

@[simp]

theorem infEdist_thickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} (hδ : 0 < δ) (s : Set E) (x : E) : EMetric.infEdist x (Metric.thickening δ s) = EMetric.infEdist x s - ENNReal.ofReal δ

@[simp]

theorem thickening_thickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (s : Set E) : Metric.thickening ε (Metric.thickening δ s) = Metric.thickening (ε + δ) s

@[simp]

theorem cthickening_thickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 < δ) (s : Set E) : Metric.cthickening ε (Metric.thickening δ s) = Metric.cthickening (ε + δ) s

@[simp]

theorem closure_thickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} (hδ : 0 < δ) (s : Set E) : closure (Metric.thickening δ s) = Metric.cthickening δ s

@[simp]

theorem infEdist_cthickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (δ : ℝ) (s : Set E) (x : E) : EMetric.infEdist x (Metric.cthickening δ s) = EMetric.infEdist x s - ENNReal.ofReal δ

@[simp]

theorem thickening_cthickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) (s : Set E) : Metric.thickening ε (Metric.cthickening δ s) = Metric.thickening (ε + δ) s

@[simp]

theorem cthickening_cthickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : Set E) : Metric.cthickening ε (Metric.cthickening δ s) = Metric.cthickening (ε + δ) s

@[simp]

theorem thickening_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (x : E) : Metric.thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)

@[simp]

theorem thickening_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) (x : E) : Metric.thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)

@[simp]

theorem cthickening_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 < δ) (x : E) : Metric.cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)

@[simp]

theorem cthickening_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (x : E) : Metric.cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)

theorem ball_add_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (a : E) (b : E) : Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

theorem ball_sub_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (a : E) (b : E) : Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

theorem ball_add_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) (a : E) (b : E) : Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)

theorem ball_sub_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) (a : E) (b : E) : Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)

theorem closedBall_add_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 < δ) (a : E) (b : E) : Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

theorem closedBall_sub_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 < δ) (a : E) (b : E) : Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

theorem closedBall_add_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} [ProperSpace E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a : E) (b : E) : Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)

theorem closedBall_sub_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} {ε : ℝ} [ProperSpace E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a : E) (b : E) : Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)

theorem smul_closedBall {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) : c • Metric.closedBall x r = Metric.closedBall (c • x) (‖c‖ * r)

theorem smul_closedUnitBall {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) : c • Metric.closedBall 0 1 = Metric.closedBall 0 ‖c‖

theorem smul_closedUnitBall_of_nonneg {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) : r • Metric.closedBall 0 1 = Metric.closedBall 0 r

In a real normed space, the image of the unit closed ball under multiplication by a nonnegative number r is the closed ball of radius r with center at the origin.

@[simp]

theorem NormedSpace.sphere_nonempty {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {r : ℝ} : (Metric.sphere x r).Nonempty ↔ 0 ≤ r

In a nontrivial real normed space, a sphere is nonempty if and only if its radius is nonnegative.

theorem smul_sphere {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) : c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)

theorem affinity_unitBall {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) (x : E) : x +ᵥ r • Metric.ball 0 1 = Metric.ball x r

Any ball Metric.ball x r, 0 < r is the image of the unit ball under fun y ↦ x + r • y.

theorem affinity_unitClosedBall {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (x : E) : x +ᵥ r • Metric.closedBall 0 1 = Metric.closedBall x r

Any closed ball Metric.closedBall x r, 0 ≤ r is the image of the unit closed ball under fun y ↦ x + r • y.