def IsMetricFun {n : ℕ} (ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) : Prop

Text 15.0.14: A metric on ℝⁿ is a function ρ : ℝⁿ × ℝⁿ → ℝ such that: (1) ρ(x, y) > 0 if x ≠ y, and ρ(x, y) = 0 if x = y; (2) ρ(x, y) = ρ(y, x) for all x, y; (3) ρ(x, z) ≤ ρ(x, y) + ρ(y, z) for all x, y, z.

The quantity ρ(x, y) is interpreted as the distance between x and y.

In this development, we use Fin n → ℝ for ℝⁿ. The usual mathlib notion of a metric space is MetricSpace, and IsMetricFun ρ records the book axioms for the distance function ρ.

Equations

• IsMetricFun ρ = ((∀ (x y : Fin n → ℝ), x ≠ y → 0 < ρ x y) ∧ (∀ (x : Fin n → ℝ), ρ x x = 0) ∧ (∀ (x y : Fin n → ℝ), ρ x y = ρ y x) ∧ ∀ (x y z : Fin n → ℝ), ρ x z ≤ ρ x y + ρ y z)

theorem eq_of_IsMetricFun_eq_zero {n : ℕ} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMetricFun ρ) {x y : Fin n → ℝ} (hxy : ρ x y = 0) : x = y

A metric function vanishes only on the diagonal.

theorem exists_metricSpace_of_IsMetricFun {n : ℕ} (ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) (hρ : IsMetricFun ρ) : ∃ (ms : MetricSpace (Fin n → ℝ)), dist = ρ

Build a metric space structure from a metric function.

theorem isMetricFun_of_exists_metricSpace {n : ℕ} (ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) (hρ : ∃ (ms : MetricSpace (Fin n → ℝ)), dist = ρ) : IsMetricFun ρ

A metric space with distance ρ satisfies the metric-function axioms.

theorem isMetricFun_iff_exists_metricSpace {n : ℕ} (ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) : IsMetricFun ρ ↔ ∃ (ms : MetricSpace (Fin n → ℝ)), dist = ρ

noncomputable def discreteMetricFun {n : ℕ} : (Fin n → ℝ) → (Fin n → ℝ) → ℝ

Text 15.0.15: An extreme example of a metric on ℝⁿ is the function ρ(x, y) = 0 if x = y and ρ(x, y) = 1 if x ≠ y (the discrete metric).

This metric has no relation to the algebraic structure of ℝⁿ.

Equations

• discreteMetricFun x y = if x = y then 0 else 1

theorem discreteMetricFun_isMetricFun {n : ℕ} : IsMetricFun discreteMetricFun

def IsMinkowskiMetricFun {n : ℕ} (ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) : Prop

Text 15.0.16: A metric ρ on ℝⁿ is called a Minkowski metric if it satisfies the metric axioms and:

• Translation invariance: ρ (x + z) (y + z) = ρ x y for all x, y, z.
• Segment homogeneity: ρ x ((1 - λ) • x + λ • y) = λ * ρ x y for all x, y and λ ∈ [0, 1].

Equations

• IsMinkowskiMetricFun ρ = (IsMetricFun ρ ∧ (∀ (x y z : Fin n → ℝ), ρ (x + z) (y + z) = ρ x y) ∧ ∀ (x y : Fin n → ℝ), ∀ r ∈ Set.Icc 0 1, ρ x ((1 - r) • x + r • y) = r * ρ x y)

def IsNormFun {n : ℕ} (k : (Fin n → ℝ) → ℝ) : Prop

A real-valued function k : ℝⁿ → ℝ is a norm if it is nonnegative, vanishes only at 0, satisfies the triangle inequality, and is absolutely homogeneous: k (r • x) = |r| * k x.

Equations

• IsNormFun k = ((∀ (x : Fin n → ℝ), 0 ≤ k x) ∧ (∀ (x : Fin n → ℝ), k x = 0 ↔ x = 0) ∧ (∀ (x y : Fin n → ℝ), k (x + y) ≤ k x + k y) ∧ ∀ (x : Fin n → ℝ) (r : ℝ), k (r • x) = |r| * k x)

def normFunToMinkowskiMetricFun {n : ℕ} (k : (Fin n → ℝ) → ℝ) : (Fin n → ℝ) → (Fin n → ℝ) → ℝ

Given a norm function k, define the associated distance function ρ x y := k (x - y).

Equations

• normFunToMinkowskiMetricFun k x y = k (x - y)

def minkowskiMetricFunToNormFun {n : ℕ} (ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) : (Fin n → ℝ) → ℝ

Given a Minkowski metric ρ, define the associated norm function k x := ρ x 0.

Equations

• minkowskiMetricFunToNormFun ρ x = ρ x 0

theorem sub_segment_eq_smul_sub {n : ℕ} (x y : Fin n → ℝ) (r : ℝ) : x - ((1 - r) • x + r • y) = r • (x - y)

Displacement to a convex combination is a scalar multiple of the difference.

theorem isMinkowskiMetricFun_normFunToMinkowskiMetricFun {n : ℕ} {k : (Fin n → ℝ) → ℝ} (hk : IsNormFun k) : IsMinkowskiMetricFun (normFunToMinkowskiMetricFun k)

A norm induces a Minkowski metric via ρ x y = k (x - y).

theorem minkowskiMetricFunToNormFun_hom_Icc {n : ℕ} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMinkowskiMetricFun ρ) (x : Fin n → ℝ) (r : ℝ) : r ∈ Set.Icc 0 1 → minkowskiMetricFunToNormFun ρ (r • x) = r * minkowskiMetricFunToNormFun ρ x

For a Minkowski metric, the induced norm is homogeneous on [0,1].

theorem minkowskiMetricFunToNormFun_neg {n : ℕ} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMinkowskiMetricFun ρ) (x : Fin n → ℝ) : minkowskiMetricFunToNormFun ρ (-x) = minkowskiMetricFunToNormFun ρ x

The norm induced by a Minkowski metric is even.

theorem minkowskiMetricFunToNormFun_hom_nonneg {n : ℕ} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMinkowskiMetricFun ρ) (x : Fin n → ℝ) (r : ℝ) : 0 ≤ r → minkowskiMetricFunToNormFun ρ (r • x) = r * minkowskiMetricFunToNormFun ρ x

The norm induced by a Minkowski metric is homogeneous for nonnegative scalars.

theorem isNormFun_minkowskiMetricFunToNormFun {n : ℕ} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMinkowskiMetricFun ρ) : IsNormFun (minkowskiMetricFunToNormFun ρ)

A Minkowski metric induces a norm via k x = ρ x 0.

theorem minkowskiMetricFun_eq_normFunToMinkowskiMetricFun_minkowskiMetricFunToNormFun {n : ℕ} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (htrans : ∀ (x y z : Fin n → ℝ), ρ (x + z) (y + z) = ρ x y) (x y : Fin n → ℝ) : ρ x y = normFunToMinkowskiMetricFun (minkowskiMetricFunToNormFun ρ) x y

Translation invariance pins down a Minkowski metric by its values at the origin.

noncomputable def normFunEquivMinkowskiMetricFun {n : ℕ} : { k : (Fin n → ℝ) → ℝ // IsNormFun k } ≃ { ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ // IsMinkowskiMetricFun ρ }

Text 15.0.17: There is a one-to-one correspondence between Minkowski metrics and norms: if k is a norm then ρ x y := k (x - y) is a Minkowski metric, and conversely every Minkowski metric ρ arises uniquely in this way from the norm k x := ρ x 0.

Equations

• One or more equations did not get rendered due to their size.

theorem isNormFun_gaugeFunction_of_symmClosedBoundedConvex_zeroInterior {n : ℕ} {C : Set (Fin n → ℝ)} (hC_symm : ∀ (x : Fin n → ℝ), x ∈ C ↔ -x ∈ C) (hC_closed : IsClosed C) (hC_bdd : Bornology.IsBounded C) (hC_conv : Convex ℝ C) (hC0 : 0 ∈ interior C) : IsNormFun (gaugeFunction C)

The gauge of a symmetric closed bounded convex set with 0 in its interior is a norm.

theorem gaugeFunction_unitBall_eq {n : ℕ} {C : Set (Fin n → ℝ)} (hC_closed : IsClosed C) (hC_conv : Convex ℝ C) (hC0 : 0 ∈ interior C) : {x : Fin n → ℝ | gaugeFunction C x ≤ 1} = C

The gauge of a closed convex set with 0 in its interior has unit sublevel set C.

theorem ball_eq_image_add_smul_of_normFun_unitBall {n : ℕ} {k : (Fin n → ℝ) → ℝ} {C : Set (Fin n → ℝ)} (hk : IsNormFun k) (hC : {x : Fin n → ℝ | k x ≤ 1} = C) (x : Fin n → ℝ) (ε : ℝ) : 0 < ε → {y : Fin n → ℝ | normFunToMinkowskiMetricFun k x y ≤ ε} = (fun (c : Fin n → ℝ) => x + ε • c) '' C

Metric balls from a norm are translates of scaled unit balls.

theorem minkowskiMetricFunToNormFun_eq_gaugeFunction_of_ball_property {n : ℕ} {C : Set (Fin n → ℝ)} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMinkowskiMetricFun ρ) (hball : ∀ (ε : ℝ), 0 < ε → {y : Fin n → ℝ | ρ 0 y ≤ ε} = (fun (c : Fin n → ℝ) => ε • c) '' C) (x : Fin n → ℝ) : minkowskiMetricFunToNormFun ρ x = gaugeFunction C x

The induced norm of a Minkowski metric with prescribed balls is the gauge of C.

theorem existsUnique_minkowskiMetricFun_ball_eq_image_add_smul {n : ℕ} {C : Set (Fin n → ℝ)} (hC_symm : ∀ (x : Fin n → ℝ), x ∈ C ↔ -x ∈ C) (hC_closed : IsClosed C) (hC_bdd : Bornology.IsBounded C) (hC_conv : Convex ℝ C) (hC0 : 0 ∈ interior C) : ∃! ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ, IsMinkowskiMetricFun ρ ∧ ∀ (x : Fin n → ℝ) (ε : ℝ), 0 < ε → {y : Fin n → ℝ | ρ x y ≤ ε} = (fun (c : Fin n → ℝ) => x + ε • c) '' C

Text 15.0.18: If C is a symmetric closed bounded convex set such that 0 ∈ interior C, then there is a unique Minkowski metric ρ such that the ρ-ball of radius ε > 0 around x is x + ε C, i.e. {y | ρ x y ≤ ε} = {x + ε • c | c ∈ C}.

def IsOpenOfDistFun {α : Type u_1} (d : α → α → ℝ) (s : Set α) : Prop

A distance function d : α → α → ℝ defines a notion of "open set" by the usual metric-ball criterion: s is open if for every x ∈ s there exists ε > 0 such that d x y < ε implies y ∈ s.

Equations

• IsOpenOfDistFun d s = ∀ x ∈ s, ∃ (ε : ℝ), 0 < ε ∧ ∀ (y : α), d x y < ε → y ∈ s

def IsClosedOfDistFun {α : Type u_1} (d : α → α → ℝ) (s : Set α) : Prop

Equations

• IsClosedOfDistFun d s = IsOpenOfDistFun d sᶜ

def CauchySeqOfDistFun {α : Type u_1} (d : α → α → ℝ) (u : ℕ → α) : Prop

A sequence u : ℕ → α is Cauchy with respect to d if for every ε > 0 there exists N such that d (u m) (u n) < ε for all m,n ≥ N.

Equations

• CauchySeqOfDistFun d u = ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (m n : ℕ), N ≤ m → N ≤ n → d (u m) (u n) < ε

noncomputable def piEuclideanDist {n : ℕ} (x y : Fin n → ℝ) : ℝ

Euclidean distance on ℝⁿ (modeled as Fin n → ℝ), defined by d(x,y) = ‖x - y‖₂ = sqrt (dotProduct (x - y) (x - y)).

We use a pi-prefixed name to avoid clashing with mathlib's euclideanDist.

Equations

• piEuclideanDist x y = √((x - y) ⬝ᵥ (x - y))