Properties of pointwise scalar multiplication of sets in normed spaces. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[seminormed_add_comm_group 𝕜]
[seminormed_add_comm_group E]
[smul_zero_class 𝕜 E]
[has_bounded_smul 𝕜 E]
(c : 𝕜)
(s : set E) :
emetric.diam (c • s) ≤ ‖c‖₊ • emetric.diam s
theorem
ediam_smul₀
{𝕜 : Type u_1}
{E : Type u_2}
[normed_division_ring 𝕜]
[seminormed_add_comm_group E]
[module 𝕜 E]
[has_bounded_smul 𝕜 E]
(c : 𝕜)
(s : set E) :
emetric.diam (c • s) = ‖c‖₊ • emetric.diam s
theorem
diam_smul₀
{𝕜 : Type u_1}
{E : Type u_2}
[normed_division_ring 𝕜]
[seminormed_add_comm_group E]
[module 𝕜 E]
[has_bounded_smul 𝕜 E]
(c : 𝕜)
(x : set E) :
metric.diam (c • x) = ‖c‖ * metric.diam x
theorem
inf_edist_smul₀
{𝕜 : Type u_1}
{E : Type u_2}
[normed_division_ring 𝕜]
[seminormed_add_comm_group E]
[module 𝕜 E]
[has_bounded_smul 𝕜 E]
{c : 𝕜}
(hc : c ≠ 0)
(s : set E)
(x : E) :
emetric.inf_edist (c • x) (c • s) = ‖c‖₊ • emetric.inf_edist x s
theorem
inf_dist_smul₀
{𝕜 : Type u_1}
{E : Type u_2}
[normed_division_ring 𝕜]
[seminormed_add_comm_group E]
[module 𝕜 E]
[has_bounded_smul 𝕜 E]
{c : 𝕜}
(hc : c ≠ 0)
(s : set E)
(x : E) :
metric.inf_dist (c • x) (c • s) = ‖c‖ * metric.inf_dist x s
theorem
smul_ball
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{c : 𝕜}
(hc : c ≠ 0)
(x : E)
(r : ℝ) :
c • metric.ball x r = metric.ball (c • x) (‖c‖ * r)
theorem
smul_unit_ball
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{c : 𝕜}
(hc : c ≠ 0) :
c • metric.ball 0 1 = metric.ball 0 ‖c‖
theorem
smul_sphere'
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{c : 𝕜}
(hc : c ≠ 0)
(x : E)
(r : ℝ) :
c • metric.sphere x r = metric.sphere (c • x) (‖c‖ * r)
theorem
smul_closed_ball'
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{c : 𝕜}
(hc : c ≠ 0)
(x : E)
(r : ℝ) :
c • metric.closed_ball x r = metric.closed_ball (c • x) (‖c‖ * r)
theorem
metric.bounded.smul
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
(hs : metric.bounded s)
(c : 𝕜) :
metric.bounded (c • s)
theorem
eventually_singleton_add_smul_subset
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
(hs : metric.bounded 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_unit_ball_of_pos
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ 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
exists_dist_eq
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
(x z : E)
{a b : ℝ}
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hab : a + b = 1) :
∃ (y : E), has_dist.dist x y = b * has_dist.dist x z ∧ has_dist.dist y z = a * has_dist.dist x z
theorem
exists_dist_le_le
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x z : E}
{δ ε : ℝ}
(hδ : 0 ≤ δ)
(hε : 0 ≤ ε)
(h : has_dist.dist x z ≤ ε + δ) :
∃ (y : E), has_dist.dist x y ≤ δ ∧ has_dist.dist y z ≤ ε
theorem
exists_dist_le_lt
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x z : E}
{δ ε : ℝ}
(hδ : 0 ≤ δ)
(hε : 0 < ε)
(h : has_dist.dist x z < ε + δ) :
∃ (y : E), has_dist.dist x y ≤ δ ∧ has_dist.dist y z < ε
theorem
exists_dist_lt_le
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x z : E}
{δ ε : ℝ}
(hδ : 0 < δ)
(hε : 0 ≤ ε)
(h : has_dist.dist x z < ε + δ) :
∃ (y : E), has_dist.dist x y < δ ∧ has_dist.dist y z ≤ ε
theorem
exists_dist_lt_lt
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x z : E}
{δ ε : ℝ}
(hδ : 0 < δ)
(hε : 0 < ε)
(h : has_dist.dist x z < ε + δ) :
∃ (y : E), has_dist.dist x y < δ ∧ has_dist.dist y z < ε
theorem
disjoint_ball_ball_iff
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x y : E}
{δ ε : ℝ}
(hδ : 0 < δ)
(hε : 0 < ε) :
disjoint (metric.ball x δ) (metric.ball y ε) ↔ δ + ε ≤ has_dist.dist x y
theorem
disjoint_ball_closed_ball_iff
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x y : E}
{δ ε : ℝ}
(hδ : 0 < δ)
(hε : 0 ≤ ε) :
disjoint (metric.ball x δ) (metric.closed_ball y ε) ↔ δ + ε ≤ has_dist.dist x y
theorem
disjoint_closed_ball_ball_iff
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x y : E}
{δ ε : ℝ}
(hδ : 0 ≤ δ)
(hε : 0 < ε) :
disjoint (metric.closed_ball x δ) (metric.ball y ε) ↔ δ + ε ≤ has_dist.dist x y
theorem
disjoint_closed_ball_closed_ball_iff
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{x y : E}
{δ ε : ℝ}
(hδ : 0 ≤ δ)
(hε : 0 ≤ ε) :
disjoint (metric.closed_ball x δ) (metric.closed_ball y ε) ↔ δ + ε < has_dist.dist x y
@[simp]
theorem
inf_edist_thickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ : ℝ}
(hδ : 0 < δ)
(s : set E)
(x : E) :
emetric.inf_edist x (metric.thickening δ s) = emetric.inf_edist x s - ennreal.of_real δ
@[simp]
theorem
thickening_thickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 < δ)
(s : set E) :
metric.thickening ε (metric.thickening δ s) = metric.thickening (ε + δ) s
@[simp]
theorem
cthickening_thickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 < δ)
(s : set E) :
metric.cthickening ε (metric.thickening δ s) = metric.cthickening (ε + δ) s
@[simp]
theorem
closure_thickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ : ℝ}
(hδ : 0 < δ)
(s : set E) :
closure (metric.thickening δ s) = metric.cthickening δ s
@[simp]
theorem
inf_edist_cthickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
(δ : ℝ)
(s : set E)
(x : E) :
emetric.inf_edist x (metric.cthickening δ s) = emetric.inf_edist x s - ennreal.of_real δ
@[simp]
theorem
thickening_cthickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 ≤ δ)
(s : set E) :
metric.thickening ε (metric.cthickening δ s) = metric.thickening (ε + δ) s
@[simp]
theorem
cthickening_cthickening
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 ≤ δ)
(s : set E) :
metric.cthickening ε (metric.cthickening δ s) = metric.cthickening (ε + δ) s
@[simp]
theorem
thickening_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 < δ)
(x : E) :
metric.thickening ε (metric.ball x δ) = metric.ball x (ε + δ)
@[simp]
theorem
thickening_closed_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 ≤ δ)
(x : E) :
metric.thickening ε (metric.closed_ball x δ) = metric.ball x (ε + δ)
@[simp]
theorem
cthickening_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 < δ)
(x : E) :
metric.cthickening ε (metric.ball x δ) = metric.closed_ball x (ε + δ)
@[simp]
theorem
cthickening_closed_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 ≤ δ)
(x : E) :
metric.cthickening ε (metric.closed_ball x δ) = metric.closed_ball x (ε + δ)
theorem
ball_add_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ 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}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 < δ)
(a b : E) :
metric.ball a ε - metric.ball b δ = metric.ball (a - b) (ε + δ)
theorem
ball_add_closed_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 ≤ δ)
(a b : E) :
metric.ball a ε + metric.closed_ball b δ = metric.ball (a + b) (ε + δ)
theorem
ball_sub_closed_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 < ε)
(hδ : 0 ≤ δ)
(a b : E) :
metric.ball a ε - metric.closed_ball b δ = metric.ball (a - b) (ε + δ)
theorem
closed_ball_add_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 < δ)
(a b : E) :
metric.closed_ball a ε + metric.ball b δ = metric.ball (a + b) (ε + δ)
theorem
closed_ball_sub_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 < δ)
(a b : E) :
metric.closed_ball a ε - metric.ball b δ = metric.ball (a - b) (ε + δ)
theorem
closed_ball_add_closed_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
[proper_space E]
(hε : 0 ≤ ε)
(hδ : 0 ≤ δ)
(a b : E) :
metric.closed_ball a ε + metric.closed_ball b δ = metric.closed_ball (a + b) (ε + δ)
theorem
closed_ball_sub_closed_ball
{E : Type u_2}
[seminormed_add_comm_group E]
[normed_space ℝ E]
{δ ε : ℝ}
[proper_space E]
(hε : 0 ≤ ε)
(hδ : 0 ≤ δ)
(a b : E) :
metric.closed_ball a ε - metric.closed_ball b δ = metric.closed_ball (a - b) (ε + δ)
theorem
smul_closed_ball
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
(c : 𝕜)
(x : E)
{r : ℝ}
(hr : 0 ≤ r) :
c • metric.closed_ball x r = metric.closed_ball (c • x) (‖c‖ * r)
theorem
smul_closed_unit_ball
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
(c : 𝕜) :
c • metric.closed_ball 0 1 = metric.closed_ball 0 ‖c‖
theorem
smul_closed_unit_ball_of_nonneg
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
{r : ℝ}
(hr : 0 ≤ r) :
r • metric.closed_ball 0 1 = metric.closed_ball 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
normed_space.sphere_nonempty
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ 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}
[normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space ℝ E]
[nontrivial E]
(c : 𝕜)
(x : E)
{r : ℝ}
(hr : 0 ≤ r) :
c • metric.sphere x r = metric.sphere (c • x) (‖c‖ * r)
theorem
affinity_unit_ball
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ 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 λ y, x + r • y.
theorem
affinity_unit_closed_ball
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
{r : ℝ}
(hr : 0 ≤ r)
(x : E) :
x +ᵥ r • metric.closed_ball 0 1 = metric.closed_ball x r
Any closed ball metric.closed_ball x r, 0 ≤ r is the image of the unit closed ball under
λ y, x + r • y.