# mathlibdocumentation

analysis.normed_space.pointwise

# 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 smul_ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {c : 𝕜} (hc : c 0) (x : E) (r : ) :
c r = metric.ball (c x) (c * r)
theorem smul_unit_ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {c : 𝕜} (hc : c 0) :
c 1 =
theorem smul_sphere' {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {c : 𝕜} (hc : c 0) (x : E) (r : ) :
c = metric.sphere (c x) (c * r)
theorem smul_closed_ball' {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {c : 𝕜} (hc : c 0) (x : E) (r : ) :
theorem metric.bounded.smul {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {s : set E} (hs : metric.bounded s) (c : 𝕜) :
theorem eventually_singleton_add_smul_subset {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {x : E} {s : set E} (hs : metric.bounded 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_unit_ball_of_pos {E : Type u_2} [ E] {r : } (hr : 0 < r) :
r 1 = 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} [ E] (x z : E) {a b : } (ha : 0 a) (hb : 0 b) (hab : a + b = 1) :
∃ (y : E), = b * = a *
theorem exists_dist_le_le {E : Type u_2} [ E] {x z : E} {δ ε : } (hδ : 0 δ) (hε : 0 ε) (h : ε + δ) :
∃ (y : E), δ ε
theorem exists_dist_le_lt {E : Type u_2} [ E] {x z : E} {δ ε : } (hδ : 0 δ) (hε : 0 < ε) (h : < ε + δ) :
∃ (y : E), δ < ε
theorem exists_dist_lt_le {E : Type u_2} [ E] {x z : E} {δ ε : } (hδ : 0 < δ) (hε : 0 ε) (h : < ε + δ) :
∃ (y : E), < δ ε
theorem exists_dist_lt_lt {E : Type u_2} [ E] {x z : E} {δ ε : } (hδ : 0 < δ) (hε : 0 < ε) (h : < ε + δ) :
∃ (y : E), < δ < ε
theorem disjoint_ball_ball_iff {E : Type u_2} [ E] {x y : E} {δ ε : } (hδ : 0 < δ) (hε : 0 < ε) :
disjoint δ) ε) δ + ε
theorem disjoint_ball_closed_ball_iff {E : Type u_2} [ E] {x y : E} {δ ε : } (hδ : 0 < δ) (hε : 0 ε) :
disjoint δ) ε) δ + ε
theorem disjoint_closed_ball_ball_iff {E : Type u_2} [ E] {x y : E} {δ ε : } (hδ : 0 δ) (hε : 0 < ε) :
ε) δ + ε
theorem disjoint_closed_ball_closed_ball_iff {E : Type u_2} [ E] {x y : E} {δ ε : } (hδ : 0 δ) (hε : 0 ε) :
ε) δ + ε <
@[simp]
theorem inf_edist_thickening {E : Type u_2} [ E] {δ : } (hδ : 0 < δ) (s : set E) (x : E) :
=
@[simp]
theorem thickening_thickening {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 < δ) (s : set E) :
= metric.thickening + δ) s
@[simp]
theorem cthickening_thickening {E : Type u_2} [ E] {δ ε : } (hε : 0 ε) (hδ : 0 < δ) (s : set E) :
@[simp]
theorem closure_thickening {E : Type u_2} [ E] {δ : } (hδ : 0 < δ) (s : set E) :
@[simp]
theorem inf_edist_cthickening {E : Type u_2} [ E] (δ : ) (s : set E) (x : E) :
@[simp]
theorem thickening_cthickening {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 δ) (s : set E) :
= metric.thickening + δ) s
@[simp]
theorem cthickening_cthickening {E : Type u_2} [ E] {δ ε : } (hε : 0 ε) (hδ : 0 δ) (s : set E) :
@[simp]
theorem thickening_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 < δ) (x : E) :
δ) = + δ)
@[simp]
theorem thickening_closed_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 δ) (x : E) :
= + δ)
@[simp]
theorem cthickening_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 ε) (hδ : 0 < δ) (x : E) :
δ) = + δ)
@[simp]
theorem cthickening_closed_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 ε) (hδ : 0 δ) (x : E) :
= + δ)
theorem ball_add_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 < δ) (a b : E) :
ε + δ = metric.ball (a + b) + δ)
theorem ball_sub_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 < δ) (a b : E) :
ε - δ = metric.ball (a - b) + δ)
theorem ball_add_closed_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 δ) (a b : E) :
ε + = metric.ball (a + b) + δ)
theorem ball_sub_closed_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 < ε) (hδ : 0 δ) (a b : E) :
ε - = metric.ball (a - b) + δ)
theorem closed_ball_add_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 ε) (hδ : 0 < δ) (a b : E) :
+ δ = metric.ball (a + b) + δ)
theorem closed_ball_sub_ball {E : Type u_2} [ E] {δ ε : } (hε : 0 ε) (hδ : 0 < δ) (a b : E) :
- δ = metric.ball (a - b) + δ)
theorem closed_ball_add_closed_ball {E : Type u_2} [ E] {δ ε : } [proper_space E] (hε : 0 ε) (hδ : 0 δ) (a b : E) :
= metric.closed_ball (a + b) + δ)
theorem closed_ball_sub_closed_ball {E : Type u_2} [ E] {δ ε : } [proper_space E] (hε : 0 ε) (hδ : 0 δ) (a b : E) :
= metric.closed_ball (a - b) + δ)
theorem smul_closed_ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] (c : 𝕜) (x : E) {r : } (hr : 0 r) :
theorem smul_closed_unit_ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] (c : 𝕜) :
c =
theorem smul_closed_unit_ball_of_nonneg {E : Type u_2} [ E] {r : } (hr : 0 r) :
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} [ E] [nontrivial E] {x : E} {r : } :
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 𝕜] [ E] [ E] [nontrivial E] (c : 𝕜) (x : E) {r : } (hr : 0 r) :
c = metric.sphere (c x) (c * r)
theorem affinity_unit_ball {E : Type u_2} [ E] {r : } (hr : 0 < r) (x : E) :
x +ᵥ r 1 = 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} [ E] {r : } (hr : 0 r) (x : E) :
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.