MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Mathematics in Lean documentation, Pinned Mathematics in Lean textbook

8 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. def C03S06.ConvergesTo line 6 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real

    Proof uses: GT.gt, OfNat.ofNat, Exists, GE.ge, LT.lt, abs, HSub.hSub

    8 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:6 (same declaration text).

  2. theorem C03S06.convergesTo_const line 9 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, C03S06.ConvergesTo, Nat

    Proof uses: GT.gt, OfNat.ofNat, Exists.intro, GE.ge, LT.lt, abs, HSub.hSub, Eq.mpr, id, Eq, congrArg, sub_self, abs_zero

    23 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:22 (same declaration text).

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  3. theorem C03S06.convergesTo_add The limit of a sum is the sum of the limits line 16 source

    L4DEL explanation

    Give each sequence half of the tolerance epsilon and wait until both are within their half.

    1. intro ε εpos, then have ε2pos : 0 < ε / 2 to get half the tolerance.
    2. rcases cs (ε / 2) ε2pos and rcases ct (ε / 2) ε2pos extract cutoffs Ns and Nt with their bounds hs and ht.
    3. use max Ns Nt picks a cutoff past both; for n at least that, le_of_max_le_left and le_of_max_le_right give n ≥ Ns and n ≥ Nt.
    4. A calc chain bounds |s n + t n - (a + b)| = |s n - a + (t n - b)| ≤ |s n - a| + |t n - b| < ε/2 + ε/2 = ε, using abs_add_le and add_lt_add.
    5. The matching exercise file leaves the part after use max Ns Nt as sorry; this is the solutions file version.

    Prerequisites: C03S06.ConvergesTo

    Sources and attribution: Pinned Lean source (dd6d752fedb1)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, C03S06.ConvergesTo, HAdd.hAdd

    Proof uses: GT.gt, OfNat.ofNat, id, Exists, GE.ge, LT.lt, abs, HSub.hSub, HDiv.hDiv, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 82 more

    109 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:29 (same statement text; different proof or body). Qualify references as C03S06.convergesTo_add@path.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

    theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n + t n) (a + b) := by
…

    Mentions: C03S06.ConvergesTo

  4. theorem C03S06.convergesTo_mul_const line 36 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, C03S06.ConvergesTo, HMul.hMul

    Proof uses: dite, Eq, OfNat.ofNat, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, id, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.mul_congr, HAdd.hAdd, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 24 more

    80 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:40 (same statement text; different proof or body). Qualify references as C03S06.convergesTo_mul_const@path.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

  5. theorem C03S06.exists_abs_le_of_convergesTo line 56 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, C03S06.ConvergesTo, Exists, LE.le, LT.lt, abs

    Proof uses: GE.ge, HSub.hSub, OfNat.ofNat, zero_lt_one, Exists.intro, HAdd.hAdd, Trans.trans, Eq, Lattice, AddGroup, Eq.rec, Eq.refl, abs_add_le, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast and 40 more

    71 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:51 (same statement text; different proof or body). Qualify references as C03S06.exists_abs_le_of_convergesTo@path.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  6. theorem C03S06.aux line 68 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, C03S06.ConvergesTo, OfNat.ofNat, HMul.hMul

    Proof uses: GT.gt, id, Exists, GE.ge, LT.lt, abs, HSub.hSub, LE.le, C03S06.exists_abs_le_of_convergesTo, lt_of_le_of_lt, abs_nonneg, le_refl, HDiv.hDiv, div_pos, Exists.intro, Max.max, le_of_max_le_left, le_of_max_le_right, Trans.trans, Eq and 9 more

    66 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:57 (same statement text; different proof or body). Qualify references as C03S06.aux@path.

    Tactic trace: 12 steps

    Open to load the checked before-and-after goal states.

  7. theorem C03S06.convergesTo_mul line 85 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, C03S06.ConvergesTo, HMul.hMul

    Proof uses: HAdd.hAdd, Neg.neg, OfNat.ofNat, C03S06.aux, Eq.mpr, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 38 more

    37 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:67 (same declaration text).

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

  8. theorem C03S06.convergesTo_unique line 97 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, C03S06.ConvergesTo, Eq

    Proof uses: Decidable.byContradiction, Not, GT.gt, abs, HSub.hSub, OfNat.ofNat, lt_of_le_of_ne, abs_nonneg, LE.le, eq_of_abs_sub_eq_zero, Eq.symm, HDiv.hDiv, id, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HMul.hMul, inferInstance and 91 more

    112 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S06_Sequences_and_Convergence.lean:79 (same statement text; different proof or body). Qualify references as C03S06.convergesTo_unique@path.

    Tactic trace: 28 steps

    Open to load the checked before-and-after goal states.