English
Definition of the Hasse derivative on Laurent series as a linear map parameterized by k.
Русский
Определение градиентной Хассе на рядов Лоренца как линейного отображения, зависящего от k.
LaTeX
$$def hasseDeriv (R) {V} [AddCommGroup V] [Module R V] (k : ℕ) : V⸨X⸩ →ₗ[R] V⸨X⸩$$
Lean4
/-- The Hasse derivative of Laurent series, as a linear map. -/
def hasseDeriv (R : Type*) {V : Type*} [AddCommGroup V] [Semiring R] [Module R V] (k : ℕ) : V⸨X⸩ →ₗ[R] V⸨X⸩
where
toFun
f :=
HahnSeries.ofSuppBddBelow (fun (n : ℤ) => (Ring.choose (n + k) k) • f.coeff (n + k))
(forallLTEqZero_supp_BddBelow _ (f.order - k : ℤ)
(fun _ h_lt ↦ by rw [coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h_lt, smul_zero]))
map_add' f
g := by
ext
simp only [ofSuppBddBelow, coeff_add', Pi.add_apply, smul_add]
map_smul' r
f := by
ext
simp only [ofSuppBddBelow, HahnSeries.coeff_smul, RingHom.id_apply, smul_comm r]
