Leibniz remainders for the Cantor–Bendixson value

For nonpositive Hahn series, the endpoint pairs of the finite convolution give the two product-rule terms. All remaining pairs have both coordinates strictly between the cutoff and zero. Strict local rank decrease and the canonical ordinal factorisation then bound the remainder by the first value's residual factor times the second value, provided the first principal factor is no larger. Multiplication in this bound is Hessenberg multiplication.

These are remainder estimates for the ambient Cantor–Bendixson value, not claims about the ordinary support-order value on a general exponent group. They use ordered uniform exponent groups that are Cauchy complete and ring coefficients; neither density nor characteristic zero is assumed.

theorem HahnSeries.cantorBendixsonValue_leibnizRemainder_lt_of_forall {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [Ring R] (b d : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (hd : d.support ⊆ Set.Iic 0) {γ : G} (hγ : γ < 0) {ρ : Ordinal.{u}} (hρ : 0 < ρ) (hterm : ∀ (x y : G), γ < x → x < 0 → γ < y → y < 0 → x + y = γ → ((translate (-x)) ((truncLE x) b) * (translate (-y)) ((truncLE y) d)).cantorBendixsonValue < ρ) : ((translate (-γ)) ((truncLE γ) (b * d)) - (translate (-γ)) ((truncLE γ) b) * d - b * (translate (-γ)) ((truncLE γ) d)).cantorBendixsonValue < ρ

Removing the two endpoint terms leaves only interior convolution products, up to value zero. A common strict positive bound on those products therefore bounds the Leibniz remainder.

theorem HahnSeries.eventually_cantorBendixsonValue_leibnizRemainder_lt_of_le_wpow {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [Ring R] (b d : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (hd : d.support ⊆ Set.Iic 0) (α β : NatOrdinal) (hv : NatOrdinal.of b.cantorBendixsonValue ≤ ω^ (α + 1)) (hw : NatOrdinal.of d.cantorBendixsonValue ≤ ω^ β) : ∀ᶠ (γ : G) in nhdsWithin 0 (Set.Iio 0), NatOrdinal.of ((translate (-γ)) ((truncLE γ) (b * d)) - (translate (-γ)) ((truncLE γ) b) * d - b * (translate (-γ)) ((truncLE γ) d)).cantorBendixsonValue < ω^ (α + β)

A successor exponent bound on the first value gives the corresponding strict remainder bound. This includes zero values and a second value at most one.

theorem HahnSeries.eventually_cantorBendixsonValue_leibnizRemainder_lt {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [Ring R] (b d : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (hd : d.support ⊆ Set.Iic 0) (B D : Ordinal.AdditivePrincipalAboveOne) (hB : b.cantorBendixsonValue = ↑B) (hD : d.cantorBendixsonValue = ↑D) (hp : B.principalFactor ≤ D.principalFactor) : ∀ᶠ (γ : G) in nhdsWithin 0 (Set.Iio 0), NatOrdinal.of ((translate (-γ)) ((truncLE γ) (b * d)) - (translate (-γ)) ((truncLE γ) b) * d - b * (translate (-γ)) ((truncLE γ) d)).cantorBendixsonValue < NatOrdinal.of B.residualFactor * NatOrdinal.of ↑D

If the first value has no larger final canonical factor, the Leibniz remainder is eventually strictly below the natural product of its residual factor with the second value.