structure FunctionSequences.PowerSeries : Type

A real power series about a center point x₀, given by a sequence of real coefficients a : ℕ → ℝ. Formally, it represents the formal series ∑ₘ aₘ (x - x₀)^m.

• a : ℕ → ℝ
• x₀ : ℝ

def FunctionSequences.PowerSeries.term (p : PowerSeries) (x : ℝ) (m : ℕ) : ℝ

The m-th term of the power series p evaluated at x, i.e. aₘ · (x - x₀)^m.

def FunctionSequences.PowerSeries.partialSum (p : PowerSeries) (x : ℝ) (n : ℕ) : ℝ

The n-th partial sum of the power series p evaluated at x, i.e. ∑_{m=0}^{n-1} aₘ (x - x₀)^m.

noncomputable def FunctionSequences.radiusOfConvergence (a : ℕ → ℝ) : ENNReal

The radius of convergence ρ of a real power series with coefficients a : ℕ → ℝ, defined via the Cauchy–Hadamard formula as the reciprocal of limsup_{n → ∞} ‖aₙ‖^(1/n), taking values in ℝ≥0∞.

theorem FunctionSequences.radiusOfConvergence_eq_formalRadius (a : ℕ → ℝ) : radiusOfConvergence a = (FormalMultilinearSeries.ofScalars ℝ a).radius

The Cauchy–Hadamard radius of convergence of a scalar power series with coefficients a agrees with the radius of the associated formal multilinear series FormalMultilinearSeries.ofScalars ℝ a from Mathlib.

theorem FunctionSequences.summable_abs_bounded (f : ℕ → ℝ) (hf : Summable f) : ∃ (C : ℝ), ∀ (n : ℕ), |f n| ≤ C

The absolute values of the terms of a summable real sequence are uniformly bounded: if f : ℕ → ℝ is summable, then there exists a constant C with |f n| ≤ C for all n.

theorem FunctionSequences.le_radiusOfConvergence_of_bound (a : ℕ → ℝ) (r : NNReal) (C : ℝ) (h : ∀ (n : ℕ), |a n| * ↑r ^ n ≤ C) : ↑r ≤ radiusOfConvergence a

Comparison criterion for the radius of convergence: if the sequence |aₙ| · rⁿ is uniformly bounded by some constant C, then r lies inside the disk of convergence, i.e. r ≤ radiusOfConvergence a.

theorem FunctionSequences.summable_abs_mul_pow_of_lt_radius (a : ℕ → ℝ) (r : NNReal) (hr : ↑r < radiusOfConvergence a) : Summable fun (n : ℕ) => |a n| * ↑r ^ n

Absolute convergence inside the radius of convergence: for any r < radiusOfConvergence a, the series ∑ₙ |aₙ| · rⁿ is summable.

theorem FunctionSequences.power_series_uniform_convergence (a : ℕ → ℝ) (x₀ r : ℝ) (hr : 0 < r) (hr_lt : ENNReal.ofReal r < radiusOfConvergence a) : TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => ∑ j ∈ Finset.range n, a j * (x - x₀) ^ j) (fun (x : ℝ) => ∑' (j : ℕ), a j * (x - x₀) ^ j) Filter.atTop (Set.Icc (x₀ - r) (x₀ + r))

Uniform convergence of a power series on closed sub-intervals of its disk of convergence: if ∑ aⱼ (x - x₀)^j has radius of convergence ρ ∈ (0, ∞], then for every r ∈ (0, ρ) the partial sums converge uniformly on [x₀ - r, x₀ + r] to the sum ∑' j, aⱼ (x - x₀)^j.