generalized binomial theorem

Stream: mathlib4

[Zhuanhao Z Wu]

Hi there,

As result of a separate work, we proved the following form of the generalized binomial theorem on real numbers using formal power series (FormalMultilinearSeries):

$$(1+x)^\alpha = \sum_{k=0}^{\infty}\binom{\alpha}{k}x^k$$

The main theorems look as follows with conditions on its convergence radius. AFAIK, this is not in mathlib yet, so I'm looking into guidance on whether this is worth adding to mathlib, and we will be happy to contribute; or perhaps there is a trivial proof from existing theorems that we might be missing.

noncomputable def one_add_x_pow (α: ℝ) := FormalMultilinearSeries.ofScalars ℝ <| Ring.choose α

theorem one_add_x_has_pow_series:
  HasFPowerSeriesAt (𝕜 := ℝ) (λ(x:ℝ) => ((1:ℝ) + x)^α) (one_add_x_pow α) 0 := by sorry

theorem binomial_sum:
  ∀{α:ℝ} {x:ℝ}, ∃r>0, x∈(EMetric.ball 0 r) -> (1 + x)^α = ∑' (n: ℕ), Ring.choose α n * x^n := by sorry

[Vasilii Nesterov]

Hi! I actually just PRed this — please check #20011. I'd be happy if you could improve or add to it. My PR, at the very least, is missing your HasFPowerSeriesAt theorem.

[Zhuanhao Z Wu]

Sounds good! I will check the PR and see if there's more relevant results that I can add