Binomial expansions of powers of Hahn Series

We introduce binomial expansions using embDomain.

Main Definitions

• HahnSeries.binomialFamily

Main results

• coefficients of powers of binomials

noncomputable def HahnSeries.SummableFamily.binomialFamily {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] [CommRing A] [Algebra R A] (x : HahnSeries Γ A) (r : R) : SummableFamily Γ A ℕ

A summable family of Hahn series, whose nth term is Ring.choose r n • (x - 1) ^ n when x is close to 1 (more precisely, when 0 < (x - 1).orderTop), and 0 ^ n otherwise. These terms give a formal expansion of x ^ r as (1 + (x - 1)) ^ r.

Equations

• HahnSeries.SummableFamily.binomialFamily x r = HahnSeries.SummableFamily.powerSeriesFamily (x - 1) (PowerSeries.binomialSeries A r)

@[simp]

theorem HahnSeries.SummableFamily.binomialFamily_apply {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] [CommRing A] [Algebra R A] {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop) (r : R) (n : ℕ) : (binomialFamily x r) n = Ring.choose r n • (x - 1) ^ n

@[simp]

theorem HahnSeries.SummableFamily.binomialFamily_apply_of_orderTop_nonpos {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] [CommRing A] [Algebra R A] {x : HahnSeries Γ A} (hx : ¬0 < (x - 1).orderTop) (r : R) (n : ℕ) : (binomialFamily x r) n = 0 ^ n

theorem HahnSeries.SummableFamily.binomialFamily_orderTop_pos {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] [CommRing A] [Algebra R A] {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop) (r : R) {n : ℕ} (hn : 0 < n) : 0 < ((binomialFamily x r) n).orderTop

theorem HahnSeries.SummableFamily.binomialFamily_mem_support {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] [CommRing A] [Algebra R A] {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop) (r : R) (n : ℕ) {g : Γ} (hg : g ∈ ((binomialFamily x r) n).support) : 0 ≤ g

theorem HahnSeries.SummableFamily.orderTop_hsum_binomialFamily_pos {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] [CommRing A] [Algebra R A] {x : HahnSeries Γ A} (hx : 0 < (x - 1).orderTop) (r : R) : 0 < ((binomialFamily x r).hsum - 1).orderTop

@[instance_reducible]

noncomputable instance HahnSeries.instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] : Pow (↥(orderTopSubOnePos Γ R)) R

Equations

• HahnSeries.instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos = { pow := fun (x : ↥(HahnSeries.orderTopSubOnePos Γ R)) (r : R) => HahnSeries.toOrderTopSubOnePos ⋯ }

@[simp]

theorem HahnSeries.binomial_power {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] {x : ↥(orderTopSubOnePos Γ R)} {r : R} : x ^ r = toOrderTopSubOnePos ⋯

theorem HahnSeries.pow_add {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] {x : ↥(orderTopSubOnePos Γ R)} {r s : R} : x ^ (r + s) = x ^ r * x ^ s

theorem HahnSeries.coeff_toOrderTopSubOnePos_pow {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [BinomialRing R] {g : Γ} (hg : 0 < g) (r s : R) (k : ℕ) : (↑↑(toOrderTopSubOnePos ⋯ ^ s)).coeff (k • g) = Ring.choose s k • r ^ k