Existence of Berarducci critical points #
Berarducci, Lemma 10.1 proves that the ordinal values of all translated truncations of a nonzero nonpositive real Hahn series have a maximum. Definition 10.2 chooses the least nonpositive cutoff where that maximum occurs.
The proof realizes the maximum through the LM24 normal form. Its principal head has the same degree as the full series. Truncating at the head exponent recovers that principal coefficient up to a constant, so its ordinal-value degree reaches the upper bound for every translated truncation. The maximizers lie in the closed support, which is partially well ordered, and therefore have a least element.
References #
- A. Berarducci, Factorization in generalized power series, Trans. Amer. Math. Soc. 352 (2000), 553–577, cited as [Ber00].
theorem
Berarducci.exists_isCriticalPoint
{K : Type v}
[Field K]
{b : Series K}
(hb : b ≠ 0)
:
∃ (x : ℝ), IsCriticalPoint b x
Berarducci, Lemma 10.1 and Definition 10.2: every nonzero nonpositive real Hahn series has a critical point.