Upper bounds on Cantor–Bendixson values of Hahn products

In an ordered uniform exponent group that is Cauchy complete, every derivative point of a product support lifts to a pair in the closed factor supports with a sufficient natural sum of ranks. For nonpositive supports the only pair summing to zero is (0, 0), giving submultiplicativity of the value. This is an upper bound only; coefficient cancellation is not excluded.

theorem HahnSeries.closedSupport_mul_subset_add {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [NonUnitalNonAssocSemiring R] (b d : HahnSeries G R) : ↑(b * d).closedSupport ⊆ ↑b.closedSupport + ↑d.closedSupport

The closed support of a product is contained in the sum of the closed supports.

theorem HahnSeries.exists_cantorBendixsonRank_add_ge_of_mem_mul_derivative {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [NonUnitalNonAssocSemiring R] (b d : HahnSeries G R) (o : Ordinal.{u}) {z : G} (hz : z ∈ ↑((b * d).closedSupport.cantorBendixson o)) : ∃ x ∈ b.closedSupport, ∃ y ∈ d.closedSupport, x + y = z ∧ o ≤ NatOrdinal.val (NatOrdinal.of (b.cantorBendixsonRank x) + NatOrdinal.of (d.cantorBendixsonRank y))

A product derivative point lifts to closed-support summands whose ranks bound its stage.

theorem HahnSeries.cantorBendixsonRank_mul_le {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [NonUnitalNonAssocSemiring R] (b d : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (hd : d.support ⊆ Set.Iic 0) (h : 0 ∈ closure (b * d).support) : 0 ∈ closure b.support ∧ 0 ∈ closure d.support ∧ (b * d).cantorBendixsonRank 0 ≤ NatOrdinal.val (NatOrdinal.of (b.cantorBendixsonRank 0) + NatOrdinal.of (d.cantorBendixsonRank 0))

For nonpositive supports, the product rank at zero is bounded by the natural sum.

theorem HahnSeries.cantorBendixsonValue_mul_le {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [NonUnitalNonAssocSemiring R] (b d : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (hd : d.support ⊆ Set.Iic 0) : NatOrdinal.of (b * d).cantorBendixsonValue ≤ NatOrdinal.of b.cantorBendixsonValue * NatOrdinal.of d.cantorBendixsonValue

The value of a product with nonpositive supports is bounded by the natural product.

theorem HahnSeries.cantorBendixsonValue_pow_le {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 : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (m : ℕ) : NatOrdinal.of (b ^ m).cantorBendixsonValue ≤ NatOrdinal.of b.cantorBendixsonValue ^ m

A nonnegative integer power is bounded by the natural power of the original value.

theorem HahnSeries.cantorBendixsonValue_single_zero_mul {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [OrderTopology G] [Ring R] [NoZeroDivisors R] (b : HahnSeries G R) {a : R} (ha : a ≠ 0) : ((single 0) a * b).cantorBendixsonValue = b.cantorBendixsonValue

Multiplication by a nonzero ordinary scalar preserves the value.

theorem HahnSeries.cantorBendixsonValue_mul_eq_zero_of_left {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) (hz : b.cantorBendixsonValue = 0) : (b * d).cantorBendixsonValue = 0

A nonpositive factor of value zero makes the product value zero.

theorem HahnSeries.cantorBendixsonValue_mul_of_left_eq_one {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [UniformSpace G] [IsUniformAddGroup G] [OrderTopology G] [Nontrivial G] [CompleteSpace G] [Ring R] [NoZeroDivisors R] (b d : HahnSeries G R) (hb : b.support ⊆ Set.Iic 0) (hd : d.support ⊆ Set.Iic 0) (hone : b.cantorBendixsonValue = 1) : (b * d).cantorBendixsonValue = d.cantorBendixsonValue

A nonpositive factor of value one preserves the other factor's value.