theorem helperForTheorem_3_6_eventually_norm_sub_le_on_uIoc {a b : ℝ} (hab : a < b) {fseq : ℕ → ℝ → ℝ} {f : ℝ → ℝ} (h_unif : TendstoUniformlyOn fseq f Filter.atTop (Set.Icc a b)) (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ Set.uIoc a b, ‖fseq n x - f x‖ ≤ ε

Helper for Theorem 3.6: uniform convergence on Set.Icc gives a uniform bound on Set.uIoc.

theorem helperForTheorem_3_6_ae_tendsto_on_uIoc {a b : ℝ} (hab : a < b) {fseq : ℕ → ℝ → ℝ} {f : ℝ → ℝ} (h_unif : TendstoUniformlyOn fseq f Filter.atTop (Set.Icc a b)) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc a b), Filter.Tendsto (fun (n : ℕ) => fseq n x) Filter.atTop (nhds (f x))

Helper for Theorem 3.6: almost everywhere pointwise convergence on Set.uIoc.

theorem helperForTheorem_3_6_intervalIntegrable_limit {a b : ℝ} (hab : a < b) {fseq : ℕ → ℝ → ℝ} {f : ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (h_unif : TendstoUniformlyOn fseq f Filter.atTop (Set.Icc a b)) : IntervalIntegrable f MeasureTheory.volume a b

Helper for Theorem 3.6: the uniform limit is interval integrable.

theorem helperForTheorem_3_6_tendsto_intervalIntegral {a b : ℝ} (hab : a < b) {fseq : ℕ → ℝ → ℝ} {f : ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (h_unif : TendstoUniformlyOn fseq f Filter.atTop (Set.Icc a b)) (hf_int : IntervalIntegrable f MeasureTheory.volume a b) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in a..b, fseq n x) Filter.atTop (nhds (∫ (x : ℝ) in a..b, f x))

Helper for Theorem 3.6: convergence of interval integrals under uniform convergence.

theorem uniformLimit_intervalIntegral {a b : ℝ} (_hab : a < b) {fseq : ℕ → ℝ → ℝ} {f : ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (h_unif : TendstoUniformlyOn fseq f Filter.atTop (Set.Icc a b)) : IntervalIntegrable f MeasureTheory.volume a b ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in a..b, fseq n x) Filter.atTop (nhds (∫ (x : ℝ) in a..b, f x))

Theorem 3.6: Let a < b be real numbers. For each integer n ≥ 1, let f^{(n)} : [a,b] → ℝ be Riemann integrable, and assume that f^{(n)} → f uniformly on [a,b]. Then f is Riemann integrable and lim_{n→∞} ∫_{[a,b]} f^{(n)} = ∫_{[a,b]} f.

theorem uniformLimit_intervalIntegral_interchange {a b : ℝ} (_hab : a ≤ b) {fseq : ℕ → ℝ → ℝ} {f : ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (h_unif : TendstoUniformlyOn fseq f Filter.atTop (Set.Icc a b)) : IntervalIntegrable f MeasureTheory.volume a b ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in a..b, fseq n x) Filter.atTop (nhds (∫ (x : ℝ) in a..b, f x))

Theorem 3.7: [Interchange of limit and integral under uniform convergence] Let [a,b] be a compact interval in ℝ. If f^{(n)} are Riemann-integrable on [a,b] and converge uniformly to f on [a,b], then f is Riemann-integrable and lim_{n→∞} ∫_a^b f^{(n)} = ∫_a^b f.

theorem helperForTheorem_3_8_intervalIntegrable_partialSums {a b : ℝ} {fseq : ℕ → ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (n : ℕ) : IntervalIntegrable (fun (x : ℝ) => ∑ i ∈ Finset.range n, fseq i x) MeasureTheory.volume a b

Helper for Theorem 3.8: partial sums are interval integrable.

theorem helperForTheorem_3_8_intervalIntegral_partialSums {a b : ℝ} {fseq : ℕ → ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (n : ℕ) : ∫ (x : ℝ) in a..b, ∑ i ∈ Finset.range n, fseq i x = ∑ i ∈ Finset.range n, ∫ (x : ℝ) in a..b, fseq i x

Helper for Theorem 3.8: interval integral of a partial sum is the sum of integrals.

theorem helperForTheorem_3_8_tendsto_integral_partials {a b : ℝ} {fseq : ℕ → ℝ → ℝ} {s : ℝ → ℝ} {partials : ℕ → ℝ → ℝ} (hrewrite : ∀ (n : ℕ), ∫ (x : ℝ) in a..b, partials n x = ∑ i ∈ Finset.range n, ∫ (x : ℝ) in a..b, fseq i x) (htend : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in a..b, partials n x) Filter.atTop (nhds (∫ (x : ℝ) in a..b, s x))) : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, ∫ (x : ℝ) in a..b, fseq i x) Filter.atTop (nhds (∫ (x : ℝ) in a..b, s x))

Helper for Theorem 3.8: rewrite Tendsto after identifying two sequences.

theorem helperForTheorem_3_8_hasSumConditional_of_tendsto_range {g : ℕ → ℝ} {L : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (Finset.range n).sum g) Filter.atTop (nhds L)) : HasSum g L (SummationFilter.conditional ℕ)

Helper for Theorem 3.8: convert Tendsto of range partial sums to conditional HasSum.

theorem helperForTheorem_3_8_intervalIntegral_hasSumConditional {a b : ℝ} (hab : a < b) {fseq : ℕ → ℝ → ℝ} {s : ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (h_unif : TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => ∑ i ∈ Finset.range n, fseq i x) s Filter.atTop (Set.Icc a b)) : IntervalIntegrable s MeasureTheory.volume a b ∧ HasSum (fun (n : ℕ) => ∫ (x : ℝ) in a..b, fseq n x) (∫ (x : ℝ) in a..b, s x) (SummationFilter.conditional ℕ)

Helper for Theorem 3.8: conditional summation of integrals from uniform convergence.

theorem helperForTheorem_3_8_hasSum_of_summable_unconditional {f : ℕ → ℝ} {L : ℝ} (h_cond : HasSum f L (SummationFilter.conditional ℕ)) (h_summable : Summable f) : HasSum f L

Helper for Theorem 3.8: upgrade conditional HasSum to unconditional under unconditional summability.

theorem uniformSeries_intervalIntegral {a b : ℝ} (hab : a < b) {fseq : ℕ → ℝ → ℝ} {s : ℝ → ℝ} (h_integrable : ∀ (n : ℕ), IntervalIntegrable (fseq n) MeasureTheory.volume a b) (h_unif : TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => ∑ i ∈ Finset.range n, fseq i x) s Filter.atTop (Set.Icc a b)) : IntervalIntegrable s MeasureTheory.volume a b ∧ HasSum (fun (n : ℕ) => ∫ (x : ℝ) in a..b, fseq n x) (∫ (x : ℝ) in a..b, s x) (SummationFilter.conditional ℕ)

Theorem 3.8: Let a < b and let f^{(n)} be Riemann-integrable on [a,b]. Assume the series ∑ f^{(n)}(x) converges uniformly on [a,b] to s(x). Then s is Riemann-integrable on [a,b] and ∫_{[a,b]} s = ∑_{n=1}^∞ ∫_{[a,b]} f^{(n)}.

theorem helperForExample_3_6_3_hasSum_power_div {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) : HasSum (fun (n : ℕ) => r ^ n / ↑n) (-Real.log (1 - r))

Helper for Example 3.6.3 : the series ∑ r^n / n sums to -log(1-r) for 0 < r < 1.

theorem helperForExample_3_6_3_tsum_shift_pow_div {r : ℝ} (h : Summable fun (n : ℕ) => r ^ n / ↑n) : ∑' (n : ℕ), r ^ (n + 1) / (↑n + 1) = ∑' (n : ℕ), r ^ n / ↑n

Helper for Example 3.6.3 : shift the index in ∑ r^n / n.

theorem log_one_sub_eq_tsum_power_div {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) : -Real.log (1 - r) = ∑' (n : ℕ), r ^ (n + 1) / (↑n + 1)

Example 3.6.3 : For every real number r with 0 < r < 1, the identity -log(1-r) = ∑_{n=0}^∞ r^{n+1}/(n+1) holds.