HahnSeries.SummableFamily.finite_co_support
theorem HahnSeries.SummableFamily.finite_co_support :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_3}
(s : HahnSeries.SummableFamily Γ R α) (g : Γ), (Function.support fun a => (s a).coeff g).Finite
This theorem states that for any summable family `s` of Hahn series, indexed by a type `α`, where each series has coefficients from an additive commutative monoid `R` and its index set is ordered by a partial order `Γ`, and for any index `g` from `Γ`, the set of indices `a` from `α` for which the coefficient of `g` in the series `s a` is non-zero is finite. In other words, only finitely many series in the summable family have a non-zero coefficient at a given index.
More concisely: For any summable family of Hahn series indexed by a type with a partial order, indexed by an additive commutative monoid, only finitely many series have a non-zero coefficient at any given index.
|
HahnSeries.SummableFamily.ext
theorem HahnSeries.SummableFamily.ext :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_3}
{s t : HahnSeries.SummableFamily Γ R α}, (∀ (a : α), s a = t a) → s = t
This theorem states that for any type `Γ` with a partial order, any type `R` with an additive commutative monoid structure, and any additional type `α`, if we have two summable families of Hahn series `s` and `t` indexed by `α`, then `s` and `t` are equal if and only if they are equal at every index `a` in `α`. Essentially, it says that two summable families of Hahn series are equal if they produce the same series for each index in the family.
More concisely: Given types `Γ` with a partial order, `R` with an additive commutative monoid structure, and `α`, if `s` and `t` are two summable families of Hahn series indexed by `α` over `Γ` and `R`, then `s = t` if and only if `s a = t a` for all `a ∈ α`.
|
HahnSeries.unit_aux
theorem HahnSeries.unit_aux :
∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrderedAddCommGroup Γ] [inst_1 : CommRing R] [inst_2 : IsDomain R]
(x : HahnSeries Γ R) {r : R},
r * x.coeff x.order = 1 →
0 < (HahnSeries.addVal Γ R) (1 - HahnSeries.C r * (HahnSeries.single (-x.order)) 1 * x)
The theorem `HahnSeries.unit_aux` states that for any type `Γ` which forms a linearly ordered additive commutative group, any commutative ring `R`, an instance of `R` being an integral domain, a given Hahn series `x` over `Γ` and `R`, and a real number `r`, if the product of `r` and the coefficient of `x` at the order of `x` equals 1, then the additive valuation of the difference between 1 and the product of the constant Hahn series `r`, the Hahn series which has a coefficient of 1 at `-order x` and zero elsewhere, and `x` itself is positive.
In simpler terms, if we can multiply a coefficient of our Hahn series `x` by some number `r` to get 1, then the additive valuation (which gives the smallest index with a nonzero coefficient) of a certain Hahn series related to `x` and `r` will be a positive value.
More concisely: For any Hahn series `x` over a linearly ordered additive commutative group `Γ` and an integral domain `R`, if the coefficient of `x` at `-order x` multiplied by a real number `r` equals 1, then the additive valuation of `1 - r * x` is positive.
|
HahnSeries.SummableFamily.isPWO_iUnion_support
theorem HahnSeries.SummableFamily.isPWO_iUnion_support :
∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {α : Type u_3}
(s : HahnSeries.SummableFamily Γ R α), (⋃ a, (s a).support).IsPWO
This theorem states that for all types `Γ`, `R`, and `α`, and given a partial order on `Γ` and an additive commutative monoid on `R`, for any summable family `s` of Hahn series over `Γ` and `R` indexed by `α`, the set union of the supports of the Hahn series in the summable family is partially well-ordered. In other words, any infinite sequence from this set union contains a monotone subsequence of length 2, i.e., an infinite monotone subsequence. The "support" of a Hahn series is defined as the set of indices whose coefficients are nonzero, and being "partially well-ordered" is a property of a subset of a preorder.
More concisely: Given a summable family of Hahn series over a partially ordered type `Γ` and an additive commutative monoid `R`, the set union of their supports is a partially well-ordered set, containing an infinite monotone subsequence.
|