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] [TopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] : E ≃L[ℝ] EuclideanSpace ℝ (Fin (FiniteDimensional.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.

Equations

• toEuclidean = ContinuousLinearEquiv.ofFinrankEq (_ : FiniteDimensional.finrank ℝ E = FiniteDimensional.finrank ℝ (EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ E))))

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

Equations

• Euclidean.dist x y = dist (toEuclidean x) (toEuclidean y)

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

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

Equations

• Euclidean.closedBall x r = {y : E | Euclidean.dist y x ≤ r}

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

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

Equations

• Euclidean.ball x r = {y : E | Euclidean.dist y x < r}

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Euclidean.ball_mem_nhds {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [T2Space E] [Module ℝ E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : Euclidean.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 : F → G} {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)