Limits of Formal Power Series

This file formalizes the notion of coefficientwise limits of formal power series, following Section 7.5 of Loehr's "Bijective Combinatorics".

Main Definitions

• Seq.StabilizesTo: A sequence (a_i)_{i ∈ ℕ} stabilizes to a if there exists N such that for all i ≥ N, we have a_i = a. (Definition 7.5.1)
• PowerSeries.CoeffStabilizesTo: A sequence of FPSs (f_i) coefficientwise stabilizes to f if for each n ∈ ℕ, the sequence of n-th coefficients stabilizes. (Definition 7.5.2)

Main Results

• PowerSeries.coeffStabilizesTo_of_forall_coeff_stabilizes: If each coefficient sequence stabilizes, then the FPS sequence coefficientwise stabilizes. (Theorem 7.5.3)
• PowerSeries.exists_xnEquiv_of_coeffStabilizesTo: If f_i → f, then for each n, eventually f_i ≡ f (mod x^{n+1}). (Lemma 7.5.4)
• PowerSeries.coeffStabilizesTo_add: Limits respect addition. (Proposition 7.5.5)
• PowerSeries.coeffStabilizesTo_mul: Limits respect multiplication. (Proposition 7.5.5)
• PowerSeries.coeffStabilizesTo_div: Limits respect division. (Proposition 7.5.6)
• PowerSeries.coeffStabilizesTo_comp: Limits respect composition. (Proposition 7.5.7)
• PowerSeries.coeffStabilizesTo_derivative: Limits respect derivatives. (Proposition 7.5.8)
• PowerSeries.coeffStabilizesTo_sum: Infinite sum is limit of partial sums. (Theorem 7.5.9)
• PowerSeries.coeffStabilizesTo_prod: Infinite product is limit of partial products. (Theorem 7.5.10)
• PowerSeries.fps_eq_limit_of_polynomials: Each FPS is a limit of polynomials. (Corollary 7.5.11)

Relationship with InfiniteProducts.lean

This file also defines IsMultipliable and tprod' for ℕ-indexed sequences of FPS. These are more restrictive than the general PowerSeries.Multipliable and PowerSeries.tprod in InfiniteProducts.lean:

• IsMultipliable f requires: (1) all constant terms equal 1, AND (2) eventually all terms are 1 + O(x^{n+1}) for each n.
• PowerSeries.Multipliable a only requires that each coefficient is finitely determined.

The IsMultipliable/tprod' definitions are used specifically for limits of partial products (where the index is ℕ and we consider products ∏_{i=0}^{N} f_i). For general infinite products over arbitrary index types, use the definitions in InfiniteProducts.lean.

References

• [Loehr, Bijective Combinatorics, Section 7.5]

def Seq.StabilizesTo {K : Type u_1} (a : ℕ → K) (lim : K) : Prop

A sequence (a_i)_{i ∈ ℕ} stabilizes to a if there exists N such that for all i ≥ N, we have a_i = a.

This is the notion of convergence in the discrete topology. (Definition 7.5.1, label: def.fps.lim.stab)

Equations

• Seq.StabilizesTo a lim = ∃ (N : ℕ), ∀ i ≥ N, a i = lim

theorem Seq.stabilizesTo_unique {K : Type u_1} {a : ℕ → K} {lim₁ lim₂ : K} (h₁ : StabilizesTo a lim₁) (h₂ : StabilizesTo a lim₂) : lim₁ = lim₂

If a sequence stabilizes to a limit, that limit is unique.

@[simp]

theorem Seq.stabilizesTo_const {K : Type u_1} (c : K) : StabilizesTo (fun (x : ℕ) => c) c

A constant sequence stabilizes to its value.

theorem Seq.stabilizesTo_of_eventually_eq {K : Type u_1} {a b : ℕ → K} {lim : K} (h : StabilizesTo a lim) (heq : ∃ (N : ℕ), ∀ i ≥ N, a i = b i) : StabilizesTo b lim

If a sequence is eventually equal to another, they stabilize to the same limit.

theorem Seq.stabilizesTo_add {K : Type u_1} [Add K] {a b : ℕ → K} {la lb : K} (ha : StabilizesTo a la) (hb : StabilizesTo b lb) : StabilizesTo (fun (i : ℕ) => a i + b i) (la + lb)

Addition preserves stabilization.

theorem Seq.stabilizesTo_mul {K : Type u_1} [Mul K] {a b : ℕ → K} {la lb : K} (ha : StabilizesTo a la) (hb : StabilizesTo b lb) : StabilizesTo (fun (i : ℕ) => a i * b i) (la * lb)

Multiplication preserves stabilization.

theorem Seq.stabilizesTo_neg {K : Type u_1} [Neg K] {a : ℕ → K} {la : K} (ha : StabilizesTo a la) : StabilizesTo (fun (i : ℕ) => -a i) (-la)

Negation preserves stabilization.

theorem Seq.stabilizesTo_pow_of_nilpotent {K : Type u_1} [MonoidWithZero K] {s : K} {k : ℕ} (hs : s ^ k = 0) : StabilizesTo (fun (i : ℕ) => s ^ i) 0

If s is nilpotent (i.e., s^k = 0 for some k), then (s^i) stabilizes to 0.

theorem Seq.stabilizesTo_pow_of_idempotent {K : Type u_1} [Monoid K] {s : K} (hs : s * s = s) : StabilizesTo (fun (i : ℕ) => s ^ (i + 1)) s

If s is idempotent (i.e., s^2 = s), then (s^i)_{i ≥ 1} stabilizes to s.

theorem Seq.stabilizesTo_finset_sum {K : Type u_1} {ι : Type u_2} [AddCommMonoid K] [DecidableEq ι] (s : Finset ι) {a : ι → ℕ → K} {la : ι → K} (h : ∀ i ∈ s, StabilizesTo (a i) (la i)) : StabilizesTo (fun (n : ℕ) => ∑ i ∈ s, a i n) (∑ i ∈ s, la i)

A finite sum of stabilizing sequences stabilizes.

def PowerSeries.CoeffStabilizesTo {K : Type u_1} [CommRing K] (f : ℕ → PowerSeries K) (lim : PowerSeries K) : Prop

A sequence of FPSs (f_i)_{i ∈ ℕ} coefficientwise stabilizes to f if for each n ∈ ℕ, the sequence ([x^n] f_i)_{i ∈ ℕ} stabilizes to [x^n] f.

This is the notion of convergence in the product topology where each factor K has the discrete topology. (Definition 7.5.2, label: def.fps.lim.coeff-stab)

Equations

• PowerSeries.CoeffStabilizesTo f lim = ∀ (n : ℕ), Seq.StabilizesTo (fun (i : ℕ) => (PowerSeries.coeff n) (f i)) ((PowerSeries.coeff n) lim)

theorem PowerSeries.coeffStabilizesTo_unique {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lim₁ lim₂ : PowerSeries K} (h₁ : CoeffStabilizesTo f lim₁) (h₂ : CoeffStabilizesTo f lim₂) : lim₁ = lim₂

If a sequence coefficientwise stabilizes to a limit, that limit is unique.

@[simp]

theorem PowerSeries.coeffStabilizesTo_const {K : Type u_1} [CommRing K] (g : PowerSeries K) : CoeffStabilizesTo (fun (x : ℕ) => g) g

A constant sequence coefficientwise stabilizes to its value.

theorem PowerSeries.coeffStabilizesTo_X_pow {K : Type u_1} [CommRing K] : CoeffStabilizesTo (fun (i : ℕ) => X ^ i) 0

The sequence (x^i)_{i ∈ ℕ} coefficientwise stabilizes to 0.

For each n, the sequence of n-th coefficients is (0, 0, ..., 0, 1, 0, 0, ...) which stabilizes to 0.

theorem PowerSeries.coeffStabilizesTo_of_forall_coeff_stabilizes {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {g : ℕ → K} (h : ∀ (n : ℕ), Seq.StabilizesTo (fun (i : ℕ) => (coeff n) (f i)) (g n)) : CoeffStabilizesTo f (mk g)

If each coefficient sequence stabilizes, the FPS sequence coefficientwise stabilizes. (Theorem 7.5.3, label: thm.fps.lim.lim-crit)

x^n-Equivalence Properties

The canonical definition of x^n-equivalence (XnEquiv) and its properties are in AlgebraicCombinatorics.FPS.XnEquivalence. The notation f ≡[x^n] g is defined there.

This section provides:

1. xnEquiv as an alias for XnEquiv (for use in this file's context)
2. xnEquiv_* lemmas as convenience aliases with underscore naming convention
3. Additional lemmas not in XnEquivalence.lean (e.g., xnEquiv_subst, xnEquiv_invOfUnit)

Note: xnEquiv_refl has @[refl] for use with the refl tactic.

@[reducible, inline]

abbrev PowerSeries.xnEquiv {K : Type u_1} [CommRing K] (n : ℕ) (f g : PowerSeries K) : Prop

Alias for XnEquiv in the current type context.

Equations

• PowerSeries.xnEquiv = PowerSeries.XnEquiv

theorem PowerSeries.xnEquiv_refl {K : Type u_1} [CommRing K] (n : ℕ) (f : PowerSeries K) : f ≡[x^n] f

x^n-equivalence is reflexive.

@[simp]

theorem PowerSeries.xnEquiv_self {K : Type u_1} [CommRing K] (n : ℕ) (f : PowerSeries K) : xnEquiv n f f

x^n-equivalence is reflexive (simp-friendly version).

This is a simp lemma for automatic simplification in proofs involving x^n-equivalence. The theorem xnEquiv_refl has the @[refl] attribute for use with the refl tactic.

theorem PowerSeries.xnEquiv_symm {K : Type u_1} [CommRing K] {n : ℕ} {f g : PowerSeries K} (h : f ≡[x^n] g) : g ≡[x^n] f

x^n-equivalence is symmetric.

theorem PowerSeries.xnEquiv_trans {K : Type u_1} [CommRing K] {n : ℕ} {f g h : PowerSeries K} (hfg : f ≡[x^n] g) (hgh : g ≡[x^n] h) : f ≡[x^n] h

x^n-equivalence is transitive.

theorem PowerSeries.xnEquiv_add {K : Type u_1} [CommRing K] {n : ℕ} {f₁ f₂ g₁ g₂ : PowerSeries K} (hf : f₁ ≡[x^n] f₂) (hg : g₁ ≡[x^n] g₂) : f₁ + g₁ ≡[x^n] f₂ + g₂

x^n-equivalence is compatible with addition.

theorem PowerSeries.xnEquiv_sub {K : Type u_1} [CommRing K] {n : ℕ} {f₁ f₂ g₁ g₂ : PowerSeries K} (hf : f₁ ≡[x^n] f₂) (hg : g₁ ≡[x^n] g₂) : f₁ - g₁ ≡[x^n] f₂ - g₂

x^n-equivalence is compatible with subtraction. (Theorem 7.3.11(b), label: thm.fps.xneq.props)

theorem PowerSeries.xnEquiv_smul {K : Type u_1} [CommRing K] {n : ℕ} {f g : PowerSeries K} (c : K) (h : f ≡[x^n] g) : c • f ≡[x^n] c • g

x^n-equivalence is compatible with scalar multiplication. (Theorem 7.3.11(c), label: thm.fps.xneq.props)

theorem PowerSeries.xnEquiv_mul {K : Type u_1} [CommRing K] {n : ℕ} {f₁ f₂ g₁ g₂ : PowerSeries K} (hf : f₁ ≡[x^n] f₂) (hg : g₁ ≡[x^n] g₂) : f₁ * g₁ ≡[x^n] f₂ * g₂

x^n-equivalence is compatible with multiplication.

theorem PowerSeries.xnEquiv_pow {K : Type u_1} [CommRing K] {n : ℕ} {f g : PowerSeries K} (h : f ≡[x^n] g) (d : ℕ) : f ^ d ≡[x^n] g ^ d

x^n-equivalence is compatible with powers.

theorem PowerSeries.xnEquiv_finset_sum {K : Type u_1} [CommRing K] {ι : Type u_2} [DecidableEq ι] {n : ℕ} (s : Finset ι) {f g : ι → PowerSeries K} (h : ∀ i ∈ s, f i ≡[x^n] g i) : ∑ i ∈ s, f i ≡[x^n] ∑ i ∈ s, g i

x^n-equivalence is compatible with finite sums. (Theorem 7.3.11(f), label: thm.fps.xneq.props)

theorem PowerSeries.xnEquiv_finset_prod {K : Type u_1} [CommRing K] {ι : Type u_2} [DecidableEq ι] {n : ℕ} (s : Finset ι) {f g : ι → PowerSeries K} (h : ∀ i ∈ s, f i ≡[x^n] g i) : ∏ i ∈ s, f i ≡[x^n] ∏ i ∈ s, g i

x^n-equivalence is compatible with finite products.

If two families of FPSs (c_w)_{w ∈ V} and (d_w)_{w ∈ V} satisfy c_w ≡[x^n] d_w for each w ∈ V, then ∏_{w ∈ V} c_w ≡[x^n] ∏_{w ∈ V} d_w.

This is a key lemma used in proving that the family of fiber subproducts is multipliable (Proposition prop.fps.prods-mulable-rules.SW1).

(Theorem 7.3.11(f), label: thm.fps.xneq.props) (Also: Lemma lem.fps.prods-mulable-rules.SW1.lem1)

theorem PowerSeries.coeff_pow_eq_zero_of_constantCoeff_zero {K : Type u_1} [CommRing K] (g : PowerSeries K) (hg : constantCoeff g = 0) (n d : ℕ) (hd : d > n) : (coeff n) (g ^ d) = 0

When constantCoeff g = 0, the coefficient coeff n (g ^ d) is zero for d > n. This is because order(g) ≥ 1 implies order(g^d) ≥ d.

theorem PowerSeries.coeff_subst_eq_finite_sum {K : Type u_1} [CommRing K] (f g : PowerSeries K) (hg : constantCoeff g = 0) (n : ℕ) : (coeff n) (subst g f) = ∑ d ∈ Finset.range (n + 1), (coeff d) f • (coeff n) (g ^ d)

The n-th coefficient of f.subst g equals a finite sum over coefficients. When constantCoeff g = 0, only coefficients 0 through n of f contribute.

theorem PowerSeries.xnEquiv_subst {K : Type u_1} [CommRing K] {n : ℕ} {f₁ f₂ g₁ g₂ : PowerSeries K} (hf : f₁ ≡[x^n] f₂) (hg : g₁ ≡[x^n] g₂) (hg₁ : constantCoeff g₁ = 0) (hg₂ : constantCoeff g₂ = 0) : subst g₁ f₁ ≡[x^n] subst g₂ f₂

x^n-equivalence is compatible with composition (when inner series have zero constant term). This is the key lemma (Proposition 7.4.7 in Loehr).

theorem PowerSeries.coeff_mul_eq_of_coeff_eq {K : Type u_1} [CommRing K] {a b c d : PowerSeries K} {n : ℕ} (hab : ∀ m ≤ n, (coeff m) a = (coeff m) b) (hcd : ∀ m ≤ n, (coeff m) c = (coeff m) d) (m : ℕ) : m ≤ n → (coeff m) (a * c) = (coeff m) (b * d)

If two pairs of FPSs agree on their first n+1 coefficients, then their products also agree on those coefficients. (Lemma 7.3.15, label: lem.fps.prod.irlv.cong-mul)

This is a direct consequence of the fact that the k-th coefficient of a product only depends on coefficients 0 through k of each factor.

This is an alternative formulation of xnEquiv_mul using explicit coefficient equality.

theorem PowerSeries.xnEquiv_invOfUnit {K : Type u_1} [CommRing K] {n : ℕ} {f g : PowerSeries K} (u : Kˣ) (h : f ≡[x^n] g) : f.invOfUnit u ≡[x^n] g.invOfUnit u

x^n-equivalence is compatible with taking inverses (when constant coefficients are units). The key insight is that the coefficients of the inverse are determined by a recursive formula that only depends on lower coefficients.

theorem PowerSeries.xnEquiv_invOfUnit' {K : Type u_1} [CommRing K] {n : ℕ} {f g : PowerSeries K} (u v : Kˣ) (huv : ↑u = ↑v) (h : f ≡[x^n] g) : f.invOfUnit u ≡[x^n] g.invOfUnit v

x^n-equivalence is compatible with taking inverses (with different units that are equal as elements). This variant is useful when the units come from different IsUnit proofs but have the same value.

theorem PowerSeries.xnEquiv_div {K : Type u_1} [CommRing K] {n : ℕ} {a b c d : PowerSeries K} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (u : Kˣ) (hu : constantCoeff c = ↑u) (v : Kˣ) (hv : constantCoeff d = ↑v) : a * c.invOfUnit u ≡[x^n] b * d.invOfUnit v

x^n-equivalence is compatible with division (when denominators are invertible). (Theorem 7.3.11(e), label: thm.fps.xneq.props)

If a ≡[x^n] b and c ≡[x^n] d, and c, d are invertible, then a/c ≡[x^n] b/d.

theorem PowerSeries.coeff_div_eq_of_coeff_eq {K : Type u_1} [CommRing K] {a b c d : PowerSeries K} {n : ℕ} (hab : ∀ m ≤ n, (coeff m) a = (coeff m) b) (hcd : ∀ m ≤ n, (coeff m) c = (coeff m) d) (u : Kˣ) (hu : constantCoeff c = ↑u) (v : Kˣ) (hv : constantCoeff d = ↑v) (m : ℕ) : m ≤ n → (coeff m) (a * c.invOfUnit u) = (coeff m) (b * d.invOfUnit v)

If two pairs of FPSs agree on their first n+1 coefficients, and the denominators are invertible, then their quotients also agree on those coefficients. (Lemma 7.3.16, label: lem.fps.prod.irlv.cong-div)

This is a direct consequence of the fact that the k-th coefficient of a quotient only depends on coefficients 0 through k of each factor.

This is an alternative formulation of xnEquiv_div using explicit coefficient equality.

theorem PowerSeries.exists_xnEquiv_of_coeffStabilizesTo {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo f lim) (n : ℕ) : ∃ (N : ℕ), ∀ i ≥ N, f i ≡[x^n] lim

If f_i → f, then for each n, eventually f_i ≡[x^n] f. (Lemma 7.5.4, label: lem.fps.lim.xn-equiv)

theorem PowerSeries.coeffStabilizesTo_add {K : Type u_1} [CommRing K] {f g : ℕ → PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) : CoeffStabilizesTo (fun (i : ℕ) => f i + g i) (lf + lg)

Limits respect addition. (Proposition 7.5.5, label: prop.fps.lim.sum-prod)

theorem PowerSeries.coeffStabilizesTo_mul {K : Type u_1} [CommRing K] {f g : ℕ → PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) : CoeffStabilizesTo (fun (i : ℕ) => f i * g i) (lf * lg)

Limits respect multiplication. (Proposition 7.5.5, label: prop.fps.lim.sum-prod)

theorem PowerSeries.coeffStabilizesTo_finset_sum {K : Type u_1} [CommRing K] {ι : Type u_2} (s : Finset ι) {f : ι → ℕ → PowerSeries K} {lf : ι → PowerSeries K} (h : ∀ i ∈ s, CoeffStabilizesTo (f i) (lf i)) : CoeffStabilizesTo (fun (n : ℕ) => ∑ i ∈ s, f i n) (∑ i ∈ s, lf i)

Limits respect finite sums. (Corollary 7.5.6, label: cor.fps.lim.sum-prod-k)

theorem PowerSeries.coeffStabilizesTo_finset_prod {K : Type u_1} [CommRing K] {ι : Type u_2} (s : Finset ι) {f : ι → ℕ → PowerSeries K} {lf : ι → PowerSeries K} (h : ∀ i ∈ s, CoeffStabilizesTo (f i) (lf i)) : CoeffStabilizesTo (fun (n : ℕ) => ∏ i ∈ s, f i n) (∏ i ∈ s, lf i)

Limits respect finite products. (Corollary 7.5.6, label: cor.fps.lim.sum-prod-k)

theorem PowerSeries.coeffStabilizesTo_neg {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lf : PowerSeries K} (hf : CoeffStabilizesTo f lf) : CoeffStabilizesTo (fun (i : ℕ) => -f i) (-lf)

Limits respect negation.

theorem PowerSeries.coeffStabilizesTo_sub {K : Type u_1} [CommRing K] {f g : ℕ → PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) : CoeffStabilizesTo (fun (i : ℕ) => f i - g i) (lf - lg)

Limits respect subtraction.

theorem PowerSeries.isUnit_constantCoeff_of_coeffStabilizesTo {K : Type u_1} [CommRing K] {g : ℕ → PowerSeries K} {lg : PowerSeries K} (hg : CoeffStabilizesTo g lg) (hunit : ∀ (i : ℕ), IsUnit (constantCoeff (g i))) : IsUnit (constantCoeff lg)

If each g_i is invertible and g_i → g, then g is invertible.

theorem PowerSeries.unit_eq_of_coeffStabilizesTo {K : Type u_1} [CommRing K] {g : ℕ → PowerSeries K} {lg : PowerSeries K} (hg : CoeffStabilizesTo g lg) (hunit : ∀ (i : ℕ), IsUnit (constantCoeff (g i))) : ∃ (N : ℕ), ∀ i ≥ N, ⋯.unit = ⋯.unit

Helper: the unit from isUnit_constantCoeff_of_coeffStabilizesTo equals the unit from hunit i for sufficiently large i.

theorem PowerSeries.coeffStabilizesTo_invOfUnit {K : Type u_1} [CommRing K] {g : ℕ → PowerSeries K} {lg : PowerSeries K} (hg : CoeffStabilizesTo g lg) (hunit : ∀ (i : ℕ), IsUnit (constantCoeff (g i))) : CoeffStabilizesTo (fun (i : ℕ) => (g i).invOfUnit ⋯.unit) (lg.invOfUnit ⋯.unit)

Coefficients of invOfUnit stabilize when the input coefficients stabilize. This is the key lemma for proving that limits respect division.

theorem PowerSeries.coeffStabilizesTo_mul_inv {K : Type u_1} [CommRing K] {f g : ℕ → PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) (hunit : ∀ (i : ℕ), IsUnit (constantCoeff (g i))) : CoeffStabilizesTo (fun (i : ℕ) => f i * (g i).invOfUnit ⋯.unit) (lf * lg.invOfUnit ⋯.unit)

Limits respect division (when denominators are invertible). (Proposition 7.5.6, label: prop.fps.lim.sum-quot)

Note: We state this in terms of multiplication by the inverse.

theorem PowerSeries.coeffStabilizesTo_subst {K : Type u_1} [CommRing K] {f g : ℕ → PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) (hconst : ∀ (i : ℕ), constantCoeff (g i) = 0) : CoeffStabilizesTo (fun (i : ℕ) => subst (g i) (f i)) (subst lg lf)

Limits respect composition (when the inner FPS has zero constant term). (Proposition 7.5.7, label: prop.fps.lim.comp)

We use subst for composition.

theorem PowerSeries.coeffStabilizesTo_derivativeFun {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lf : PowerSeries K} (hf : CoeffStabilizesTo f lf) : CoeffStabilizesTo (fun (i : ℕ) => (f i).derivativeFun) lf.derivativeFun

Limits respect derivatives. (Proposition 7.5.8, label: prop.fps.lim.deriv-lim)

def PowerSeries.IsSummable {K : Type u_1} [CommRing K] (f : ℕ → PowerSeries K) : Prop

A family of FPSs is summable if for each n, only finitely many have nonzero n-th coeff.

Equations

• PowerSeries.IsSummable f = ∀ (n : ℕ), {i : ℕ | (PowerSeries.coeff n) (f i) ≠ 0}.Finite

noncomputable def PowerSeries.tsum' {K : Type u_1} [CommRing K] (f : ℕ → PowerSeries K) (hf : IsSummable f) : PowerSeries K

The infinite sum of a summable family.

Equations

• PowerSeries.tsum' f hf = PowerSeries.mk fun (n : ℕ) => ∑ i ∈ ⋯.toFinset, (PowerSeries.coeff n) (f i)

theorem PowerSeries.coeffStabilizesTo_partial_sum {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} (hf : IsSummable f) : CoeffStabilizesTo (fun (i : ℕ) => ∑ j ∈ Finset.range (i + 1), f j) (tsum' f hf)

Infinite sum is the limit of partial sums. (Theorem 7.5.9, label: thm.fps.lim.sum-lim)

The proof proceeds by showing that for each coefficient index n, the sequence of partial sums of n-th coefficients eventually equals the infinite sum. This follows from the summability condition: only finitely many terms have nonzero n-th coefficient, so once the partial sum includes all of these, it stabilizes.

def PowerSeries.IsMultipliable {K : Type u_1} [CommRing K] (f : ℕ → PowerSeries K) : Prop

A family of FPSs is multipliable if each has constant term 1 and for each n, eventually all terms are 1 + O(x^{n+1}).

Note: This is a more restrictive definition than PowerSeries.Multipliable in InfiniteProducts.lean. This definition is specifically designed for ℕ-indexed sequences where we consider limits of partial products ∏_{i=0}^{N} f_i.

The general PowerSeries.Multipliable a only requires that each coefficient is finitely determined, and works for arbitrary index types. For general infinite products, use the definitions in InfiniteProducts.lean.

Equations

• PowerSeries.IsMultipliable f = ((∀ (i : ℕ), PowerSeries.constantCoeff (f i) = 1) ∧ ∀ (n : ℕ), ∃ (N : ℕ), ∀ i ≥ N, ∀ k ≤ n, (PowerSeries.coeff k) (f i) = if k = 0 then 1 else 0)

noncomputable def PowerSeries.tprod' {K : Type u_1} [CommRing K] (f : ℕ → PowerSeries K) (hf : IsMultipliable f) : PowerSeries K

The infinite product of a multipliable family (ℕ-indexed version).

The n-th coefficient of the infinite product equals the n-th coefficient of any sufficiently large partial product.

Note: This is the ℕ-indexed version for use with IsMultipliable. For the general infinite product over arbitrary index types, use PowerSeries.tprod in InfiniteProducts.lean.

Equations

• PowerSeries.tprod' f hf = PowerSeries.mk fun (n : ℕ) => have N := ⋯.choose; (PowerSeries.coeff n) (∏ j ∈ Finset.range (N + 1), f j)

theorem PowerSeries.coeff_mul_one_plus_higher {K : Type u_1} [CommRing K] {g f : PowerSeries K} {n : ℕ} (hf : ∀ k ≤ n, (coeff k) f = if k = 0 then 1 else 0) (k : ℕ) : k ≤ n → (coeff k) (g * f) = (coeff k) g

If f has the form 1 + O(x^{n+1}), then (g * f) agrees with g on coefficients ≤ n. This is a key lemma for showing that partial products stabilize.

theorem PowerSeries.coeff_prod_extend {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {n m : ℕ} (hf : ∀ k ≤ n, (coeff k) (f m) = if k = 0 then 1 else 0) (k : ℕ) (hk : k ≤ n) : (coeff k) (∏ j ∈ Finset.range (m + 1), f j) = (coeff k) (∏ j ∈ Finset.range m, f j)

Extending the partial product by one more term that is 1 + O(x^{n+1}) doesn't change coefficients ≤ n.

theorem PowerSeries.coeff_prod_range_eq_of_ge {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {n N : ℕ} (hN : ∀ j ≥ N, ∀ k ≤ n, (coeff k) (f j) = if k = 0 then 1 else 0) {i : ℕ} (hi : i ≥ N) {k : ℕ} (hk : k ≤ n) : (coeff k) (∏ j ∈ Finset.range (i + 1), f j) = (coeff k) (∏ j ∈ Finset.range (N + 1), f j)

For a multipliable family, once the index exceeds N (where N witnesses the multipliability condition for n), the k-th coefficient of partial products stabilizes.

theorem PowerSeries.coeff_partial_prod_stabilizes {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} (hf : IsMultipliable f) (n : ℕ) : ∃ (N : ℕ), ∀ i ≥ N, (coeff n) (∏ j ∈ Finset.range (i + 1), f j) = (coeff n) (tprod' f hf)

For a multipliable family, the n-th coefficient of partial products stabilizes.

theorem PowerSeries.coeffStabilizesTo_partial_prod {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} (hf : IsMultipliable f) : CoeffStabilizesTo (fun (i : ℕ) => ∏ j ∈ Finset.range (i + 1), f j) (tprod' f hf)

Infinite product is the limit of partial products. (Theorem 7.5.10, label: thm.fps.lim.prod-lim)

theorem PowerSeries.coeffStabilizesTo_trunc {K : Type u_1} [CommRing K] (a : PowerSeries K) : CoeffStabilizesTo (fun (i : ℕ) => ↑((trunc (i + 1)) a)) a

Each FPS is a limit of polynomials. (Corollary 7.5.11, label: cor.fps.lim.fps-as-pol)

This can be restated as "the polynomials are dense in the FPSs".

theorem PowerSeries.isSummable_of_coeffStabilizesTo_partial_sum {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ℕ) => ∑ j ∈ Finset.range (i + 1), f j) lim) : IsSummable f

Converse of coeffStabilizesTo_partial_sum: if the partial sums converge, the family is summable. (Theorem 7.5.12, label: thm.fps.lim.sum-lim-conv)

theorem PowerSeries.tsum'_eq_of_coeffStabilizesTo_partial_sum {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ℕ) => ∑ j ∈ Finset.range (i + 1), f j) lim) : tsum' f ⋯ = lim

If partial sums converge, the limit equals the infinite sum. (Theorem 7.5.12, label: thm.fps.lim.sum-lim-conv)

theorem PowerSeries.constantCoeff_prod_eq_one {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {s : Finset ℕ} (hf : ∀ i ∈ s, constantCoeff (f i) = 1) : constantCoeff (∏ j ∈ s, f j) = 1

Helper lemma: constant coeff of product of power series with constant coeff 1 is 1.

theorem PowerSeries.isMultipliable_of_coeffStabilizesTo_partial_prod {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ℕ) => ∏ j ∈ Finset.range (i + 1), f j) lim) (hconst : ∀ (i : ℕ), constantCoeff (f i) = 1) : IsMultipliable f

Converse of coeffStabilizesTo_partial_prod: if the partial products converge, the family is multipliable. (Theorem 7.5.13, label: thm.fps.lim.prod-lim-conv)

theorem PowerSeries.tprod'_eq_of_coeffStabilizesTo_partial_prod {K : Type u_1} [CommRing K] {f : ℕ → PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ℕ) => ∏ j ∈ Finset.range (i + 1), f j) lim) (hconst : ∀ (i : ℕ), constantCoeff (f i) = 1) : tprod' f ⋯ = lim

If partial products converge, the limit equals the infinite product. (Theorem 7.5.13, label: thm.fps.lim.prod-lim-conv)