Berarducci's main lemma

Berarducci, Lemma 8.2. Assuming v_J^p(b) ≤ v_J^p(c) and that, for residual points of b close to zero, the value of b^{|γ} b^m c^2 is the expected Hessenberg product, the value of b^{m+1} c is the expected Hessenberg product too.

The argument multiplies the product-rule estimate by c. Assuming for contradiction that v_J(b^{m+1} c) falls short, continuity of ordinal multiplication at the principal value bounds it by a proper multiple of the remainder bound, which makes the term b^{m+1} c c^{|γ} small as well. What survives is the term supplied by the hypothesis, whose value is exactly the remainder bound times v_J(c); its natural-number coefficient is invertible because the coefficient field has characteristic zero. Submultiplicativity then divides by c, and Lemma 6.9 turns the resulting bound along the residual points into the missing lower bound on v_J(b^{m+1} c).

The statement is placed with the residual-point statements because its proof uses Lemma 6.9.

theorem Berarducci.ordinalValue_pow_mul_eq_of_eventually {K : Type v} [Field K] [CharZero K] (b c : SeriesWithOrdinalValueAboveOne K) (hp : b.principalValue ≤ c.principalValue) (m : ℕ) (hyp : ∀ᶠ (γ : ℝ) in nhdsWithin 0 (Set.Iio 0), γ ∈ residualPointSet b → ordinalValue (translatedTruncation (↑↑b) γ * ↑b ^ m * ↑c ^ 2) = ordinalValue ↑b ^ m * ordinalValue (translatedTruncation (↑↑b) γ) * ordinalValue ↑c * ordinalValue ↑c) : ordinalValue (↑b ^ (m + 1) * ↑c) = ordinalValue ↑b ^ (m + 1) * ordinalValue ↑c

Berarducci, Lemma 8.2.

theorem Berarducci.ordinalValue_pow_eq_of_eventually {K : Type v} [Field K] [CharZero K] (b : SeriesWithOrdinalValueAboveOne K) (m : ℕ) (hyp : ∀ᶠ (γ : ℝ) in nhdsWithin 0 (Set.Iio 0), γ ∈ residualPointSet b → ordinalValue (translatedTruncation (↑↑b) γ * ↑b ^ m) = ordinalValue ↑b ^ m * ordinalValue (translatedTruncation (↑↑b) γ)) : ordinalValue (↑b ^ (m + 1)) = ordinalValue ↑b ^ (m + 1)

Berarducci, Lemma 8.2 for a pure power, the case c = 1 of the source. The comparison of principal values disappears with the term it controlled, and so does the division by v_J(c).