The polar-part Rota–Baxter operator on Laurent series [UPSTREAM]

The prototype Rota–Baxter operator of weight -1 ([MCB25] Prop. 3.5.2, eq. (3.5.4)) — the minimal-subtraction operator of Connes–Kreimer renormalization in physics. On the Laurent series LaurentSeries A = HahnSeries ℤ A, the projection onto the polar part (the strictly-negative-degree coefficients),

R(Σ aᵢ tⁱ) = Σ_{i < 0} aᵢ tⁱ,

is a Rota–Baxter operator of weight -1. This realizes the example named in RotaBaxter.lean's docstring (the Laurent-series polar projection) and is the operator [MCB25] §3.5.2 use to recast Minimal Yield as a Birkhoff factorization (Sideward Merge appears as the polar/divergent part, removed by the renormalized character).

The Rota–Baxter identity is proved from the splitting LaurentSeries A = R ⊕ (1 − R) into the two subalgebras of polar (support < 0) and non-polar (support ≥ 0) series: R fixes products of polar parts and kills products of non-polar parts, because support (x * y) ⊆ support x + support y (HahnSeries.support_mul_subset).

Implementation notes

The lemmas are stated at the coefficient function level (polarHahn, not a packaged LinearMap) and the op field of rotaBaxterPolar is constructed inline, so its module is the expected Algebra.toModule rather than HahnSeries.instModule. This avoids the Module-instance diamond on LaurentSeries A (the two modules are defeq but distinct terms, and reconciling them runs isDefEq through the noncomputable Laurent multiplication) — the same way mathlib proves the HahnSeries ring axioms directly at the coefficient level rather than by transporting packaged maps.

Main definitions

• LaurentSeries.polarHahn: the polar projection on coefficients.
• LaurentSeries.rotaBaxterPolar: the weight--1 Rota–Baxter operator structure.

References

[MCB25] (Prop. 3.5.2, eq. (3.5.4))

def LaurentSeries.polarHahn {A : Type u_2} [CommRing A] (s : LaurentSeries A) : LaurentSeries A

The polar part of a Laurent series: the strictly-negative-degree part ([MCB25] eq. (3.5.4)).

Equations

• s.polarHahn = { coeff := LaurentSeries.polarCoeff✝ s, isPWO_support' := ⋯ }

@[simp]

theorem LaurentSeries.coeff_polarHahn {A : Type u_2} [CommRing A] (s : LaurentSeries A) (i : ℤ) : s.polarHahn.coeff i = if i < 0 then s.coeff i else 0

@[simp]

theorem LaurentSeries.polarHahn_zero {A : Type u_2} [CommRing A] : polarHahn 0 = 0

theorem LaurentSeries.polarHahn_add {A : Type u_2} [CommRing A] (x y : LaurentSeries A) : (x + y).polarHahn = x.polarHahn + y.polarHahn

theorem LaurentSeries.polarHahn_sub {A : Type u_2} [CommRing A] (x y : LaurentSeries A) : (x - y).polarHahn = x.polarHahn - y.polarHahn

@[simp]

theorem LaurentSeries.polarHahn_polarHahn {A : Type u_2} [CommRing A] (s : LaurentSeries A) : s.polarHahn.polarHahn = s.polarHahn

R is idempotent: projecting onto the polar part twice is projecting once.

@[simp]

theorem LaurentSeries.polarHahn_sub_self {A : Type u_2} [CommRing A] (s : LaurentSeries A) : (s - s.polarHahn).polarHahn = 0

The complement (1 − R) s = s − R s is nonpolar: R annihilates it. So 1 − R projects onto the nonpolar subring DM[[t]].

The two subalgebras of the splitting

theorem LaurentSeries.polarHahn_eq_self {A : Type u_2} [CommRing A] (s : LaurentSeries A) (h : ∀ (i : ℤ), 0 ≤ i → s.coeff i = 0) : s.polarHahn = s

R fixes a series supported on strictly-negative degrees.

theorem LaurentSeries.polarHahn_eq_zero {A : Type u_2} [CommRing A] (s : LaurentSeries A) (h : ∀ i < 0, s.coeff i = 0) : s.polarHahn = 0

R kills a series supported on non-negative degrees.

@[simp]

theorem LaurentSeries.polarHahn_one {A : Type u_2} [CommRing A] : polarHahn 1 = 0

1 = t⁰ is nonpolar.

theorem LaurentSeries.support_subset_nonneg {A : Type u_2} [CommRing A] (s : LaurentSeries A) (hs : s.polarHahn = 0) : HahnSeries.support s ⊆ {i : ℤ | 0 ≤ i}

A nonpolar series (R s = 0) is supported on non-negative degrees.

theorem LaurentSeries.polarHahn_mul {A : Type u_2} [CommRing A] (a b : LaurentSeries A) (ha : a.polarHahn = 0) (hb : b.polarHahn = 0) : (a * b).polarHahn = 0

The nonpolar series form a subalgebra: a product of nonpolar series is nonpolar.

theorem LaurentSeries.support_polarHahn_subset {A : Type u_2} [CommRing A] (s : LaurentSeries A) : HahnSeries.support s.polarHahn ⊆ {i : ℤ | i < 0}

The polar part is supported on strictly-negative degrees.

theorem LaurentSeries.support_sub_polarHahn_subset {A : Type u_2} [CommRing A] (s : LaurentSeries A) : HahnSeries.support (s - s.polarHahn) ⊆ {i : ℤ | 0 ≤ i}

The complementary part 1 − R is supported on non-negative degrees.

theorem LaurentSeries.polarMul_coeff_eq_zero_of_nonneg {A : Type u_2} [CommRing A] (a b : LaurentSeries A) {i : ℤ} (hi : 0 ≤ i) : (a.polarHahn * b.polarHahn).coeff i = 0

A product of polar parts has no non-negative-degree coefficients (the polar series form a subalgebra).

theorem LaurentSeries.coPolarMul_coeff_eq_zero_of_neg {A : Type u_2} [CommRing A] (a b : LaurentSeries A) {i : ℤ} (hi : i < 0) : ((a - a.polarHahn) * (b - b.polarHahn)).coeff i = 0

A product of non-polar parts has no strictly-negative-degree coefficients (the non-polar series form a subalgebra).

The Rota–Baxter operator

theorem LaurentSeries.polarHahn_rotaBaxter {A : Type u_2} [CommRing A] (a b : LaurentSeries A) : a.polarHahn * b.polarHahn = (a.polarHahn * b + a * b.polarHahn - a * b).polarHahn

The polar-projection Rota–Baxter identity (weight -1, sub-form) ([MCB25] Prop. 3.5.2): R(a)R(b) = R(R(a)b + aR(b) − ab), from the ring identity R(a)b + aR(b) − ab = R(a)R(b) − (a−R(a))(b−R(b)) and the splitting into the two subalgebras (R fixes R(a)R(b), kills (a−R(a))(b−R(b))).

noncomputable def LaurentSeries.rotaBaxterPolar {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] : RotaBaxter k (LaurentSeries A) (-1)

The polar projection is a Rota–Baxter operator of weight -1 on LaurentSeries A ([MCB25] Prop. 3.5.2): the prototype minimal-subtraction operator. The op linear map is built inline with letI := Algebra.toModule to pin the expected module (see the implementation note); map_smul' is then over the algebra action c • x = algebraMap c * x.

Equations

• LaurentSeries.rotaBaxterPolar = { op := { toFun := LaurentSeries.polarHahn, map_add' := ⋯, map_smul' := ⋯ }, rotaBaxter := ⋯ }

@[simp]

theorem LaurentSeries.rotaBaxterPolar_op_apply {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (s : LaurentSeries A) : rotaBaxterPolar.op s = s.polarHahn