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.

theorem Complex.ofReal_choose (a : ℝ) (n : ℕ) : ↑(Ring.choose a n) = Ring.choose (↑a) n

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

@[simp]

theorem binomialSeries_apply {𝕂 : Type u} [Field 𝕂] [CharZero 𝕂] (𝔸 : Type v) [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (a : 𝕂) {n : ℕ} (v : Fin n → 𝔸) : (binomialSeries 𝔸 a n) v = Ring.choose a n • (List.ofFn v).prod

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.

theorem binomialSeries_radius_ge_one {𝕂 : Type u_1} [RCLike 𝕂] {𝔸 : Type u_2} [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] {a : 𝕂} : 1 ≤ (binomialSeries 𝔸 a).radius

theorem Complex.one_add_cpow_hasFPowerSeriesOnBall_zero {a : ℂ} : HasFPowerSeriesOnBall (fun (x : ℂ) => (1 + x) ^ a) (binomialSeries ℂ a) 0 1

@[deprecated Complex.one_add_cpow_hasFPowerSeriesOnBall_zero (since := "2025-12-08")]

theorem one_add_cpow_hasFPowerSeriesOnBall_zero {a : ℂ} : HasFPowerSeriesOnBall (fun (x : ℂ) => (1 + x) ^ a) (binomialSeries ℂ a) 0 1

Alias of Complex.one_add_cpow_hasFPowerSeriesOnBall_zero.

theorem Complex.one_add_cpow_hasFPowerSeriesAt_zero {a : ℂ} : HasFPowerSeriesAt (fun (x : ℂ) => (1 + x) ^ a) (binomialSeries ℂ a) 0

@[deprecated Complex.one_add_cpow_hasFPowerSeriesAt_zero (since := "2025-12-08")]

theorem one_add_cpow_hasFPowerSeriesAt_zero {a : ℂ} : HasFPowerSeriesAt (fun (x : ℂ) => (1 + x) ^ a) (binomialSeries ℂ a) 0

Alias of Complex.one_add_cpow_hasFPowerSeriesAt_zero.

theorem Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero (a : ℂ) : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (1 - x) ^ a) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => Ring.choose (a + ↑n - 1) n) 0 1

theorem Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero (a : ℕ) : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (1 - x) ^ (a + 1)) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => ↑((a + n).choose a)) 0 1

theorem Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero (a : ℕ) {z : ℂ} (hz : z ≠ 0) : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (z - x) ^ (a + 1)) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ

theorem Complex.one_div_sub_hasFPowerSeriesOnBall_zero {z : ℂ} (hz : z ≠ 0) : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (z - x)) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (z ^ (n + 1))⁻¹) 0 ‖z‖ₑ

theorem Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero {z : ℂ} (hz : z ≠ 0) : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (z - x) ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => (z ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖z‖ₑ

theorem Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (1 - x)) (FormalMultilinearSeries.ofScalars ℂ 1) 0 1

theorem Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun (x : ℂ) => 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => ↑n + 1) 0 1

theorem Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero (a b : ℂ) : HasFPowerSeriesOnBall (fun (x : ℂ) => (b - a) / (1 - x) + a / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => a * ↑n + b) 0 1

∑ (ai + b) zⁱ = (b - a) / (1 - z) + a / (1 - z)²

theorem Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero (w x : ℂ) (hw : w ≠ x) : HasFPowerSeriesOnBall (fun (z : ℂ) => 1 / (z - w) ^ 2 - 1 / w ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) => (↑i + 1) * (w - x) ^ (-↑(i + 2)) - Nat.casesOn i (w ^ (-2)) 0) x ‖w - x‖ₑ

theorem Real.one_add_rpow_hasFPowerSeriesOnBall_zero {a : ℝ} : HasFPowerSeriesOnBall (fun (x : ℝ) => (1 + x) ^ a) (binomialSeries ℝ a) 0 1

@[deprecated Real.one_add_rpow_hasFPowerSeriesOnBall_zero (since := "2025-12-08")]

theorem one_add_rpow_hasFPowerSeriesOnBall_zero {a : ℝ} : HasFPowerSeriesOnBall (fun (x : ℝ) => (1 + x) ^ a) (binomialSeries ℝ a) 0 1

Alias of Real.one_add_rpow_hasFPowerSeriesOnBall_zero.

theorem Real.one_add_rpow_hasFPowerSeriesAt_zero {a : ℝ} : HasFPowerSeriesAt (fun (x : ℝ) => (1 + x) ^ a) (binomialSeries ℝ a) 0

@[deprecated Real.one_add_rpow_hasFPowerSeriesAt_zero (since := "2025-12-08")]

theorem one_add_rpow_hasFPowerSeriesAt_zero {a : ℝ} : HasFPowerSeriesAt (fun (x : ℝ) => (1 + x) ^ a) (binomialSeries ℝ a) 0

Alias of Real.one_add_rpow_hasFPowerSeriesAt_zero.

theorem Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero (a : ℝ) : HasFPowerSeriesOnBall (fun (x : ℝ) => 1 / (1 - x) ^ a) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => Ring.choose (a + ↑n - 1) n) 0 1

theorem Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero (a : ℕ) {r : ℝ} (hr : r ≠ 0) : HasFPowerSeriesOnBall (fun (x : ℝ) => 1 / (r - x) ^ (a + 1)) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖r‖ₑ

theorem Real.one_div_sub_hasFPowerSeriesOnBall_zero {r : ℝ} (hr : r ≠ 0) : HasFPowerSeriesOnBall (fun (x : ℝ) => 1 / (r - x)) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ

theorem Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero {r : ℝ} (hr : r ≠ 0) : HasFPowerSeriesOnBall (fun (x : ℝ) => 1 / (r - x) ^ 2) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => (r ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖r‖ₑ

theorem Real.one_div_one_sub_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun (x : ℝ) => 1 / (1 - x)) (FormalMultilinearSeries.ofScalars ℝ 1) 0 1

theorem Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun (x : ℝ) => 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => ↑n + 1) 0 1

theorem Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero (a b : ℝ) : HasFPowerSeriesOnBall (fun (x : ℝ) => (b - a) / (1 - x) + a / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) => a * ↑x + b) 0 1

∑ (ai + b) zⁱ = (b - a) / (1 - z) + a / (1 - z)²

@[deprecated Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero (since := "2025-12-28")]

theorem Real.hasFPowerSeriesOnBall_linear_zero (a b : ℝ) : HasFPowerSeriesOnBall (fun (x : ℝ) => (b - a) / (1 - x) + a / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) => a * ↑x + b) 0 1

Alias of Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero.

---

∑ (ai + b) zⁱ = (b - a) / (1 - z) + a / (1 - z)²