MIL/C03_Logic/S06_Sequences_and_Convergence.lean

GitHub source file

12 declarations, 5 contain sorry, 0 declared as axioms

1. def C03S06.ConvergesTo Convergence of a real sequence line 6 source

   L4DEL explanation

   A sequence converges to a if, for every positive epsilon, all terms past some index N stay within epsilon of a.

   1. The definition is ConvergesTo (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε.
   2. The alternation of quantifiers matters: N may depend on ε, and n ranges over every index at least N.

   See also: C03S06.convergesTo_const

   Sources and attribution: Pinned Lean source (dd6d752fedb1)

   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/solutions/Solutions_S06_Sequences_and_Convergence.lean:6 (same declaration text).

   epsilon-N definition: the formulation of a limit that quantifies over a tolerance epsilon and a cutoff index N, as used by ConvergesTo.

   Tactic trace: 8 steps

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

   def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
   …

2. example C03S06.(example at line 9) line 9 source
3. example C03S06.(example at line 13) line 13 source
4. example C03S06.(example at line 17) line 17 source
5. theorem C03S06.convergesTo_const A constant sequence converges to its constant line 22 source

   L4DEL explanation

   Every term equals a, so the distance to a is 0, which is below any positive epsilon.

   1. intro ε εpos fixes a positive tolerance.
   2. use 0 chooses the cutoff N = 0, since all indices work.
   3. intro n nge fixes an arbitrary index.
   4. rw [sub_self, abs_zero] turns |a - a| into 0, and apply εpos closes 0 < ε.

   Prerequisites: C03S06.ConvergesTo

   Sources and attribution: Pinned Lean source (dd6d752fedb1)

   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/solutions/Solutions_S06_Sequences_and_Convergence.lean:9 (same declaration text).

   Tactic trace: 5 steps

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

   theorem convergesTo_const (a : ℝ) : ConvergesTo (fun _x : ℕ ↦ a) a := by
   …

   Mentions: C03S06.ConvergesTo

6. theorem C03S06.convergesTo_add sorry line 29 source

   depends on sorry 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 69 more

   82 instances, coercions and auxiliary constants left out.

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

   Tactic trace: 8 steps

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

7. theorem C03S06.convergesTo_mul_const sorry line 40 source

   depends on sorry 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 16 more

   46 instances, coercions and auxiliary constants left out.

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

   Tactic trace: 10 steps

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

8. theorem C03S06.exists_abs_le_of_convergesTo sorry line 51 source

   depends on sorry 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, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   23 instances, coercions and auxiliary constants left out.

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

   Tactic trace: 3 steps

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

9. theorem C03S06.aux sorry line 57 source

   depends on sorry 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, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   44 instances, coercions and auxiliary constants left out.

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

   Tactic trace: 7 steps

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

10. theorem C03S06.convergesTo_mul line 67 source

    depends on sorry 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/solutions/Solutions_S06_Sequences_and_Convergence.lean:85 (same declaration text).

    Tactic trace: 10 steps

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

11. theorem C03S06.convergesTo_unique sorry line 79 source

    depends on sorry what this means

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

    Proof uses: Decidable.byContradiction, Not, GT.gt, abs, HSub.hSub, OfNat.ofNat, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, HDiv.hDiv, id, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd and 72 more

    80 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 17 steps

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

12. def C03S06.ConvergesTo' line 99 source

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

    Statement uses: LinearOrder, Real

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

    13 instances, coercions and auxiliary constants left out.