Helper for Lemma 4.3.1: finite summation-by-parts identity over Finset.range N.
Helper for Lemma 4.3.1: convergence of ordered partial sums of
a (n+1) * (b (n+1) - b n) to the summation-by-parts limit value.
Helper for Lemma 4.3.1: if the forward-difference series has a prescribed sum S,
the summation-by-parts identity holds with that same S.
Helper for Lemma 4.3.1: a HasSum hypothesis for the forward-difference series
immediately yields summability and the corresponding summation-by-parts identity.
Helper for Lemma 4.3.1: an explicit forward-difference HasSum hypothesis
already yields the textbook identity written with tsum.
Helper for Lemma 4.3.1: a corrected summation-by-parts statement with an explicit
forward HasSum hypothesis gives both forward summability and the textbook tsum identity.
Helper for Lemma 4.3.1: assuming unconditional summability of the forward-difference series, the target summation-by-parts identity follows from uniqueness of the partial-sum limit.
Helper for Lemma 4.3.1: if forward-difference summability is given explicitly, the full summation-by-parts conclusion follows.
Helper for Lemma 4.3.1: the alternating harmonic sequence tends to 0.
Helper for Lemma 4.3.1: for the explicit constant-one and alternating-harmonic data, the weighted forward-difference series is not summable.
Helper for Lemma 4.3.1: the explicit constant-one and alternating-harmonic
data with concrete limits A = 1, B = 0 satisfy the hypotheses while
the weighted forward-difference series is not summable.
Helper for Lemma 4.3.1: for the explicit constant-one and alternating-harmonic data,
the ordered partial sums of the weighted forward-difference series converge to -1.
Helper for Lemma 4.3.1: there exists an explicit sequence whose ordered
partial sums converge, while the sequence is not Summable in Lean's
finite-subset summability sense.
Helper for Lemma 4.3.1: explicit data satisfy the hypotheses while the forward-difference series fails to be unconditionally summable.
Helper for Lemma 4.3.1: the stated hypotheses do not force unconditional
summability of the forward-difference series in Lean's Summable sense.
Helper for Lemma 4.3.1: for the explicit constant-one and alternating-harmonic data at concrete limits, even the forward-summability implication alone is false.
Helper for Lemma 4.3.1: the full universal statement of the textbook conclusion would imply a universal forward-summability implication, which is false.
Helper for Lemma 4.3.1: there exists explicit data satisfying the hypotheses
for which the full textbook conclusion fails in Lean's unconditional Summable sense.
Helper for Lemma 4.3.1: the explicit constant-one and alternating-harmonic
data at concrete limits A = 1, B = 0 refute the full textbook conclusion.
Helper for Lemma 4.3.1: for the explicit constant-one and alternating-harmonic
data, convergence of ∑ (a_{n+1} - a_n)b_n does not imply unconditional
summability of ∑ a_{n+1}(b_{n+1} - b_n) in Lean.
Helper for Lemma 4.3.1: any universal proof of the textbook conclusion contradicts the explicit counterexample already established above.
Helper for Lemma 4.3.1: for the explicit constant-one and alternating-harmonic data at concrete limits, the implication from the stated hypotheses to the full textbook conclusion is false.
Lemma 4.3.1 (Summation by parts formula): Let a, b : ℕ → ℝ with Tendsto a atTop (𝓝 A) and Tendsto b atTop (𝓝 B). If the series ∑' n, (a (n + 1) - a n) * b n converges, then the ordered partial sums of ∑ a (n + 1) * (b (n + 1) - b n) converge to A * B - a 0 * b 0 - ∑' n, (a (n + 1) - a n) * b n.
Helper for Theorem 4.3.1: the right-endpoint affine normalization
x ↦ (x-a)/R tends to 1 from below when x → a+R inside (a-R,a+R).
Helper for Theorem 4.3.1: the left-endpoint affine normalization
x ↦ (a-x)/R tends to 1 from below when x → a-R inside (a-R,a+R).
Theorem 4.3.1 (Abel's theorem): let f(x) = ∑' n, c_n (x-a)^n be a real
power series centered at a with radius of convergence R and 0 < R.
(1) If ∑' n, c_n R^n converges, then x ↦ ∑' n, c_n (x-a)^n tends to
∑' n, c_n R^n as x → a + R within (a - R, a + R).
(2) If ∑' n, c_n (-R)^n converges, then x ↦ ∑' n, c_n (x-a)^n tends to
∑' n, c_n (-R)^n as x → a - R within (a - R, a + R).