English
If Valued.v f ≤ exp(-D) for D ∈ℤ, then for any natural n with n < D, the coefficient coeff n f is zero; a detailed case split addresses negative and nonnegative order cases.
Русский
Если Valued.v f ≤ exp(-D) для D ∈ ℤ, то для любого натурального n с n < D коэффициент coeff n f равен 0; приводится разбиение по случаям порядка f.
LaTeX
$$$\forall D\in\mathbb{Z},\; (\mathrm{Valued}.v f \le e^{-D}) \Rightarrow (\forall n< D,\; \mathrm{coeff}_n f = 0)$$$
Lean4
theorem coeff_zero_of_lt_valuation {n D : ℤ} {f : K⸨X⸩} (H : Valued.v f ≤ exp (-D)) : n < D → f.coeff n = 0 :=
by
intro hnd
by_cases h_n_ord : n < f.order
· exact coeff_eq_zero_of_lt_order h_n_ord
rw [not_lt] at h_n_ord
set F := powerSeriesPart f with hF
by_cases ord_nonpos : f.order ≤ 0
· obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (neg_le_iff_add_nonneg.mp (hs ▸ h_n_ord))
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D + s) (by cutsat)
rw [eq_add_neg_of_add_eq hm, add_comm, ← hs, ← powerSeriesPart_coeff]
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
rw [hF, ofPowerSeries_powerSeriesPart f, hs, neg_neg, ← hd, neg_add_rev, exp_add, map_mul, ← ofPowerSeries_X_pow s,
PowerSeries.coe_pow, valuation_X_pow K s]
gcongr
· rw [not_le] at ord_nonpos
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (le_of_lt ord_nonpos))
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (a := n - s) (by omega)
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D - s) (by cutsat)
rw [(sub_eq_iff_eq_add).mp hm, add_comm, ← neg_neg (s : ℤ), ← hs, neg_neg, ← powerSeriesPart_coeff]
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
rw [hF, ofPowerSeries_powerSeriesPart f, map_mul, ← hd, hs, neg_sub, sub_eq_add_neg, exp_add, valuation_single_zpow,
neg_neg]
gcongr
/- The valuation of a Laurent series is the order of the first non-zero coefficient. -/
