Local derivative estimates for Corvaja--Zannier

The local Wronskian argument is carried out after expanding a rational function in a Laurent series at a point of the curve. This file proves the completion-level estimate that an r-th derivative lowers the Laurent-series order by at most r.

The statements use HahnSeries.orderTop, rather than HahnSeries.order, so that they remain valid when the derivative vanishes.

theorem BGS.CorvajaZannier.order_sub_le_orderTop_hasseDeriv {K : Type u_1} [Ring K] (r : ℕ) (f : LaurentSeries K) : ↑(HahnSeries.order f - ↑r) ≤ HahnSeries.orderTop ((LaurentSeries.hasseDeriv K r) f)

The r-th Hasse derivative lowers Laurent-series order by at most r.

The orderTop formulation also covers the case in which the Hasse derivative is zero.

theorem BGS.CorvajaZannier.order_sub_le_orderTop_derivative_iterate {K : Type u_1} [Ring K] (r : ℕ) (f : LaurentSeries K) : ↑(HahnSeries.order f - ↑r) ≤ HahnSeries.orderTop ((⇑(LaurentSeries.derivative K))^[r] f)

Every ordinary iterated derivative lowers Laurent-series order by at most its iteration count.

The orderTop formulation also covers the case in which the iterated derivative is zero.