mathlib3 documentation

analysis.inner_product_space.euclidean_dist

Euclidean distance on a finite dimensional space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 topological vector 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

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

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

Equations

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

Equations
theorem euclidean.exists_pos_lt_subset_ball {E : Type u_1} [add_comm_group E] [topological_space E] [topological_add_group E] [t2_space E] [module E] [has_continuous_smul 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 cont_diff.euclidean_dist {F : Type u_2} [normed_add_comm_group F] [normed_space F] {G : Type u_3} [normed_add_comm_group G] [normed_space G] [finite_dimensional G] {f g : F G} {n : ℕ∞} (hf : cont_diff n f) (hg : cont_diff n g) (h : (x : F), f x g x) :
cont_diff n (λ (x : F), euclidean.dist (f x) (g x))