mathlib documentation

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.

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
def euclidean.dist {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional 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] [normed_space E] [finite_dimensional 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] [normed_space E] [finite_dimensional E] (x : E) (r : ) :
set E

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

Equations
theorem euclidean.is_open_ball {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} {r : } :
theorem euclidean.mem_ball_self {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} {r : } (hr : 0 < r) :
theorem euclidean.closure_ball {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] (x : E) {r : } (h : 0 < r) :
theorem euclidean.exists_pos_lt_subset_ball {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {R : } {s : set E} {x : E} (hR : 0 < R) (hs : is_closed s) (h : s euclidean.ball x R) :
∃ (r : ) (H : r set.Ioo 0 R), s euclidean.ball x r
theorem euclidean.nhds_basis_closed_ball {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} :
(𝓝 x).has_basis (λ (r : ), 0 < r) (euclidean.closed_ball x)
theorem euclidean.closed_ball_mem_nhds {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} {r : } (hr : 0 < r) :
theorem euclidean.nhds_basis_ball {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} :
(𝓝 x).has_basis (λ (r : ), 0 < r) (euclidean.ball x)
theorem euclidean.ball_mem_nhds {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} {r : } (hr : 0 < r) :
theorem times_cont_diff.euclidean_dist {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {F : Type u_2} [normed_group F] [normed_space F] {f g : F → E} {n : with_top } (hf : times_cont_diff n f) (hg : times_cont_diff n g) (h : ∀ (x : F), f x g x) :
times_cont_diff n (λ (x : F), euclidean.dist (f x) (g x))