Analysis I, Section 6.3: Suprema and infima of sequences

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Suprema and infima of sequences.

namespace Chapter6

Definition 6.3.1

noncomputable abbrev Sequence.sup (a:Sequence) : EReal := sSup { x | ∃ n ≥ a.m, x = a n }

Definition 6.3.1

noncomputable abbrev Sequence.inf (a:Sequence) : EReal := sInf { x | ∃ n ≥ a.m, x = a n }

Example 6.3.3

declaration uses `sorry`example : ((fun (n:ℕ) ↦ (-1:ℝ)^(n+1)):Sequence).sup = 1 := by⊢ (↑fun n => (-1) ^ (n + 1)).sup = 1 sorryAll goals completed! 🐙

Example 6.3.3

declaration uses `sorry`example : ((fun (n:ℕ) ↦ (-1:ℝ)^(n+1)):Sequence).inf = -1 := by⊢ (↑fun n => (-1) ^ (n + 1)).inf = -1 sorryAll goals completed! 🐙

Example 6.3.4 / Exercise 6.3.1

declaration uses `sorry`example : ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)):Sequence).sup = 1 := by⊢ (↑fun n => 1 / (↑n + 1)).sup = 1 sorryAll goals completed! 🐙

Example 6.3.4 / Exercise 6.3.1

declaration uses `sorry`example : ((fun (n:ℕ) ↦ 1/((n:ℝ)+1)):Sequence).inf = 0 := by⊢ (↑fun n => 1 / (↑n + 1)).inf = 0 sorryAll goals completed! 🐙

Example 6.3.5

declaration uses `sorry`example : ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).sup = ⊤ := by⊢ (↑fun n => ↑n + 1).sup = ⊤ sorryAll goals completed! 🐙

Example 6.3.5

declaration uses `sorry`example : ((fun (n:ℕ) ↦ (n+1:ℝ)):Sequence).inf = 1 := by⊢ (↑fun n => ↑n + 1).inf = 1 sorryAll goals completed! 🐙

abbrev Sequence.BddAboveBy (a:Sequence) (M:ℝ) : Prop := ∀ n ≥ a.m, a n ≤ Mabbrev Sequence.BddAbove (a:Sequence) : Prop := ∃ M, a.BddAboveBy Mabbrev Sequence.BddBelowBy (a:Sequence) (M:ℝ) : Prop := ∀ n ≥ a.m, a n ≥ Mabbrev Sequence.BddBelow (a:Sequence) : Prop := ∃ M, a.BddBelowBy M

theorem declaration uses `sorry`Sequence.bounded_iff (a:Sequence) : a.IsBounded ↔ a.BddAbove ∧ a.BddBelow := bya:Sequence⊢ a.IsBounded ↔ a.BddAbove ∧ a.BddBelow sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.sup_of_bounded {a:Sequence} (h: a.IsBounded) : a.sup.IsFinite := bya:Sequenceh:a.IsBounded⊢ a.sup.IsFinite sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.inf_of_bounded {a:Sequence} (h: a.IsBounded) : a.inf.IsFinite := bya:Sequenceh:a.IsBounded⊢ a.inf.IsFinite sorryAll goals completed! 🐙

Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2

theorem declaration uses `sorry`Sequence.le_sup {a:Sequence} {n:ℤ} (hn: n ≥ a.m) : a n ≤ a.sup := bya:Sequencen:ℤhn:n ≥ a.m⊢ ↑(a.seq n) ≤ a.sup sorryAll goals completed! 🐙

Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2

theorem declaration uses `sorry`Sequence.sup_le_upper {a:Sequence} {M:EReal} (h: ∀ n ≥ a.m, a n ≤ M) : a.sup ≤ M := bya:SequenceM:ERealh:∀ n ≥ a.m, ↑(a.seq n) ≤ M⊢ a.sup ≤ M sorryAll goals completed! 🐙

Proposition 6.3.6 (Least upper bound property) / Exercise 6.3.2

theorem declaration uses `sorry`Sequence.exists_between_lt_sup {a:Sequence} {y:EReal} (h: y < a.sup ) :
    ∃ n ≥ a.m, y < a n ∧ a n ≤ a.sup := bya:Sequencey:ERealh:y < a.sup⊢ ∃ n ≥ a.m, y < ↑(a.seq n) ∧ ↑(a.seq n) ≤ a.sup sorryAll goals completed! 🐙

Remark 6.3.7

theorem declaration uses `sorry`Sequence.ge_inf {a:Sequence} {n:ℤ} (hn: n ≥ a.m) : a n ≥ a.inf := bya:Sequencen:ℤhn:n ≥ a.m⊢ ↑(a.seq n) ≥ a.inf sorryAll goals completed! 🐙

Remark 6.3.7

theorem declaration uses `sorry`Sequence.inf_ge_lower {a:Sequence} {M:EReal} (h: ∀ n ≥ a.m, a n ≥ M) : a.inf ≥ M := bya:SequenceM:ERealh:∀ n ≥ a.m, ↑(a.seq n) ≥ M⊢ a.inf ≥ M sorryAll goals completed! 🐙

Remark 6.3.7

theorem declaration uses `sorry`Sequence.exists_between_gt_inf {a:Sequence} {y:EReal} (h: y > a.inf ) :
    ∃ n ≥ a.m, y > a n ∧ a n ≥ a.inf := bya:Sequencey:ERealh:y > a.inf⊢ ∃ n ≥ a.m, y > ↑(a.seq n) ∧ ↑(a.seq n) ≥ a.inf sorryAll goals completed! 🐙

abbrev Sequence.IsMonotone (a:Sequence) : Prop := ∀ n ≥ a.m, a (n+1) ≥ a nabbrev Sequence.IsAntitone (a:Sequence) : Prop := ∀ n ≥ a.m, a (n+1) ≤ a n

Proposition 6.3.8 / Exercise 6.3.3

theorem declaration uses `sorry`Sequence.convergent_of_monotone {a:Sequence} (hbound: a.BddAbove) (hmono: a.IsMonotone) :
    a.Convergent := bya:Sequencehbound:a.BddAbovehmono:a.IsMonotone⊢ a.Convergent sorryAll goals completed! 🐙

Proposition 6.3.8 / Exercise 6.3.3

theorem declaration uses `sorry`Sequence.lim_of_monotone {a:Sequence} (hbound: a.BddAbove) (hmono: a.IsMonotone) :
    lim a = a.sup := bya:Sequencehbound:a.BddAbovehmono:a.IsMonotone⊢ ↑(lim a) = a.sup sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.convergent_of_antitone {a:Sequence} (hbound: a.BddBelow) (hmono: a.IsAntitone) :
    a.Convergent := bya:Sequencehbound:a.BddBelowhmono:a.IsAntitone⊢ a.Convergent sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.lim_of_antitone {a:Sequence} (hbound: a.BddBelow) (hmono: a.IsAntitone) :
    lim a = a.inf := bya:Sequencehbound:a.BddBelowhmono:a.IsAntitone⊢ ↑(lim a) = a.inf sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.convergent_iff_bounded_of_monotone {a:Sequence} (ha: a.IsMonotone) :
    a.Convergent ↔ a.IsBounded := bya:Sequenceha:a.IsMonotone⊢ a.Convergent ↔ a.IsBounded sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.bounded_iff_convergent_of_antitone {a:Sequence} (ha: a.IsAntitone) :
    a.Convergent ↔ a.IsBounded := bya:Sequenceha:a.IsAntitone⊢ a.Convergent ↔ a.IsBounded sorryAll goals completed! 🐙

Example 6.3.9

noncomputable abbrev Example_6_3_9 (n:ℕ) := ⌊ Real.pi * 10^n ⌋ / (10:ℝ)^n

Example 6.3.9

declaration uses `sorry`example : (Example_6_3_9:Sequence).IsMonotone := by⊢ (↑Example_6_3_9).IsMonotone sorryAll goals completed! 🐙

Example 6.3.9

declaration uses `sorry`example : (Example_6_3_9:Sequence).BddAboveBy 4 := by⊢ (↑Example_6_3_9).BddAboveBy 4 sorryAll goals completed! 🐙

Example 6.3.9

declaration uses `sorry`example : (Example_6_3_9:Sequence).Convergent := by⊢ (↑Example_6_3_9).Convergent sorryAll goals completed! 🐙

Example 6.3.9

declaration uses `sorry`example : lim (Example_6_3_9:Sequence) ≤ 4 := by⊢ lim ↑Example_6_3_9 ≤ 4 sorryAll goals completed! 🐙

Proposition 6.3.1

theorem declaration uses `sorry`lim_of_exp {x:ℝ} (hpos: 0 < x) (hbound: x < 1) :
    ((fun (n:ℕ) ↦ x^n):Sequence).Convergent ∧ lim ((fun (n:ℕ) ↦ x^n):Sequence) = 0 := byx:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0
  -- This proof is written to follow the structure of the original text.
  set a := ((fun (n:ℕ) ↦ x^n):Sequence)x:ℝhpos:0 < xhbound:x < 1a:Sequence := ↑fun n => x ^ n⊢ a.Convergent ∧ lim a = 0
  have why : a.IsAntitone := sorryx:ℝhpos:0 < xhbound:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorry⊢ a.Convergent ∧ lim a = 0
  have hbound : a.BddBelowBy 0 := byx:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 intro n _x:ℝhpos:0 < xhbound:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryn:ℤa✝:n ≥ a.m⊢ a.seq n ≥ 0; positivityAll goals completed! 🐙
  have hbound' : a.BddBelow := byx:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 use 0All goals completed! 🐙
  have hconv := a.convergent_of_antitone hbound' whyx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' why⊢ a.Convergent ∧ lim a = 0
  set L := lim ax:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim a⊢ a.Convergent ∧ L = 0
  have : lim ((fun (n:ℕ) ↦ x^(n+1)):Sequence) = x * L := byx:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0
    rw [←(a.lim_smul x hconv).2]x:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim a⊢ (lim ↑fun n => x ^ (n + 1)) = lim (x • a); congre_ax:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim a⊢ (↑fun n => x ^ (n + 1)) = x • a; ext ne_a.mx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim a⊢ (↑fun n => x ^ (n + 1)).m = (x • a).me_a.seq.hx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim an:ℤ⊢ (↑fun n => x ^ (n + 1)).seq n = (x • a).seq n; rfle_a.seq.hx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim an:ℤ⊢ (↑fun n => x ^ (n + 1)).seq n = (x • a).seq n
    simp [a, pow_succ', HSMul.hSMul, SMul.smul]All goals completed! 🐙
  have why2 : lim ((fun (n:ℕ) ↦ x^(n+1)):Sequence) = lim ((fun (n:ℕ) ↦ x^n):Sequence) := byx:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 sorryAll goals completed! 🐙
  convert_to x * L = 1 * L at why2h.e'_3x:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim athis:(lim ↑fun n => x ^ (n + 1)) = x * L := 
  Eq.mpr (id (congrArg (fun _a => (lim ↑fun n => x ^ (n + 1)) = _a) (Eq.symm (Sequence.lim_smul x hconv).right)))
    ((fun a a_1 e_a => e_a ▸ Eq.refl (lim a)) (↑fun n => x ^ (n + 1)) (x • a)
      (Sequence.ext (Eq.refl (↑fun n => x ^ (n + 1)).m)
        (funext fun n =>
          of_eq_true
            (Eq.trans
              (congr (congrArg Eq (ite_congr ge_iff_le._simp_1 (fun a => pow_succ' x n.toNat) fun a => Eq.refl 0))
                (congrFun'
                  (congrArg Sequence.seq
                    (Sequence.mk.congr_simp a.m 0 (Eq.refl 0) (fun n => x * a.seq n)
                      (fun n => if 0 ≤ n then x * x ^ n.toNat else 0)
                      (funext fun n =>
                        Eq.trans
                          (Eq.trans
                            (congrArg (HMul.hMul x)
                              (ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (x ^ n.toNat)) fun a => Eq.refl 0))
                            (mul_ite (0 ≤ n) x (x ^ n.toNat) 0))
                          (ite_congr (Eq.refl (0 ≤ n)) (fun a => Eq.refl (x * x ^ n.toNat)) fun a => mul_zero x))
                      (Sequence.inst_smul._proof_1 x a)))
                  n))
              (eq_self (if 0 ≤ n then x * x ^ n.toNat else 0))))))why2:(lim ↑fun n => x ^ (n + 1)) = lim ↑fun n => x ^ n := sorry⊢ (lim ↑fun n => x ^ n) = 1 * Lx:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim athis:(lim ↑fun n => x ^ (n + 1)) = x * L := 
  Eq.mpr (id (congrArg (fun _a => (lim ↑fun n => x ^ (n + 1)) = _a) (Eq.symm (Sequence.lim_smul x hconv).right)))
    ((fun a a_1 e_a => e_a ▸ Eq.refl (lim a)) (↑fun n => x ^ (n + 1)) (x • a)
      (Sequence.ext (Eq.refl (↑fun n => x ^ (n + 1)).m)
        (funext fun n =>
          of_eq_true
            (Eq.trans
              (congr (congrArg Eq (ite_congr ge_iff_le._simp_1 (fun a => pow_succ' x n.toNat) fun a => Eq.refl 0))
                (congrFun'
                  (congrArg Sequence.seq
                    (Sequence.mk.congr_simp a.m 0 (Eq.refl 0) (fun n => x * a.seq n)
                      (fun n => if 0 ≤ n then x * x ^ n.toNat else 0)
                      (funext fun n =>
                        Eq.trans
                          (Eq.trans
                            (congrArg (HMul.hMul x)
                              (ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (x ^ n.toNat)) fun a => Eq.refl 0))
                            (mul_ite (0 ≤ n) x (x ^ n.toNat) 0))
                          (ite_congr (Eq.refl (0 ≤ n)) (fun a => Eq.refl (x * x ^ n.toNat)) fun a => mul_zero x))
                      (Sequence.inst_smul._proof_1 x a)))
                  n))
              (eq_self (if 0 ≤ n then x * x ^ n.toNat else 0))))))why2:x * L = 1 * L⊢ a.Convergent ∧ L = 0; simp [a,L]x:ℝhpos:0 < xhbound✝:x < 1a:Sequence := ↑fun n => x ^ nwhy:a.IsAntitone := sorryhbound:a.BddBelowBy 0 := 
  fun n a =>
    Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg (n ≥ 0) (pow_pos hpos n.toNat)
      (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))hbound':a.BddBelow := Exists.intro 0 hboundhconv:a.Convergent := Sequence.convergent_of_antitone hbound' whyL:ℝ := lim athis:(lim ↑fun n => x ^ (n + 1)) = x * L := 
  Eq.mpr (id (congrArg (fun _a => (lim ↑fun n => x ^ (n + 1)) = _a) (Eq.symm (Sequence.lim_smul x hconv).right)))
    ((fun a a_1 e_a => e_a ▸ Eq.refl (lim a)) (↑fun n => x ^ (n + 1)) (x • a)
      (Sequence.ext (Eq.refl (↑fun n => x ^ (n + 1)).m)
        (funext fun n =>
          of_eq_true
            (Eq.trans
              (congr (congrArg Eq (ite_congr ge_iff_le._simp_1 (fun a => pow_succ' x n.toNat) fun a => Eq.refl 0))
                (congrFun'
                  (congrArg Sequence.seq
                    (Sequence.mk.congr_simp a.m 0 (Eq.refl 0) (fun n => x * a.seq n)
                      (fun n => if 0 ≤ n then x * x ^ n.toNat else 0)
                      (funext fun n =>
                        Eq.trans
                          (Eq.trans
                            (congrArg (HMul.hMul x)
                              (ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (x ^ n.toNat)) fun a => Eq.refl 0))
                            (mul_ite (0 ≤ n) x (x ^ n.toNat) 0))
                          (ite_congr (Eq.refl (0 ≤ n)) (fun a => Eq.refl (x * x ^ n.toNat)) fun a => mul_zero x))
                      (Sequence.inst_smul._proof_1 x a)))
                  n))
              (eq_self (if 0 ≤ n then x * x ^ n.toNat else 0))))))why2:x * L = 1 * L⊢ a.Convergent ∧ L = 0
  have hx : x ≠ 1 := byx:ℝhpos:0 < xhbound:x < 1⊢ (↑fun n => x ^ n).Convergent ∧ (lim ↑fun n => x ^ n) = 0 grindAll goals completed! 🐙
  simp_all [-one_mul]All goals completed! 🐙

Exercise 6.3.4

theorem declaration uses `sorry`lim_of_exp' {x:ℝ} (hbound: x > 1) : ¬((fun (n:ℕ) ↦ x^n):Sequence).Convergent := byx:ℝhbound:x > 1⊢ ¬(↑fun n => x ^ n).Convergent sorryAll goals completed! 🐙

end Chapter6