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

Proposition 1.9 (prop:1.9): the sequence (1/n)_{n≥1} viewed as a map ℕ → [0,1].

Equations

• oneOverNatSeqInUnitInterval n = if h : n = 0 then ⟨1, oneOverNatSeqInUnitInterval._proof_1⟩ else ⟨1 / ↑n, ⋯⟩

def unitIntervalOne : { x : ℝ // x ∈ Set.Icc 0 1 }

Proposition 1.9 (prop:1.9): the point 1 in the closed unit interval.

Equations

• unitIntervalOne = ⟨1, oneOverNatSeqInUnitInterval._proof_1⟩

def unitIntervalZero : { x : ℝ // x ∈ Set.Icc 0 1 }

Proposition 1.9 (prop:1.9): the point 0 in the closed unit interval.

Equations

• unitIntervalZero = ⟨0, unitIntervalZero._proof_1⟩

theorem swapEndpointsOnUnitInterval_apply_simp : swapEndpointsOnUnitInterval unitIntervalOne = unitIntervalZero ∧ swapEndpointsOnUnitInterval unitIntervalZero = unitIntervalOne ∧ ∀ (x : { x : ℝ // x ∈ Set.Icc 0 1 }), ↑x ≠ 0 → ↑x ≠ 1 → swapEndpointsOnUnitInterval x = x

Proposition 1.9 (prop:1.9): explicit values of swapEndpointsOnUnitInterval.

theorem oneOverNatSeqInUnitInterval_coe_succ_and_interior : (∀ (n : ℕ), ↑(oneOverNatSeqInUnitInterval n.succ) = 1 / ↑n.succ) ∧ ∀ n ≥ 2, ↑(oneOverNatSeqInUnitInterval n) ≠ 0 ∧ ↑(oneOverNatSeqInUnitInterval n) ≠ 1

Proposition 1.9 (prop:1.9): coercions and interior points of the sequence.

theorem swapEndpointsMetric_oneOverNatSeq_unitIntervalOne (n : ℕ) : n ≥ 2 → swapEndpointsMetric (oneOverNatSeqInUnitInterval n) unitIntervalOne = 1 / ↑n

Proposition 1.9 (prop:1.9): the swapped metric on the sequence near 1.

theorem oneOverNat_converges_to_one_swapEndpointsMetric : SeqConvergesFromWith swapEndpointsMetric oneOverNatSeqInUnitInterval 1 unitIntervalOne

Proposition 1.9: let X = [0,1] with the usual metric d(x,y)=|x-y|, let f swap 0 and 1 and fix all x ∈ (0,1), and define d'(x,y)=|f(x)-f(y)|. Then the sequence (1/n)_{n≥1} converges to 1 with respect to d'.

theorem helperForProposition_1_10_abs_dist_dist_le {X : Type u_1} [MetricSpace X] (a b c d : X) : |dist a b - dist c d| ≤ dist a c + dist b d

Helper for Proposition 1.10: bound the difference of distances by a sum.

theorem helperForProposition_1_10_max_index_eventually {P Q : ℕ → Prop} {N1 N2 : ℕ} (hP : ∀ n ≥ N1, P n) (hQ : ∀ n ≥ N2, Q n) (n : ℕ) : n ≥ max N1 N2 → P n ∧ Q n

Helper for Proposition 1.10: combine two eventual bounds past a max index.

theorem dist_seq_converges_of_converges {X : Type u_1} [MetricSpace X] (x y : ℕ → X) (x0 y0 : X) : SeqConvergesFromWith dist x 1 x0 → SeqConvergesFromWith dist y 1 y0 → RealSeqConvergesFrom (fun (n : ℕ) => dist (x n) (y n)) 1 (dist x0 y0)

Proposition 1.10: if x_n → x and y_n → y in a metric space, then d(x_n,y_n) converges to d(x,y).

theorem l2Distance_le_l1Distance_le_sqrt_n_l2Distance_prop (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.30 (Comparison of ℓ^1 and ℓ^2 metrics): let n ≥ 1 and x,y ∈ ℝ^n. Then d_{ℓ^2}(x,y) ≤ d_{ℓ^1}(x,y) ≤ √n * d_{ℓ^2}(x,y).

theorem one_div_sqrt_n_l2Distance_le_supNormMetric_le_l2Distance_prop (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.31 (Comparison of ℓ^2 and ℓ^∞ metrics): let n ≥ 1 and x,y ∈ ℝ^n. Then (1/√n) d_{ℓ^2}(x,y) ≤ d_{ℓ^∞}(x,y) ≤ d_{ℓ^2}(x,y).

theorem l1_l2_linf_convergence_equiv_Rn_metrics (n : ℕ) (hn : 1 ≤ n) (x : ℕ → Fin n → ℝ) (x0 : Fin n → ℝ) : SeqConvergesFromWith (taxicabMetric n) x 1 x0 ↔ SeqConvergesFromWith (l2Distance n) x 1 x0 ∧ SeqConvergesFromWith (supNormMetric n) x 1 x0

Proposition 1.32 (Equivalence of ℓ^1, ℓ^2, ℓ^∞ metrics): let n ≥ 1. A sequence in ℝ^n converges to x with respect to one of these metrics iff it converges to x with respect to each of the other two metrics.