structure Chapter5.Sequence : Type

Definition 5.1.1 (Sequence). To avoid some technicalities involving dependent types, we extend sequences by zero to the left of the starting point n₀.

• n₀ : ℤ
• seq : ℤ → ℚ
• vanish (n : ℤ) : n < self.n₀ → self.seq n = 0

theorem Chapter5.Sequence.ext_iff {x y : Sequence} : x = y ↔ x.n₀ = y.n₀ ∧ x.seq = y.seq

theorem Chapter5.Sequence.ext {x y : Sequence} (n₀ : x.n₀ = y.n₀) (seq : x.seq = y.seq) : x = y

@[implicit_reducible]

instance Chapter5.Sequence.instCoeFun : CoeFun Sequence fun (x : Sequence) => ℤ → ℚ

Sequences can be thought of as functions from ℤ to ℚ.

Equations

• Chapter5.Sequence.instCoeFun = { coe := fun (a : Chapter5.Sequence) => a.seq }

def Chapter5.Sequence.ofNatFun (f : ℕ → ℚ) : Sequence

Functions from ℕ to ℚ can be thought of as sequences starting from 0; Sequence.ofNatFun performs this conversion.

The coe attribute allows the delaborator to print Sequence.ofNatFun f as ↑f, which is more concise; you may safely remove this if you prefer the more explicit notation.

Equations

• ↑f = { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then f n.toNat else 0, vanish := ⋯ }

@[implicit_reducible]

instance Chapter5.instCoeForallNatRatSequence : Coe (ℕ → ℚ) Sequence

If a : ℕ → ℚ is used in a context where a Sequence is expected, automatically coerce a to Sequence.ofNatFun a (which will be pretty-printed as ↑a).

Equations

• Chapter5.instCoeForallNatRatSequence = { coe := Chapter5.Sequence.ofNatFun }

@[reducible, inline]

abbrev Chapter5.Sequence.mk' (n₀ : ℤ) (a : { n : ℤ // n ≥ n₀ } → ℚ) : Sequence

Equations

• Chapter5.Sequence.mk' n₀ a = { n₀ := n₀, seq := fun (n : ℤ) => if h : n ≥ n₀ then a ⟨n, h⟩ else 0, vanish := ⋯ }

theorem Chapter5.Sequence.eval_mk {n n₀ : ℤ} (a : { n : ℤ // n ≥ n₀ } → ℚ) (h : n ≥ n₀) : (mk' n₀ a).seq n = a ⟨n, h⟩

@[simp]

theorem Chapter5.Sequence.eval_coe (n : ℕ) (a : ℕ → ℚ) : (↑a).seq ↑n = a n

@[simp]

theorem Chapter5.Sequence.eval_coe_at_int (n : ℤ) (a : ℕ → ℚ) : (↑a).seq n = if n ≥ 0 then a n.toNat else 0

@[simp]

theorem Chapter5.Sequence.n0_coe (a : ℕ → ℚ) : (↑a).n₀ = 0

@[reducible, inline]

abbrev Chapter5.Sequence.squares : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.squares = ↑fun (n : ℕ) => ↑n ^ 2

@[reducible, inline]

abbrev Chapter5.Sequence.three : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.three = ↑fun (x : ℕ) => 3

@[reducible, inline]

abbrev Chapter5.Sequence.squares_from_three : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.squares_from_three = Chapter5.Sequence.mk' 3 fun (x : { n : ℤ // n ≥ 3 }) => ↑↑x ^ 2

@[reducible, inline]

abbrev Rat.Steady (ε : ℚ) (a : Chapter5.Sequence) : Prop

A slight generalization of Definition 5.1.3 - definition of ε-steadiness for a sequence with an arbitrary starting point a.n₀

Equations

• ε.Steady a = ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m)

theorem Rat.steady_def (ε : ℚ) (a : Chapter5.Sequence) : ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m)

theorem Chapter5.Rat.Steady.coe (ε : ℚ) (a : ℕ → ℚ) : ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m)

Definition 5.1.3 - definition of ε-steadiness for a sequence starting at 0

@[reducible, inline]

abbrev Chapter5.Sequence.from (a : Sequence) (n₁ : ℤ) : Sequence

Sequence.from starts a : Sequence from n₁. It is intended for use when n₁ ≥ n₀, but returns the "junk" value of the original sequence a otherwise.

Equations

• a.from n₁ = Chapter5.Sequence.mk' (max a.n₀ n₁) fun (n : { n : ℤ // n ≥ max a.n₀ n₁ }) => a.seq ↑n

theorem Chapter5.Sequence.from_eval (a : Sequence) {n₁ n : ℤ} (hn : n ≥ n₁) : (a.from n₁).seq n = a.seq n

@[reducible, inline]

abbrev Rat.EventuallySteady (ε : ℚ) (a : Chapter5.Sequence) : Prop

Definition 5.1.6 (Eventually ε-steady)

Equations

• ε.EventuallySteady a = ∃ N ≥ a.n₀, ε.Steady (a.from N)

theorem Rat.eventuallySteady_def (ε : ℚ) (a : Chapter5.Sequence) : ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N)

theorem Chapter5.Sequence.ex_5_1_7_a : ¬Rat.Steady 0.1 ↑fun (n : ℕ) => (↑n + 1)⁻¹

Example 5.1.7: The sequence 1, 1/2, 1/3, ... is not 0.1-steady

theorem Chapter5.Sequence.ex_5_1_7_b : Rat.Steady 0.1 ((↑fun (n : ℕ) => (↑n + 1)⁻¹).from 10)

Example 5.1.7: The sequence a_10, a_11, a_12, ... is 0.1-steady

theorem Chapter5.Sequence.ex_5_1_7_c : Rat.EventuallySteady 0.1 ↑fun (n : ℕ) => (↑n + 1)⁻¹

Example 5.1.7: The sequence 1, 1/2, 1/3, ... is eventually 0.1-steady

theorem Chapter5.Sequence.ex_5_1_7_d {ε : ℚ} (hε : ε > 0) : ε.EventuallySteady ↑fun (n : ℕ) => if n = 0 then 10 else 0

Example 5.1.7

The sequence 10, 0, 0, ... is eventually ε-steady for every ε > 0. Left as an exercise.

@[reducible, inline]

abbrev Chapter5.Sequence.IsCauchy (a : Sequence) : Prop

Equations

• a.IsCauchy = ∀ ε > 0, ε.EventuallySteady a

theorem Chapter5.Sequence.isCauchy_def (a : Sequence) : a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a

theorem Chapter5.Sequence.IsCauchy.coe (a : ℕ → ℚ) : (↑a).IsCauchy ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε

Definition of Cauchy sequences, for a sequence starting at 0

theorem Chapter5.Sequence.IsCauchy.mk {n₀ : ℤ} (a : { n : ℤ // n ≥ n₀ } → ℚ) : (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε

noncomputable def Chapter5.Sequence.sqrt_two : Sequence

Equations

• Chapter5.Sequence.sqrt_two = ↑fun (n : ℕ) => ↑⌊√2 * 10 ^ n⌋ / 10 ^ n

theorem Chapter5.Sequence.ex_5_1_10_a : Rat.Steady 1 sqrt_two

Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem Chapter5.Sequence.ex_5_1_10_b : Rat.Steady 0.1 (sqrt_two.from 1)

Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem Chapter5.Sequence.ex_5_1_10_c : Rat.EventuallySteady 0.1 sqrt_two

theorem Chapter5.Sequence.IsCauchy.harmonic : (mk' 1 fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n).IsCauchy

Proposition 5.1.11. The harmonic sequence, defined as a₁ = 1, a₂ = 1/2, ... is a Cauchy sequence.

@[reducible, inline]

abbrev Chapter5.BoundedBy {n : ℕ} (a : Fin n → ℚ) (M : ℚ) : Prop

Equations

• Chapter5.BoundedBy a M = ∀ (i : Fin n), |a i| ≤ M

theorem Chapter5.boundedBy_def {n : ℕ} (a : Fin n → ℚ) (M : ℚ) : BoundedBy a M ↔ ∀ (i : Fin n), |a i| ≤ M

Definition 5.1.12 (bounded sequences). Here we start sequences from 0 rather than 1 to align better with Mathlib conventions.

@[reducible, inline]

abbrev Chapter5.Sequence.BoundedBy (a : Sequence) (M : ℚ) : Prop

Equations

• a.BoundedBy M = ∀ (n : ℤ), |a.seq n| ≤ M

theorem Chapter5.Sequence.boundedBy_def (a : Sequence) (M : ℚ) : a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M

Definition 5.1.12 (bounded sequences)

@[reducible, inline]

abbrev Chapter5.Sequence.IsBounded (a : Sequence) : Prop

Equations

• a.IsBounded = ∃ M ≥ 0, a.BoundedBy M

theorem Chapter5.Sequence.isBounded_def (a : Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M

Definition 5.1.12 (bounded sequences)

theorem Chapter5.IsBounded.finite {n : ℕ} (a : Fin n → ℚ) : ∃ M ≥ 0, BoundedBy a M

Lemma 5.1.14

theorem Chapter5.Sequence.isBounded_of_isCauchy {a : Sequence} (h : a.IsCauchy) : a.IsBounded

Lemma 5.1.15 (Cauchy sequences are bounded) / Exercise 5.1.1

theorem Chapter5.Sequence.isBounded_add {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hb : (↑b).IsBounded) : (↑(a + b)).IsBounded

Exercise 5.1.2

theorem Chapter5.Sequence.isBounded_sub {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hb : (↑b).IsBounded) : (↑(a - b)).IsBounded

theorem Chapter5.Sequence.isBounded_mul {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hb : (↑b).IsBounded) : (↑(a * b)).IsBounded