Degree bounds for translated truncations

Translated closed truncation at a real exponent does not increase Hahn-series degree. Since Berarducci's ordinal-value degree is bounded by Hahn-series degree, the same bound holds for the ordinal-value degree of every translated truncation.

theorem Berarducci.degree_translatedTruncation_le {K : Type v} [Field K] (b : HahnSeries ℝ K) (γ : ℝ) : (↑(translatedTruncation b γ)).degree ≤ b.degree

Translated closed truncation does not increase Hahn-series degree.

theorem Berarducci.ordinalValueDegree_translatedTruncation_le_degree {K : Type v} [Field K] (b : HahnSeries ℝ K) (γ : ℝ) : ordinalValueDegree (translatedTruncation b γ) ≤ b.degree

The ordinal-value degree of a translated closed truncation is bounded by the degree of the original Hahn series.