theorem sum_neg_mul_eq_neg_sum_mul (n : ℕ) (a b : Fin n → ℝ) : ∑ i : Fin n, -a i * b i = -∑ i : Fin n, a i * b i

Theorem 1.1: summing (-a i) * b i gives the negative of the sum of a i * b i.

theorem sum_neg_sq_eq_sum_sq (n : ℕ) (a : Fin n → ℝ) : ∑ i : Fin n, (-a i) ^ 2 = ∑ i : Fin n, a i ^ 2

Theorem 1.1: negation does not change the sum of squares.

theorem cauchySchwarz_sum_mul_upper (n : ℕ) (a b : Fin n → ℝ) : ∑ i : Fin n, a i * b i ≤ √(∑ i : Fin n, a i ^ 2) * √(∑ i : Fin n, b i ^ 2)

Theorem 1.1: the upper bound for the Cauchy--Schwarz sum.

theorem cauchySchwarz_sum_mul_lower (n : ℕ) (a b : Fin n → ℝ) : -(√(∑ i : Fin n, a i ^ 2) * √(∑ i : Fin n, b i ^ 2)) ≤ ∑ i : Fin n, a i * b i

Theorem 1.1: the lower bound for the Cauchy--Schwarz sum.

theorem cauchySchwarz_abs_sum_mul (n : ℕ) (a b : Fin n → ℝ) : |∑ i : Fin n, a i * b i| ≤ √(∑ i : Fin n, a i ^ 2) * √(∑ i : Fin n, b i ^ 2)

Theorem 1.1: absolute-value form of the finite Cauchy--Schwarz inequality.

theorem cauchySchwarz_fin_sum_real (n : ℕ) (hn : 1 ≤ n) (a b : Fin n → ℝ) : |∑ i : Fin n, a i * b i| ≤ √(∑ i : Fin n, a i ^ 2) * √(∑ i : Fin n, b i ^ 2)

Theorem 1.1 (Cauchy--Schwarz inequality): let n ≥ 1 and a b : Fin n → ℝ. Then |∑ i, a i * b i| ≤ (∑ i, (a i)^2)^{1/2} * (∑ i, (b i)^2)^{1/2}.

theorem helperForTheorem_1_2_sum_add_sq (n : ℕ) (a b : Fin n → ℝ) : ∑ i : Fin n, (a i + b i) ^ 2 = ∑ i : Fin n, a i ^ 2 + ∑ i : Fin n, b i ^ 2 + 2 * ∑ i : Fin n, a i * b i

Helper for Theorem 1.2: expand the sum of squares of a i + b i.

theorem helperForTheorem_1_2_sum_add_sq_le_rhs_sq (n : ℕ) (a b : Fin n → ℝ) : ∑ i : Fin n, (a i + b i) ^ 2 ≤ (√(∑ i : Fin n, a i ^ 2) + √(∑ i : Fin n, b i ^ 2)) ^ 2

Helper for Theorem 1.2: squared form of the triangle inequality.

theorem triangle_inequality_euclidean_norm_fin (n : ℕ) (hn : 1 ≤ n) (a b : Fin n → ℝ) : √(∑ i : Fin n, (a i + b i) ^ 2) ≤ √(∑ i : Fin n, a i ^ 2) + √(∑ i : Fin n, b i ^ 2)

Theorem 1.2 (Triangle inequality in ℝ^n for the Euclidean norm): let n ≥ 1 and a b : Fin n → ℝ. Then (∑ i, (a i + b i)^2)^{1/2} ≤ (∑ i, (a i)^2)^{1/2} + (∑ i, (b i)^2)^{1/2}.

def RealSeqConvergesFrom (x : ℕ → ℝ) (m : ℕ) (x0 : ℝ) : Prop

Definition 1.1 (Convergence of a real sequence from index m).

@[reducible, inline]

abbrev realDist (x y : ℝ) : ℝ

Definition 1.2: the distance function on ℝ.

theorem realSeqConvergesFrom_iff_realDist_tendsto_zero (m : ℕ) (x : ℕ → ℝ) (x0 : ℝ) : RealSeqConvergesFrom x m x0 ↔ RealSeqConvergesFrom (fun (n : ℕ) => realDist (x n) x0) m 0

Lemma 1.1: a real sequence starting at m converges to x iff lim_{n→∞} d(x_n,x)=0, where d(a,b)=|a-b| is the usual metric on ℝ.

structure TaoMetricAxioms {X : Type u_1} (d : X → X → ℝ) : Prop

Definition 1.3 (Metric space): a metric satisfies the usual axioms.

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

theorem eq_zero_iff_of_self_of_eq_zero_imp {X : Type u_1} {d : X → X → ℝ} (hself : ∀ (x : X), d x x = 0) (himp : ∀ (x y : X), d x y = 0 → x = y) (x y : X) : d x y = 0 ↔ x = y

If d x x = 0 and d x y = 0 → x = y, then d x y = 0 ↔ x = y.

theorem self_of_eq_zero_iff {X : Type u_1} {d : X → X → ℝ} (hiff : ∀ (x y : X), d x y = 0 ↔ x = y) (x : X) : d x x = 0

From d x y = 0 ↔ x = y we get d x x = 0.

theorem eq_of_eq_zero_of_eq_zero_iff {X : Type u_1} {d : X → X → ℝ} (hiff : ∀ (x y : X), d x y = 0 ↔ x = y) (x y : X) : d x y = 0 → x = y

From d x y = 0 ↔ x = y we get d x y = 0 → x = y.

theorem proposition_1_1 {X : Type u_1} {d : X → X → ℝ} : ((∀ (x : X), d x x = 0) ∧ ∀ (x y : X), d x y = 0 → x = y) ↔ ∀ (x y : X), d x y = 0 ↔ x = y

Proposition 1.1: the standard zero-distance formulations are equivalent.

theorem metricAxioms_dist {X : Type u_1} [MetricSpace X] : TaoMetricAxioms fun (x y : X) => dist x y

The distance of a metric space satisfies TaoMetricAxioms.

theorem metricAxioms_realDist : TaoMetricAxioms fun (x y : ℝ) => realDist x y

The real distance satisfies TaoMetricAxioms.

theorem TaoMetricAxioms.self {X : Type u_1} {d : X → X → ℝ} (h : TaoMetricAxioms d) (x : X) : d x x = 0

A metric satisfies d x x = 0.

theorem realDist_eq_abs_sub (x y : ℝ) : realDist x y = |x - y|

The real distance equals the absolute value of the difference.

theorem abs_sub_eq_realDist (x y : ℝ) : |x - y| = realDist x y

The absolute value of a difference equals the real distance.

def standardMetric (x y : ℝ) : ℝ

Definition 1.4 (Standard metric on ℝ).

theorem standardMetric_eq_realDist (x y : ℝ) : standardMetric x y = realDist x y

The standard metric agrees with realDist on ℝ.

theorem metricAxioms_standardMetric : TaoMetricAxioms fun (x y : ℝ) => standardMetric x y

The standard metric on ℝ satisfies TaoMetricAxioms.

def inducedMetric {X : Type u_1} [MetricSpace X] (Y : Set X) : Subtype Y → Subtype Y → ℝ

Definition 1.5: for a metric space (X, d) and Y ⊆ X, the induced metric on Y is the restriction d|_{Y×Y} given by d|_{Y×Y}(y1, y2) = d(y1, y2); the subspace induced by Y is the metric space (Y, d|_{Y×Y}).

@[reducible, inline]

abbrev subspaceMetricSpace {X : Type u_1} [MetricSpace X] (Y : Set X) : MetricSpace (Subtype Y)

The metric space structure on a subset induced by the ambient metric.

@[reducible, inline]

noncomputable abbrev euclideanMetric (n : ℕ) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n) → ℝ

Definition 1.6: for n ≥ 1, the Euclidean (ℓ^2) metric on ℝ^n is d_{ℓ^2}(x,y) = √(∑ i, (x i - y i)^2); the metric space (ℝ^n, d_{ℓ^2}) is called Euclidean space of dimension n.

def taxicabMetric (n : ℕ) (x y : Fin n → ℝ) : ℝ

Definition 1.7: for n ≥ 1, the taxicab (ℓ^1) metric on ℝ^n is d_{ℓ^1}(x,y) = ∑ i, |x i - y i|, where x = (x_1, ..., x_n) and y = (y_1, ..., y_n).

noncomputable def l2Distance (n : ℕ) (x y : Fin n → ℝ) : ℝ

The ℓ^2 distance on ℝ^n given by sqrt (∑ i, |x i - y i|^2).

theorem sum_abs_sub_sq_le_sq_sum_abs_sub (n : ℕ) (x y : Fin n → ℝ) : ∑ i : Fin n, |x i - y i| ^ 2 ≤ (∑ i : Fin n, |x i - y i|) ^ 2

Proposition 1.2: the sum of squares of |x i - y i| is bounded by the square of the sum.

theorem l2Distance_le_taxicabMetric (n : ℕ) (x y : Fin n → ℝ) : l2Distance n x y ≤ taxicabMetric n x y

Proposition 1.2: the ℓ² distance is bounded above by the ℓ¹ distance.

theorem taxicabMetric_le_sqrt_n_mul_l2Distance (n : ℕ) (x y : Fin n → ℝ) : taxicabMetric n x y ≤ √↑n * l2Distance n x y

Proposition 1.2: the ℓ¹ distance is bounded by √n times the ℓ² distance.

theorem l2Distance_le_l1Distance_le_sqrt_n_l2Distance (n : ℕ) (hn : 1 ≤ n) (x y : Fin n → ℝ) : l2Distance n x y ≤ taxicabMetric n x y ∧ taxicabMetric n x y ≤ √↑n * l2Distance n x y

Proposition 1.2: Let n ≥ 1 and x,y ∈ ℝ^n. Define d_{ℓ^1}(x,y) = ∑ i, |x i - y i| and d_{ℓ^2}(x,y) = (∑ i, |x i - y i|^2)^{1/2}. Then d_{ℓ^2}(x,y) ≤ d_{ℓ^1}(x,y) ≤ √n * d_{ℓ^2}(x,y).

noncomputable def supNormMetric (n : ℕ) (x y : Fin n → ℝ) : ℝ

Definition 1.8: for n ≥ 1, the sup norm (ℓ^∞) metric on ℝ^n is d_{ℓ^∞}(x,y) = sup { |x i - y i| : 1 ≤ i ≤ n }, where x = (x_1, ..., x_n) and y = (y_1, ..., y_n).

theorem prop_1_3_range_abs_sub_nonempty (n : ℕ) (hn : 1 ≤ n) (x y : Fin n → ℝ) : (Set.range fun (i : Fin n) => |x i - y i|).Nonempty

Proposition 1.3: the range of coordinate differences is nonempty when n ≥ 1.

theorem prop_1_3_bddAbove_range_abs_sub (n : ℕ) (x y : Fin n → ℝ) : BddAbove (Set.range fun (i : Fin n) => |x i - y i|)

Proposition 1.3: the range of coordinate differences is bounded above.

theorem prop_1_3_abs_sub_le_supNormMetric (n : ℕ) (x y : Fin n → ℝ) (i : Fin n) : |x i - y i| ≤ supNormMetric n x y

Proposition 1.3: each coordinate difference is bounded by the sup norm metric.

theorem prop_1_3_supNormMetric_nonneg (n : ℕ) (hn : 1 ≤ n) (x y : Fin n → ℝ) : 0 ≤ supNormMetric n x y

Proposition 1.3: the sup norm metric is nonnegative.

theorem prop_1_3_abs_sub_le_l2Distance (n : ℕ) (x y : Fin n → ℝ) (i : Fin n) : |x i - y i| ≤ l2Distance n x y

Proposition 1.3: each coordinate difference is bounded by the ℓ² distance.

theorem prop_1_3_l2Distance_le_sqrt_n_mul_supNormMetric (n : ℕ) (hn : 1 ≤ n) (x y : Fin n → ℝ) : l2Distance n x y ≤ √↑n * supNormMetric n x y

Proposition 1.3: the ℓ² distance is bounded by √n times the sup norm metric.

theorem one_div_sqrt_n_l2Distance_le_supNormMetric_le_l2Distance (n : ℕ) (hn : 1 ≤ n) (x y : Fin n → ℝ) : 1 / √↑n * l2Distance n x y ≤ supNormMetric n x y ∧ supNormMetric n x y ≤ l2Distance n x y

Proposition 1.3: Let n ≥ 1. For all x,y ∈ ℝ^n, the metrics d_{ℓ^∞} and d_{ℓ^2} satisfy (1/√n) d_{ℓ^2}(x,y) ≤ d_{ℓ^∞}(x,y) ≤ d_{ℓ^2}(x,y). Equivalently, for all v ∈ ℝ^n, (1/√n) ‖v‖_2 ≤ ‖v‖_∞ ≤ ‖v‖_2.

def MetricSeqConvergesFrom {X : Type u_1} [MetricSpace X] (x : ℤ → X) (m : ℤ) (x0 : X) : Prop

Definition 1.9 (Convergence of sequences in metric spaces): a sequence (x^{(n)})_{n=m}^∞ in a metric space converges to x if for every ε > 0 there exists an integer N ≥ m such that dist (x n) x ≤ ε for all n ≥ N (equivalently, dist (x n) x → 0 as n → ∞).

theorem tail_converges_of_converges {X : Type u_1} [MetricSpace X] (x : ℤ → X) (m : ℤ) (x0 : X) : MetricSeqConvergesFrom x m x0 → ∀ m' ≥ m, MetricSeqConvergesFrom x m' x0

Proposition 1.4: if a sequence in a metric space converges to x0 from index m, then any tail starting at m' ≥ m also converges to x0.

def SeqConvergesFromWith {X : Type u_1} (d : X → X → ℝ) (x : ℕ → X) (m : ℕ) (x0 : X) : Prop

Convergence from index m with respect to a specified distance function.

theorem seqConvergesFromWith_of_le {X : Type u_1} {d1 d2 : X → X → ℝ} {x : ℕ → X} {m : ℕ} {x0 : X} (h : ∀ (u v : X), d1 u v ≤ d2 u v) : SeqConvergesFromWith d2 x m x0 → SeqConvergesFromWith d1 x m x0

Proposition 1.5: transfer convergence when one distance is pointwise bounded by another.

theorem seqConvergesFromWith_of_le_mul {X : Type u_1} {d1 d2 : X → X → ℝ} {x : ℕ → X} {m : ℕ} {x0 : X} {C : ℝ} (hC : 0 < C) (h : ∀ (u v : X), d1 u v ≤ C * d2 u v) : SeqConvergesFromWith d2 x m x0 → SeqConvergesFromWith d1 x m x0

Proposition 1.5: transfer convergence under a pointwise bound by a positive multiple.

theorem exists_uniform_index_forall_fin (n m : ℕ) {P : Fin n → ℕ → Prop} (h : ∀ (j : Fin n), ∃ Nj ≥ m, ∀ k ≥ Nj, P j k) : ∃ N ≥ m, ∀ k ≥ N, ∀ (j : Fin n), P j k

Proposition 1.5: a uniform index for finitely many coordinate bounds.

theorem equiv_l1_l2_linf_convergence_Rn (n m : ℕ) (x : ℕ → Fin n → ℝ) (x0 : Fin n → ℝ) : (SeqConvergesFromWith (l2Distance n) x m x0 ↔ SeqConvergesFromWith (taxicabMetric n) x m x0) ∧ (SeqConvergesFromWith (taxicabMetric n) x m x0 ↔ SeqConvergesFromWith (supNormMetric n) x m x0) ∧ (SeqConvergesFromWith (supNormMetric n) x m x0 ↔ ∀ (j : Fin n), RealSeqConvergesFrom (fun (k : ℕ) => x k j) m (x0 j))

Proposition 1.5 (Equivalence of ℓ^1, ℓ^2, ℓ^∞ convergence in ℝ^n): let n ∈ ℕ, let (x^{(k)})_{k=m}^∞ be a sequence in ℝ^n with x^{(k)} = (x_1^{(k)}, ..., x_n^{(k)}), and let x = (x_1, ..., x_n). Then the following are equivalent: (a) x^{(k)} → x with respect to d_{ℓ^2}, (b) x^{(k)} → x with respect to d_{ℓ^1}, (c) x^{(k)} → x with respect to d_{ℓ^∞}, and (d) for every 1 ≤ j ≤ n, the real sequence (x_j^{(k)})_{k=m}^∞ converges to x_j.

noncomputable def discreteMetric {X : Type u_1} (a b : X) : ℝ

The discrete metric on a type: d(a,b)=0 if a=b and d(a,b)=1 otherwise.

theorem discreteMetric_le_one_half_iff_eq {X : Type u_1} (a b : X) : discreteMetric a b ≤ 1 / 2 ↔ a = b

Proposition 1.6: in the discrete metric, the bound ≤ 1/2 forces equality.

theorem discreteMetric_eventually_eq_of_converges {X : Type u_1} (x : ℕ → X) (m : ℕ) (x0 : X) : SeqConvergesFromWith discreteMetric x m x0 → ∃ N ≥ m, ∀ n ≥ N, x n = x0

Proposition 1.6: convergence in the discrete metric implies eventual equality.

theorem discreteMetric_converges_of_eventually_eq {X : Type u_1} (x : ℕ → X) (m : ℕ) (x0 : X) : (∃ N ≥ m, ∀ n ≥ N, x n = x0) → SeqConvergesFromWith discreteMetric x m x0

Proposition 1.6: eventual equality implies convergence in the discrete metric.

theorem discreteMetric_converges_iff_eventually_eq {X : Type u_1} (x : ℕ → X) (m : ℕ) (x0 : X) : SeqConvergesFromWith discreteMetric x m x0 ↔ ∃ N ≥ m, ∀ n ≥ N, x n = x0

Proposition 1.6 (Convergence in the discrete metric): a sequence converges to x0 with respect to the discrete metric iff it is eventually constantly equal to x0.

theorem metric_limit_unique {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (x0 x1 : X) : SeqConvergesFromWith dist x m x0 → SeqConvergesFromWith dist x m x1 → x0 = x1

Proposition 1.7 (Uniqueness of limits): if a sequence converges to x0 and also to x1 with respect to a metric d, then x0 = x1.

theorem metricAxioms_comp_bijective {X : Type u_1} {d : X → X → ℝ} (hd : TaoMetricAxioms d) {f : X → X} (hf : Function.Bijective f) : TaoMetricAxioms fun (x y : X) => d (f x) (f y)

Proposition 1.8: Let (X, d) be a metric space and let f : X → X be a bijection. Define d'(x,y) = d (f x) (f y). Then d' is a metric on X.

theorem zero_mem_Icc_zero_one_and_one_mem_Icc_zero_one : 0 ∈ Set.Icc 0 1 ∧ 1 ∈ Set.Icc 0 1

Proposition 1.9 (prop:1.9): 0 and 1 lie in the closed unit interval.

noncomputable def swapEndpointsOnUnitInterval : { x : ℝ // x ∈ Set.Icc 0 1 } → { x : ℝ // x ∈ Set.Icc 0 1 }

Proposition 1.9 (prop:1.9): the map on the closed unit interval that sends 0 to 1, 1 to 0, and fixes every x ∈ (0,1).

noncomputable def swapEndpointsMetric (x y : { x : ℝ // x ∈ Set.Icc 0 1 }) : ℝ

Proposition 1.9 (prop:1.9): the metric d'(x,y)=|f(x)-f(y)| on the closed unit interval induced by swapEndpointsOnUnitInterval.

theorem one_div_mem_Icc_zero_one_of_nat_pos (n : ℕ) (hn : n ≠ 0) : 1 / ↑n ∈ Set.Icc 0 1

Proposition 1.9 (prop:1.9): 1/n lies in [0,1] for positive n.