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 : ℝ)
:
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)
:
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
disjoint_ball_ball_iff
{E : Type u_2}
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
{x 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 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 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 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 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 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 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 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 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 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 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 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.