Binomial Series

This file introduces the binomial series: $$ \sum_{k=0}^{\infty} \; \binom{a}{k} \; x^k = 1 + a x + \frac{a(a-1)}{2!} x^2 + \frac{a(a-1)(a-2)}{3!} x^3 + \cdots $$ where $a$ is an element of a normed field $\mathbb{K}$, and $x$ is an element of a normed algebra over $\mathbb{K}$.

Main Statements

• binomialSeries_radius_eq_one: The radius of convergence of the binomial series is 1 when a is not a natural number.
• binomialSeries_radius_eq_top_of_nat: In case a is natural, the series converges everywhere, since it is finite.

noncomputable def binomialSeries {𝕂 : Type u} [Field 𝕂] [CharZero 𝕂] (𝔸 : Type v) [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (a : 𝕂) : FormalMultilinearSeries 𝕂 𝔸 𝔸

Binomial series: the (scalar) formal multilinear series with coefficients given by Ring.choose a. The sum of this series is fun x ↦ (1 + x) ^ a within the radius of convergence.

Equations

• binomialSeries 𝔸 a = FormalMultilinearSeries.ofScalars 𝔸 fun (x : ℕ) => Ring.choose a x

theorem binomialSeries_eq_ordinaryHypergeometricSeries {𝕂 : Type u} [Field 𝕂] [CharZero 𝕂] {𝔸 : Type v} [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] {a b : 𝕂} (h : ∀ (k : ℕ), ↑k ≠ -b) : binomialSeries 𝔸 a = (ordinaryHypergeometricSeries 𝔸 (-a) b b).compContinuousLinearMap (-ContinuousLinearMap.id 𝕂 𝔸)

theorem binomialSeries_radius_eq_top_of_nat {𝕂 : Type v} [RCLike 𝕂] {𝔸 : Type u} [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] {a : ℕ} : (binomialSeries 𝔸 ↑a).radius = ⊤

The radius of convergence of binomialSeries 𝔸 a is ⊤ for natural a.

theorem binomialSeries_radius_eq_one {𝕂 : Type v} [RCLike 𝕂] {𝔸 : Type u} [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] {a : 𝕂} (ha : ∀ (k : ℕ), a ≠ ↑k) : (binomialSeries 𝔸 a).radius = 1

The radius of convergence of binomialSeries 𝔸 a is 1, when a is not natural.