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
- to_euclidean = continuous_linear_equiv.of_finrank_eq to_euclidean._proof_2
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
- euclidean.dist x y = dist (⇑to_euclidean x) (⇑to_euclidean y)
Closed ball w.r.t. the euclidean distance.
Equations
- euclidean.closed_ball x r = {y : E | euclidean.dist y x ≤ r}
Open ball w.r.t. the euclidean distance.
Equations
- euclidean.ball x r = {y : E | euclidean.dist y x < r}