# mathlibdocumentation

analysis.inner_product_space.euclidean_dist

# Euclidean distance on a finite dimensional space #

When we define a smooth bump function on a normed space, it is useful to have a smooth distance on the space. Since the default distance is not guaranteed to be smooth, we define to_euclidean to be an equivalence between a finite dimensional normed space and the standard Euclidean space of the same dimension. Then we define euclidean.dist x y = dist (to_euclidean x) (to_euclidean y) and provide some definitions (euclidean.ball, euclidean.closed_ball) and simple lemmas about this distance. This way we hide the usage of to_euclidean behind an API.

noncomputable def to_euclidean {E : Type u_1} [normed_group E] [ E]  :

If E is a finite dimensional space over ℝ, then to_euclidean is a continuous ℝ-linear equivalence between E and the Euclidean space of the same dimension.

Equations
noncomputable def euclidean.dist {E : Type u_1} [normed_group E] [ E] (x y : E) :

If x and y are two points in a finite dimensional space over ℝ, then euclidean.dist x y is the distance between these points in the metric defined by some inner product space structure on E.

Equations
def euclidean.closed_ball {E : Type u_1} [normed_group E] [ E] (x : E) (r : ) :
set E

Closed ball w.r.t. the euclidean distance.

Equations
def euclidean.ball {E : Type u_1} [normed_group E] [ E] (x : E) (r : ) :
set E

Open ball w.r.t. the euclidean distance.

Equations
• = {y : E | < r}
theorem euclidean.ball_eq_preimage {E : Type u_1} [normed_group E] [ E] (x : E) (r : ) :
theorem euclidean.closed_ball_eq_preimage {E : Type u_1} [normed_group E] [ E] (x : E) (r : ) :
theorem euclidean.ball_subset_closed_ball {E : Type u_1} [normed_group E] [ E] {x : E} {r : } :
theorem euclidean.is_open_ball {E : Type u_1} [normed_group E] [ E] {x : E} {r : } :
theorem euclidean.mem_ball_self {E : Type u_1} [normed_group E] [ E] {x : E} {r : } (hr : 0 < r) :
x
theorem euclidean.closed_ball_eq_image {E : Type u_1} [normed_group E] [ E] (x : E) (r : ) :
theorem euclidean.is_compact_closed_ball {E : Type u_1} [normed_group E] [ E] {x : E} {r : } :
theorem euclidean.is_closed_closed_ball {E : Type u_1} [normed_group E] [ E] {x : E} {r : } :
theorem euclidean.closure_ball {E : Type u_1} [normed_group E] [ E] (x : E) {r : } (h : r 0) :
theorem euclidean.exists_pos_lt_subset_ball {E : Type u_1} [normed_group E] [ E] {R : } {s : set E} {x : E} (hR : 0 < R) (hs : is_closed s) (h : s ) :
∃ (r : ) (H : r R), s
theorem euclidean.nhds_basis_closed_ball {E : Type u_1} [normed_group E] [ E] {x : E} :
(nhds x).has_basis (λ (r : ), 0 < r)
theorem euclidean.closed_ball_mem_nhds {E : Type u_1} [normed_group E] [ E] {x : E} {r : } (hr : 0 < r) :
theorem euclidean.nhds_basis_ball {E : Type u_1} [normed_group E] [ E] {x : E} :
(nhds x).has_basis (λ (r : ), 0 < r)
theorem euclidean.ball_mem_nhds {E : Type u_1} [normed_group E] [ E] {x : E} {r : } (hr : 0 < r) :
theorem cont_diff.euclidean_dist {E : Type u_1} [normed_group E] [ E] {F : Type u_2} [normed_group F] [ F] {f g : F → E} {n : with_top } (hf : f) (hg : g) (h : ∀ (x : F), f x g x) :
(λ (x : F), euclidean.dist (f x) (g x))