English
For every PowerSeries f, the zero-th coefficient of heval x f equals the zero-th (constant) coefficient of f.
Русский
Для любого степенного ряда f нулевой коэффициент у heval x f равен нулевому коэффициенту (постоянному члену) ряда f.
LaTeX
$$$ (\\text{heval } x\, f).\\mathrm{coeff}\; 0 = \\text{PowerSeries}.\\mathrm{constantCoeff}\\; f $$$
Lean4
theorem coeff_heval_zero (f : PowerSeries R) : (heval x f).coeff 0 = PowerSeries.constantCoeff f :=
by
rw [coeff_heval, finsum_eq_single (fun n => ((powerSeriesFamily x f).coeff 0) n) 0, ←
PowerSeries.coeff_zero_eq_constantCoeff_apply]
· simp
· intro n hn
simp only [coeff_toFun, smulFamily_toFun, HahnSeries.coeff_smul, smul_eq_mul]
refine mul_eq_zero_of_right (coeff n f) (coeff_eq_zero_of_lt_orderTop ?_)
by_cases h : 0 < x.orderTop
· refine (lt_of_lt_of_le ((nsmul_pos_iff hn).mpr h) ?_)
simp [h, orderTop_nsmul_le_orderTop_pow]
· simp [h, hn]
