x^n-Equivalence of Formal Power Series

This file formalizes the notion of x^n-equivalence of formal power series from Section sec.gf.xneq of the source text.

Main Definitions

• PowerSeries.XnEquiv n f g: Two FPS are x^n-equivalent if their first n+1 coefficients agree. This is written as f ≡ g [mod X^(n+1)] in the source, and is equivalent to X^(n+1) ∣ (f - g).

Main Results

• PowerSeries.XnEquiv.equivalence: x^n-equivalence is an equivalence relation.
• PowerSeries.XnEquiv.add: x^n-equivalence is preserved by addition.
• PowerSeries.XnEquiv.sub: x^n-equivalence is preserved by subtraction.
• PowerSeries.XnEquiv.mul: x^n-equivalence is preserved by multiplication.
• PowerSeries.XnEquiv.smul: x^n-equivalence is preserved by scalar multiplication.
• PowerSeries.XnEquiv.invOfUnit: x^n-equivalence is preserved by inversion (for invertible FPS).
• PowerSeries.XnEquiv.sum: x^n-equivalence is preserved by finite sums.
• PowerSeries.XnEquiv.prod: x^n-equivalence is preserved by finite products.
• PowerSeries.xnEquiv_iff_dvd: f ≡ g [mod X^(n+1)] iff X^(n+1) ∣ (f - g).
• PowerSeries.XnEquiv.comp: x^n-equivalence is preserved by composition (with constant term 0).

Implementation Notes

We define x^n-equivalence in terms of coefficient equality rather than divisibility, as this is more directly usable in proofs. The equivalence to divisibility is established in xnEquiv_iff_dvd.

The definition uses n for the degree, so XnEquiv n f g means the first n+1 coefficients agree (i.e., coefficients 0, 1, ..., n).

References

• Section sec.gf.xneq (x^n-equivalence) of the source text.

Tags

power series, equivalence, truncation, congruence

Definition of x^n-equivalence

def PowerSeries.XnEquiv {R : Type u_1} [CommSemiring R] (n : ℕ) (f g : PowerSeries R) : Prop

Two formal power series are x^n-equivalent if their first n+1 coefficients agree. This corresponds to Definition def.fps.xneq in the source text.

We say XnEquiv n f g to mean that for all m ∈ {0, 1, ..., n}, we have [x^m] f = [x^m] g.

Equations

• (f ≡[x^n] g) = ∀ m ≤ n, (PowerSeries.coeff m) f = (PowerSeries.coeff m) g

def PowerSeries.«term_≡[x^_]_» : Lean.TrailingParserDescr

Notation for x^n-equivalence: f ≡[x^n] g means XnEquiv n f g. This notation is used throughout the limits and infinite products theory.

Equations

• One or more equations did not get rendered due to their size.

Basic properties: Equivalence relation (Theorem thm.fps.xneq.props (a))

theorem PowerSeries.XnEquiv.refl {R : Type u_1} [CommSemiring R] (n : ℕ) (f : PowerSeries R) : f ≡[x^n] f

x^n-equivalence is reflexive.

theorem PowerSeries.XnEquiv.symm {R : Type u_1} [CommSemiring R] {n : ℕ} {f g : PowerSeries R} (h : f ≡[x^n] g) : g ≡[x^n] f

x^n-equivalence is symmetric.

theorem PowerSeries.XnEquiv.trans {R : Type u_1} [CommSemiring R] {n : ℕ} {f g h : PowerSeries R} (hfg : f ≡[x^n] g) (hgh : g ≡[x^n] h) : f ≡[x^n] h

x^n-equivalence is transitive.

theorem PowerSeries.XnEquiv.equivalence {R : Type u_1} [CommSemiring R] (n : ℕ) : Equivalence (XnEquiv n)

x^n-equivalence is an equivalence relation (Theorem thm.fps.xneq.props (a)).

theorem PowerSeries.XnEquiv.of_le {R : Type u_1} [CommSemiring R] {m n : ℕ} (hmn : m ≤ n) {f g : PowerSeries R} (h : f ≡[x^n] g) : f ≡[x^m] g

x^n-equivalence implies x^m-equivalence for m ≤ n.

Simp lemmas for basic cases

@[simp]

theorem PowerSeries.XnEquiv_zero_iff {R : Type u_1} [CommSemiring R] (f g : PowerSeries R) : (f ≡[x^0] g) ↔ constantCoeff f = constantCoeff g

x^0-equivalence is equivalent to having equal constant coefficients. This is a useful simplification lemma for the base case of x^n-equivalence.

@[simp]

theorem PowerSeries.XnEquiv_self {R : Type u_1} [CommSemiring R] (n : ℕ) (f : PowerSeries R) : f ≡[x^n] f

Any FPS is x^n-equivalent to itself (reflexivity as a simp lemma).

Algebraic properties (Theorem thm.fps.xneq.props (b), (c))

theorem PowerSeries.XnEquiv.add {R : Type u_1} [CommSemiring R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) : a + c ≡[x^n] b + d

x^n-equivalence is preserved by addition (Theorem thm.fps.xneq.props (b), eq.thm.fps.xneq.props.b.+).

theorem PowerSeries.XnEquiv.sub {R : Type u_2} [CommRing R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) : a - c ≡[x^n] b - d

x^n-equivalence is preserved by subtraction (Theorem thm.fps.xneq.props (b), eq.thm.fps.xneq.props.b.-).

theorem PowerSeries.XnEquiv.smul {R : Type u_1} [CommSemiring R] {n : ℕ} {a b : PowerSeries R} (hab : a ≡[x^n] b) (r : R) : r • a ≡[x^n] r • b

x^n-equivalence is preserved by scalar multiplication (Theorem thm.fps.xneq.props (c)).

theorem PowerSeries.XnEquiv.mul {R : Type u_1} [CommSemiring R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) : a * c ≡[x^n] b * d

x^n-equivalence is preserved by multiplication (Theorem thm.fps.xneq.props (b), eq.thm.fps.xneq.props.b.*).

Inversion (Theorem thm.fps.xneq.props (d))

theorem PowerSeries.XnEquiv.neg {R : Type u_2} [CommRing R] {n : ℕ} {a b : PowerSeries R} (hab : a ≡[x^n] b) : -a ≡[x^n] -b

x^n-equivalence is preserved by negation.

theorem PowerSeries.XnEquiv.invOfUnit {R : Type u_2} [CommRing R] {n : ℕ} {a b : PowerSeries R} (ua ub : Rˣ) (ha : constantCoeff a = ↑ua) (hb : constantCoeff b = ↑ub) (hab : a ≡[x^n] b) : a.invOfUnit ua ≡[x^n] b.invOfUnit ub

x^n-equivalence is preserved by inversion via invOfUnit for FPS with invertible constant term (Theorem thm.fps.xneq.props (d)).

The proof proceeds by strong induction on the coefficient index, using the formula for coefficients of the inverse.

theorem PowerSeries.XnEquiv.inv {K : Type u_2} [Field K] {n : ℕ} {a b : PowerSeries K} (ha : constantCoeff a ≠ 0) (hb : constantCoeff b ≠ 0) (hab : a ≡[x^n] b) : a⁻¹ ≡[x^n] b⁻¹

x^n-equivalence is preserved by inversion for FPS over a field (Theorem thm.fps.xneq.props (d)).

theorem PowerSeries.XnEquiv.invOfUnit' {R : Type u_2} [CommRing R] {n : ℕ} {f g : PowerSeries R} (u v : Rˣ) (huv : ↑u = ↑v) (hfg : f ≡[x^n] g) : f.invOfUnit u ≡[x^n] g.invOfUnit v

Variant of XnEquiv.invOfUnit where the units may be different but their values agree. This is useful when working with limits where we have different units for each term.

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

x^n-equivalence is preserved by division (Theorem thm.fps.xneq.props (e)).

Finite sums and products (Theorem thm.fps.xneq.props (f))

theorem PowerSeries.XnEquiv.sum {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] {n : ℕ} {s : Finset ι} {a b : ι → PowerSeries R} (h : ∀ i ∈ s, a i ≡[x^n] b i) : ∑ i ∈ s, a i ≡[x^n] ∑ i ∈ s, b i

x^n-equivalence is preserved by finite sums (Theorem thm.fps.xneq.props (f), eq.thm.fps.xneq.props.e.+).

theorem PowerSeries.XnEquiv.prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] {n : ℕ} {s : Finset ι} {a b : ι → PowerSeries R} (h : ∀ i ∈ s, a i ≡[x^n] b i) : ∏ i ∈ s, a i ≡[x^n] ∏ i ∈ s, b i

x^n-equivalence is preserved by finite products (Theorem thm.fps.xneq.props (f), eq.thm.fps.xneq.props.e.*).

Characterization via divisibility (Proposition prop.fps.xneq-multiple)

This section proves prop.fps.xneq-multiple: Two FPS f and g satisfy f ≡ g [mod X^(n+1)] if and only if the FPS f - g is a multiple of X^(n+1).

theorem PowerSeries.xnEquiv_iff_dvd {R : Type u_3} [CommRing R] {n : ℕ} {f g : PowerSeries R} : (f ≡[x^n] g) ↔ X ^ (n + 1) ∣ f - g

x^n-equivalence is equivalent to divisibility by X^(n+1) (Proposition prop.fps.xneq-multiple).

Two FPS f and g satisfy f ≡ g [mod X^(n+1)] if and only if X^(n+1) divides f - g.

This is the main characterization theorem that connects the coefficient-wise definition of x^n-equivalence to the divisibility formulation.

theorem PowerSeries.xnEquiv_iff_sub_eq_mul_X_pow {R : Type u_3} [CommRing R] {n : ℕ} {f g : PowerSeries R} : (f ≡[x^n] g) ↔ ∃ (q : PowerSeries R), f - g = X ^ (n + 1) * q

Alternative statement of prop.fps.xneq-multiple: f ≡ g [mod X^(n+1)] iff f - g is a multiple of X^(n+1).

This is definitionally equal to xnEquiv_iff_dvd since divisibility is defined as the existence of such a quotient. The explicit existential form is sometimes more convenient to work with.

Truncation characterization

theorem PowerSeries.xnEquiv_iff_trunc {R : Type u_1} [CommSemiring R] {n : ℕ} {f g : PowerSeries R} : (f ≡[x^n] g) ↔ (trunc (n + 1)) f = (trunc (n + 1)) g

x^n-equivalence is equivalent to having equal truncations.

theorem PowerSeries.exists_polynomial_xnEquiv {R : Type u_1} [CommSemiring R] (n : ℕ) (f : PowerSeries R) : ∃ (p : Polynomial R), f ≡[x^n] ↑p

Every FPS is x^n-equivalent to some polynomial (Example (d) in the source).

Powers

theorem PowerSeries.XnEquiv.pow {R : Type u_1} [CommSemiring R] {n : ℕ} {a b : PowerSeries R} (hab : a ≡[x^n] b) (k : ℕ) : a ^ k ≡[x^n] b ^ k

x^n-equivalence is preserved by powers.

Composition (Proposition prop.fps.xneq.comp)

theorem PowerSeries.coeff_pow_eq_zero_of_lt_of_constantCoeff_eq_zero {R : Type u_3} [CommRing R] {f : PowerSeries R} (hf : constantCoeff f = 0) {m k : ℕ} (hmk : m < k) : (coeff m) (f ^ k) = 0

Coefficients of f^k are zero for indices < k when constantCoeff f = 0. This is a key lemma for proving that composition preserves x^n-equivalence.

theorem PowerSeries.XnEquiv.comp {R : Type u_3} [CommRing R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (hc : constantCoeff c = 0) (hd : constantCoeff d = 0) : subst c a ≡[x^n] subst d b

x^n-equivalence is preserved by composition when the inner series have constant term 0 (Proposition prop.fps.xneq.comp).

If a ≡ b [mod X^(n+1)] and c ≡ d [mod X^(n+1)] with [x^0]c = 0 and [x^0]d = 0, then a ∘ c ≡ b ∘ d [mod X^(n+1)].

The proof follows the sketch in the source text:

1. Write a = ∑ aᵢ xⁱ and b = ∑ bᵢ xⁱ
2. For i ≤ n: aᵢ = bᵢ (by hab) and c^i ≡ d^i [mod X^(n+1)] (by XnEquiv.pow)
3. For i > n: x^m = x^m = 0 for all m ≤ n (since constantCoeff = 0)
4. Therefore a ∘ c ≡ b ∘ d [mod X^(n+1)]

Connection to equality

theorem PowerSeries.eq_iff_forall_xnEquiv {R : Type u_1} [CommSemiring R] {f g : PowerSeries R} : f = g ↔ ∀ (n : ℕ), f ≡[x^n] g

Two FPS are equal iff they are x^n-equivalent for all n.