# Documentation

Mathlib.Analysis.InnerProductSpace.EuclideanDist

# 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 toEuclidean 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 (toEuclidean x) (toEuclidean y) and provide some definitions (Euclidean.ball, Euclidean.closedBall) and simple lemmas about this distance. This way we hide the usage of toEuclidean behind an API.

def toEuclidean {E : Type u_1} [] [] [] [] [] [] :

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

Instances For
def Euclidean.dist {E : Type u_1} [] [] [] [] [] [] (x : E) (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.

Instances For
def Euclidean.closedBall {E : Type u_1} [] [] [] [] [] [] (x : E) (r : ) :
Set E

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

Instances For
def Euclidean.ball {E : Type u_1} [] [] [] [] [] [] (x : E) (r : ) :
Set E

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

Instances For
theorem Euclidean.ball_eq_preimage {E : Type u_1} [] [] [] [] [] [] (x : E) (r : ) :
= toEuclidean ⁻¹' Metric.ball (toEuclidean x) r
theorem Euclidean.closedBall_eq_preimage {E : Type u_1} [] [] [] [] [] [] (x : E) (r : ) :
= toEuclidean ⁻¹' Metric.closedBall (toEuclidean x) r
theorem Euclidean.ball_subset_closedBall {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } :
theorem Euclidean.isOpen_ball {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } :
theorem Euclidean.mem_ball_self {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } (hr : 0 < r) :
x
theorem Euclidean.closedBall_eq_image {E : Type u_1} [] [] [] [] [] [] (x : E) (r : ) :
= ↑(ContinuousLinearEquiv.symm toEuclidean) '' Metric.closedBall (toEuclidean x) r
theorem Euclidean.isCompact_closedBall {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } :
theorem Euclidean.isClosed_closedBall {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } :
theorem Euclidean.closure_ball {E : Type u_1} [] [] [] [] [] [] (x : E) {r : } (h : r 0) :
theorem Euclidean.exists_pos_lt_subset_ball {E : Type u_1} [] [] [] [] [] [] {R : } {s : Set E} {x : E} (hR : 0 < R) (hs : ) (h : s ) :
r, r Set.Ioo 0 R s
theorem Euclidean.nhds_basis_closedBall {E : Type u_1} [] [] [] [] [] [] {x : E} :
Filter.HasBasis (nhds x) (fun r => 0 < r) ()
theorem Euclidean.closedBall_mem_nhds {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } (hr : 0 < r) :
theorem Euclidean.nhds_basis_ball {E : Type u_1} [] [] [] [] [] [] {x : E} :
Filter.HasBasis (nhds x) (fun r => 0 < r) ()
theorem Euclidean.ball_mem_nhds {E : Type u_1} [] [] [] [] [] [] {x : E} {r : } (hr : 0 < r) :
theorem ContDiff.euclidean_dist {F : Type u_2} [] {G : Type u_3} [] [] {f : FG} {g : FG} {n : ℕ∞} (hf : ) (hg : ) (h : ∀ (x : F), f x g x) :
ContDiff n fun x => Euclidean.dist (f x) (g x)