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} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] : E ≃L[ℝ] EuclideanSpace ℝ (Fin (Module.finrank ℝ E))

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.

def Euclidean.dist {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ 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.

def Euclidean.closedBall {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] (x : E) (r : ℝ) : Set E

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

def Euclidean.ball {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] (x : E) (r : ℝ) : Set E

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

theorem Euclidean.ball_eq_preimage {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] (x : E) (r : ℝ) : ball x r = ⇑toEuclidean ⁻¹' Metric.ball (toEuclidean x) r

theorem Euclidean.closedBall_eq_preimage {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] (x : E) (r : ℝ) : closedBall x r = ⇑toEuclidean ⁻¹' Metric.closedBall (toEuclidean x) r

theorem Euclidean.ball_subset_closedBall {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} : ball x r ⊆ closedBall x r

@[simp]

theorem Euclidean.isOpen_ball {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} : IsOpen (ball x r)

theorem Euclidean.mem_ball_self {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : x ∈ ball x r

theorem Euclidean.closedBall_eq_image {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] (x : E) (r : ℝ) : closedBall x r = ⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r

theorem Euclidean.isCompact_closedBall {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} : IsCompact (closedBall x r)

theorem Euclidean.isClosed_closedBall {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} : IsClosed (closedBall x r)

theorem Euclidean.closure_ball {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] (x : E) {r : ℝ} (h : r ≠ 0) : closure (ball x r) = closedBall x r

theorem Euclidean.exists_pos_lt_subset_ball {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {R : ℝ} {s : Set E} {x : E} (hR : 0 < R) (hs : IsClosed s) (h : s ⊆ ball x R) : ∃ r ∈ Set.Ioo 0 R, s ⊆ ball x r

theorem Euclidean.nhds_basis_closedBall {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} : (nhds x).HasBasis (fun (r : ℝ) => 0 < r) (closedBall x)

theorem Euclidean.closedBall_mem_nhds {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : closedBall x r ∈ nhds x

theorem Euclidean.nhds_basis_ball {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} : (nhds x).HasBasis (fun (r : ℝ) => 0 < r) (ball x)

theorem Euclidean.ball_mem_nhds {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : ball x r ∈ nhds x

theorem ContDiff.euclidean_dist {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] {f g : F → G} {n : ℕ∞} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) (h : ∀ (x : F), f x ≠ g x) : ContDiff ℝ ↑n fun (x : F) => Euclidean.dist (f x) (g x)