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.

source

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

source

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

source

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

source

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

source

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

source

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)

source

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‖

source

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)

source

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)

source

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 Metric.Bounded.smul for a similar lemma about an isometric action.

source

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.

source

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.

source

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, dist x y = b * dist x z ∧ dist y z = a * dist x z

source

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, dist x y ≤ δ ∧ dist y z ≤ ε

source

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, dist x y ≤ δ ∧ dist y z < ε

source

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, dist x y < δ ∧ dist y z ≤ ε

source

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, dist x y < δ ∧ dist y z < ε

source

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

source

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

source

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

source

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

source

@[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 δ

source

@[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

source

@[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

source

@[simp]

theorem closure_thickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ} (hδ : 0 < δ) (s : Set E) :

closure (Metric.thickening δ s) = Metric.cthickening δ s

source

@[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 δ

source

@[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

source

@[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

source

@[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 (ε + δ)

source

@[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 (ε + δ)

source

@[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 (ε + δ)

source

@[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 (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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) (ε + δ)

source

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)

source

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‖

source

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.

source

@[simp]

theorem NormedSpace.sphere_nonempty {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {r : ℝ} :

Set.Nonempty (Metric.sphere x r) ↔ 0 ≤ r

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

source

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)

source

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.

source

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.