Step
*
1
of Lemma
common-limit-midpoints
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. ∀n:ℕ. (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n])))
4. ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|)
⊢ ∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)
BY
{ (Assert ∀n,d:ℕ.
(((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|)) BY
((D 0 THENA Auto)
THEN (InductionOnNat
THENL [((D 0 THENA Auto)
THEN Subst' n + 0 ~ n 0
THEN Auto
THEN nRNorm 0
THEN Subst' (-0) * 2^n ~ 0 0
THEN Auto
THEN (RWO "rabs-rminus<" 0 THENA Auto)
THEN (Assert -(-(a[n]) + b[n]) = (a[n] - b[n]) BY
Auto)
THEN RWO "-1" 0
THEN Auto)
; (((InstHyp [⌜n + (d - 1)⌝] 3⋅ THENA Auto)
THEN (Subst' (n + (d - 1)) + 1 ~ n + d -1 THENA Auto)
THEN RepeatFor 2 (D -1)
THEN RWO "-1 -2" 0
THEN Auto
THEN (((Assert (a[n] - (a[n + (d - 1)] + b[n + (d - 1)]/r(2)))
= ((a[n] - a[n + (d - 1)]) + (a[n] - b[n + (d - 1)])/r(2)) BY
(nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN MoveToConcl 9
THEN MoveToConcl 8
THEN GenConclTerms Auto [⌜a[n] - a[n + (d - 1)]⌝;⌜a[n] - b[n + (d - 1)]⌝;
⌜|a[0] - b[0]|⌝]⋅
THEN All Thin
THEN Auto)
ORELSE ((Assert (b[n] - (a[n + (d - 1)] + b[n + (d - 1)]/r(2)))
= ((b[n] - a[n + (d - 1)]) + (b[n] - b[n + (d - 1)])/r(2)) BY
(nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN MoveToConcl 11
THEN MoveToConcl 10
THEN GenConclTerms Auto [⌜b[n] - a[n + (d - 1)]⌝;⌜b[n] - b[n + (d - 1)]⌝;
⌜|a[0] - b[0]|⌝]⋅
THEN All Thin
THEN Auto)
))
THEN (Assert r0 < |r(2)| BY
(RWO "rabs-of-nonneg" 0 THEN Auto))
THEN (RWO "rabs-rdiv" 0 THENA Auto)
THEN (Assert |r(2)| = r(2) BY
(RWO "rabs-of-nonneg" 0 THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN (nRMul ⌜r(2)⌝ 0⋅ THENA Auto)
THEN (Assert |v + v1| ≤ (|v| + |v1|) BY
Auto)
THEN (nRMul ⌜r(2^n)⌝ (-1)⋅ THENA Auto)
THEN RWW "-1 5 6" 0
THEN Auto)]
)
)) }
1
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. ∀n:ℕ. (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n])))
4. ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|)
5. ∀n,d:ℕ.
(((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
⊢ ∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)
Latex:
Latex:
1. a : \mBbbN{} {}\mrightarrow{} \mBbbR{}
2. b : \mBbbN{} {}\mrightarrow{} \mBbbR{}
3. \mforall{}n:\mBbbN{}
(((a[n + 1] = a[n]) \mwedge{} (b[n + 1] = (a[n] + b[n]/r(2))))
\mvee{} ((a[n + 1] = (a[n] + b[n]/r(2))) \mwedge{} (b[n + 1] = b[n])))
4. \mforall{}n:\mBbbN{}. ((r(2\^{}n) * |a[n] - b[n]|) \mleq{} |a[0] - b[0]|)
\mvdash{} \mexists{}y:\mBbbR{}. (lim n\mrightarrow{}\minfty{}.a[n] = y \mwedge{} lim n\mrightarrow{}\minfty{}.b[n] = y)
By
Latex:
(Assert \mforall{}n,d:\mBbbN{}.
(((r(2\^{}n) * |a[n] - a[n + d]|) \mleq{} |a[0] - b[0]|)
\mwedge{} ((r(2\^{}n) * |a[n] - b[n + d]|) \mleq{} |a[0] - b[0]|)
\mwedge{} ((r(2\^{}n) * |b[n] - a[n + d]|) \mleq{} |a[0] - b[0]|)
\mwedge{} ((r(2\^{}n) * |b[n] - b[n + d]|) \mleq{} |a[0] - b[0]|)) BY
((D 0 THENA Auto)
THEN (InductionOnNat
THENL [((D 0 THENA Auto)
THEN Subst' n + 0 \msim{} n 0
THEN Auto
THEN nRNorm 0
THEN Subst' (-0) * 2\^{}n \msim{} 0 0
THEN Auto
THEN (RWO "rabs-rminus<" 0 THENA Auto)
THEN (Assert -(-(a[n]) + b[n]) = (a[n] - b[n]) BY
Auto)
THEN RWO "-1" 0
THEN Auto)
; (((InstHyp [\mkleeneopen{}n + (d - 1)\mkleeneclose{}] 3\mcdot{} THENA Auto)
THEN (Subst' (n + (d - 1)) + 1 \msim{} n + d -1 THENA Auto)
THEN RepeatFor 2 (D -1)
THEN RWO "-1 -2" 0
THEN Auto
THEN (((Assert (a[n] - (a[n + (d - 1)] + b[n + (d - 1)]/r(2)))
= ((a[n] - a[n + (d - 1)]) + (a[n] - b[n + (d - 1)])/r(2)) BY
(nRMul \mkleeneopen{}r(2)\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN MoveToConcl 9
THEN MoveToConcl 8
THEN GenConclTerms Auto [\mkleeneopen{}a[n] - a[n + (d - 1)]\mkleeneclose{};\mkleeneopen{}a[n] - b[n
+ (d - 1)]\mkleeneclose{};
\mkleeneopen{}|a[0] - b[0]|\mkleeneclose{}]\mcdot{}
THEN All Thin
THEN Auto)
ORELSE ((Assert (b[n] - (a[n + (d - 1)] + b[n + (d - 1)]/r(2)))
= ((b[n] - a[n + (d - 1)]) + (b[n] - b[n + (d - 1)])/r(2)) BY
(nRMul \mkleeneopen{}r(2)\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN MoveToConcl 11
THEN MoveToConcl 10
THEN GenConclTerms Auto [\mkleeneopen{}b[n] - a[n + (d - 1)]\mkleeneclose{};\mkleeneopen{}b[n] - b[n
+ (d - 1)]\mkleeneclose{};
\mkleeneopen{}|a[0] - b[0]|\mkleeneclose{}]\mcdot{}
THEN All Thin
THEN Auto)
))
THEN (Assert r0 < |r(2)| BY
(RWO "rabs-of-nonneg" 0 THEN Auto))
THEN (RWO "rabs-rdiv" 0 THENA Auto)
THEN (Assert |r(2)| = r(2) BY
(RWO "rabs-of-nonneg" 0 THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN (nRMul \mkleeneopen{}r(2)\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (Assert |v + v1| \mleq{} (|v| + |v1|) BY
Auto)
THEN (nRMul \mkleeneopen{}r(2\^{}n)\mkleeneclose{} (-1)\mcdot{} THENA Auto)
THEN RWW "-1 5 6" 0
THEN Auto)]
)
))
Home
Index