structure MetricAxioms (X : Type u) (d : X → X → ℝ) : Prop

Definition 7.1.1: A metric on a set X is a function d : X × X → ℝ satisfying (i) d x y ≥ 0 (nonnegativity), (ii) d x y = 0 iff x = y (identity of indiscernibles), (iii) d x y = d y x (symmetry), and (iv) d x z ≤ d x y + d y z (triangle inequality). The pair (X, d) is a metric space.

• nonneg (x y : X) : 0 ≤ d x y
• eq_zero (x y : X) : d x y = 0 ↔ x = y
• symm (x y : X) : d x y = d y x
• triangle (x y z : X) : d x z ≤ d x y + d y z

theorem metricSpace_metricAxioms (X : Type u) [MetricSpace X] : MetricAxioms X fun (x y : X) => dist x y

A mathlib MetricSpace structure satisfies the book's metric axioms.

theorem metricAxioms_iff_metricSpace (X : Type u) (d : X → X → ℝ) : MetricAxioms X d ↔ ∃ (inst : MetricSpace X), dist = d

The metric axioms ensure there is a corresponding mathlib MetricSpace whose distance is the given function.

theorem real_standard_metric (x y : ℝ) : dist x y = |x - y|

Example 7.1.2: The standard metric on ℝ is given by d x y = |x - y|, and with this metric ℝ is a metric space.

noncomputable def realNonstandardDist (x y : ℝ) : ℝ

Example 7.1.3: On ℝ we can define a nonstandard metric d x y = |x - y| / (|x - y| + 1), which is symmetric, vanishes on the diagonal, satisfies the triangle inequality, and is bounded by 1, so every pair of points is at distance < 1.

Equations

• realNonstandardDist x y = |x - y| / (|x - y| + 1)

theorem realNonstandardDist_metric_axioms : (∀ (x y : ℝ), 0 ≤ realNonstandardDist x y) ∧ (∀ (x : ℝ), realNonstandardDist x x = 0) ∧ (∀ (x y : ℝ), realNonstandardDist x y = realNonstandardDist y x) ∧ (∀ (x y z : ℝ), realNonstandardDist x z ≤ realNonstandardDist x y + realNonstandardDist y z) ∧ ∀ (x y : ℝ), realNonstandardDist x y < 1

theorem cauchySchwarz_fin (n : ℕ) (x y : Fin n → ℝ) : (∑ k : Fin n, x k * y k) ^ 2 ≤ (∑ k : Fin n, x k ^ 2) * ∑ k : Fin n, y k ^ 2

Lemma 7.1.4 (Cauchy--Schwarz inequality): For vectors x = (x₁, x₂, …, xₙ) and y = (y₁, y₂, …, yₙ) in ℝⁿ, ((∑ₖ xₖ yₖ)²) ≤ (∑ₖ xₖ²)(∑ₖ yₖ²).

noncomputable def euclideanStandardDist (n : ℕ) (x y : EuclideanSpace ℝ (Fin n)) : ℝ

Example 7.1.5: The standard metric on ℝⁿ is d x y = √(∑ k, (x k - y k) ^ 2), and the triangle inequality follows from the Cauchy--Schwarz inequality.

Equations

• euclideanStandardDist n x y = √(∑ k : Fin n, (x.ofLp k - y.ofLp k) ^ 2)

theorem euclideanStandardDist_eq_dist (n : ℕ) (x y : EuclideanSpace ℝ (Fin n)) : euclideanStandardDist n x y = dist x y

theorem euclideanStandardDist_triangle (n : ℕ) (x y z : EuclideanSpace ℝ (Fin n)) : euclideanStandardDist n x z ≤ euclideanStandardDist n x y + euclideanStandardDist n y z

theorem complex_dist_eq_abs (z₁ z₂ : ℂ) : dist z₁ z₂ = ‖z₁ - z₂‖

Example 7.1.6: Viewing ℂ as ℝ², the metric is the Euclidean one, so dist z₁ z₂ = |z₁ - z₂|. The complex modulus is |x + iy| = √(x^2 + y^2), and its square is x^2 + y^2.

theorem complex_abs_sq (z : ℂ) : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2

noncomputable def discreteDist {X : Type u} [DecidableEq X] (x y : X) : ℝ

Example 7.1.7: On any set with decidable equality, the discrete distance d x y = 1 if x ≠ y and d x x = 0 defines a metric. In finite cases this places every distinct pair at distance 1; for infinite sets it still provides a genuine metric space structure.

Equations

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

theorem discreteDist_nonneg {X : Type u} [DecidableEq X] (x y : X) : 0 ≤ discreteDist x y

theorem discreteDist_eq_zero_iff {X : Type u} [DecidableEq X] (x y : X) : discreteDist x y = 0 ↔ x = y

theorem discreteDist_triangle {X : Type u} [DecidableEq X] (x y z : X) : discreteDist x z ≤ discreteDist x y + discreteDist y z

theorem discreteDist_metricAxioms (X : Type u) [DecidableEq X] : MetricAxioms X fun (x y : X) => discreteDist x y

theorem discreteDist_metric_space (X : Type u) [DecidableEq X] : ∃ (inst : MetricSpace X), dist = fun (x y : X) => discreteDist x y

theorem continuous_interval_dist_eq_uniform {a b : ℝ} (f g : C(↑(Set.Icc a b), ℝ)) : dist f g = ‖f - g‖

Example 7.1.8: On the space C([a,b], ℝ) of continuous real-valued functions on the interval [a,b], the metric is given by d f g = sup_{x ∈ [a,b]} |f x - g x|, which agrees with the uniform norm ‖f - g‖. Whenever we view C([a,b], ℝ) as a metric space, this is the understood distance.

@[reducible, inline]

abbrev spherePoints (r : ℝ) : Type

Example 7.1.9: On the unit sphere S² ⊂ ℝ³, the great circle distance between two points is the angle between the lines from the origin, so if x = (x₁,x₂,x₃) and y = (y₁,y₂,y₃), then d x y = arccos (x₁ y₁ + x₂ y₂ + x₃ y₃). This distance satisfies the usual metric axioms (the triangle inequality requires more work). On a sphere of radius r, the distance scales to r • θ.

Equations

• spherePoints r = { p : EuclideanSpace ℝ (Fin 3) // dist p 0 = r }

noncomputable def greatCircleDist (x y : spherePoints 1) : ℝ

Equations

• greatCircleDist x y = Real.arccos (inner ℝ ↑x ↑y)

theorem spherePoints_norm_eq_one (x : spherePoints 1) : ‖↑x‖ = 1

theorem greatCircleDist_eq_angle (x y : spherePoints 1) : greatCircleDist x y = InnerProductGeometry.angle ↑x ↑y

theorem greatCircleDist_triangle (x y z : spherePoints 1) : greatCircleDist x z ≤ greatCircleDist x y + greatCircleDist y z

theorem greatCircleDist_metric_axioms : (∀ (x y : spherePoints 1), 0 ≤ greatCircleDist x y) ∧ (∀ (x : spherePoints 1), greatCircleDist x x = 0) ∧ (∀ (x y : spherePoints 1), greatCircleDist x y = greatCircleDist y x) ∧ ∀ (x y z : spherePoints 1), greatCircleDist x z ≤ greatCircleDist x y + greatCircleDist y z

noncomputable def greatCircleDistOfRadius (r : ℝ) (x y : spherePoints r) : ℝ

Scaling the great circle distance to a sphere of radius r by multiplying the angular separation by r.

Equations

• greatCircleDistOfRadius r x y = r * Real.arccos (inner ℝ ↑x ↑y / r ^ 2)

def restricted_dist_metric {X : Type u} [MetricSpace X] (Y : Set X) : MetricSpace { x : X // x ∈ Y }

Proposition 7.1.10: For a metric space (X, d) and subset Y ⊆ X, the restriction of the distance function to Y × Y defines a metric on Y.

Equations

• restricted_dist_metric Y = inferInstance

def subspaceMetric {X : Type u} [MetricSpace X] (Y : Set X) : MetricSpace { x : X // x ∈ Y }

Definition 7.1.11: For a metric space (X, d) and subset Y ⊆ X, the restriction of d to Y × Y endows Y with the subspace metric.

Equations

• subspaceMetric Y = restricted_dist_metric Y

theorem subspaceMetric_eq_subtype {X : Type u} [MetricSpace X] (Y : Set X) : subspaceMetric Y = inferInstance

The subspace metric agrees with the standard metric structure that mathlib provides on the subtype Y.

def boundedSubset {X : Type u} [MetricSpace X] (S : Set X) : Prop

Definition 7.1.12: In a metric space (X, d), a subset S ⊆ X is bounded if there exists a point p and real number B with dist p x ≤ B for every x ∈ S. The space itself is bounded when its entire underlying set is bounded.

Equations

• boundedSubset S = ∃ (p : X) (B : ℝ), ∀ x ∈ S, dist p x ≤ B

def boundedSpace {X : Type u} [MetricSpace X] : Prop

Equations

• boundedSpace = boundedSubset Set.univ

theorem boundedSubset_iff_isBounded {X : Type u} [MetricSpace X] [Nonempty X] (S : Set X) : boundedSubset S ↔ Bornology.IsBounded S

The book's boundedness agrees with the standard bornological notion in a metric space.