Euclidean distance on a finite dimensional space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 topological vector 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.
noncomputable
def
to_euclidean
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E] :
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_5
noncomputable
def
euclidean.dist
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ 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.
Equations
- euclidean.dist x y = has_dist.dist (⇑to_euclidean x) (⇑to_euclidean y)
def
euclidean.closed_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
(x : E)
(r : ℝ) :
set E
Closed ball w.r.t. the euclidean distance.
Equations
- euclidean.closed_ball x r = {y : E | euclidean.dist y x ≤ r}
def
euclidean.ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ 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}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
(x : E)
(r : ℝ) :
euclidean.ball x r = ⇑to_euclidean ⁻¹' metric.ball (⇑to_euclidean x) r
theorem
euclidean.closed_ball_eq_preimage
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
(x : E)
(r : ℝ) :
theorem
euclidean.ball_subset_closed_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ} :
euclidean.ball x r ⊆ euclidean.closed_ball x r
theorem
euclidean.is_open_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ} :
is_open (euclidean.ball x r)
theorem
euclidean.mem_ball_self
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ}
(hr : 0 < r) :
x ∈ euclidean.ball x r
theorem
euclidean.closed_ball_eq_image
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
(x : E)
(r : ℝ) :
euclidean.closed_ball x r = ⇑(to_euclidean.symm) '' metric.closed_ball (⇑to_euclidean x) r
theorem
euclidean.is_compact_closed_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ} :
theorem
euclidean.is_closed_closed_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ} :
theorem
euclidean.closure_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
(x : E)
{r : ℝ}
(h : r ≠ 0) :
closure (euclidean.ball x r) = euclidean.closed_ball x r
theorem
euclidean.exists_pos_lt_subset_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{R : ℝ}
{s : set E}
{x : E}
(hR : 0 < R)
(hs : is_closed s)
(h : s ⊆ euclidean.ball x R) :
theorem
euclidean.nhds_basis_closed_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E} :
(nhds x).has_basis (λ (r : ℝ), 0 < r) (euclidean.closed_ball x)
theorem
euclidean.closed_ball_mem_nhds
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ}
(hr : 0 < r) :
euclidean.closed_ball x r ∈ nhds x
theorem
euclidean.nhds_basis_ball
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E} :
(nhds x).has_basis (λ (r : ℝ), 0 < r) (euclidean.ball x)
theorem
euclidean.ball_mem_nhds
{E : Type u_1}
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[t2_space E]
[module ℝ E]
[has_continuous_smul ℝ E]
[finite_dimensional ℝ E]
{x : E}
{r : ℝ}
(hr : 0 < r) :
euclidean.ball x r ∈ nhds x
theorem
cont_diff.euclidean_dist
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
{G : Type u_3}
[normed_add_comm_group G]
[normed_space ℝ G]
[finite_dimensional ℝ G]
{f g : F → G}
{n : ℕ∞}
(hf : cont_diff ℝ n f)
(hg : cont_diff ℝ n g)
(h : ∀ (x : F), f x ≠ g x) :
cont_diff ℝ n (λ (x : F), euclidean.dist (f x) (g x))