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.

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
Instances For

    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
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For
          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.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) :
          rSet.Ioo 0 R, s Euclidean.ball x r
          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} :
          (nhds x).HasBasis (fun (r : ) => 0 < r) (Euclidean.ball x)
          theorem ContDiff.euclidean_dist {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace G] [FiniteDimensional G] {f : FG} {g : FG} {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)