English
The nth coefficient of inv.aux a φ is given by a recursive formula: it equals a if n = 0, and otherwise equals -a times the sum over pairs (x,y) in the antidiagonal of n of coeff x φ times coeff y (inv.aux a φ) provided y < n.
Русский
n-й коэффициент inv.aux a φ удовлетворяет рекурсивной формуле: при n=0 равен a, иначе равен -a сумма по парам (x,y) из антидиагонали n: коэффициент x φ умножить на коэффициент y (inv.aux a φ), если y < n.
LaTeX
$$$ \operatorname{coeff}_n(\operatorname{inv.aux} a \varphi) = \begin{cases} a, & n=0 \\ -a \cdot \sum_{x \in \operatorname{antidiagonal} n} (coeff_{x.1} \varphi) (coeff_{x.2}(\operatorname{inv.aux} a \varphi)), & n>0 \end{cases} $$$
Lean4
theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) :
coeff n (inv.aux a φ) =
if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then coeff x.1 φ * coeff x.2 (inv.aux a φ) else 0 :=
by
rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]
simp only [Finsupp.single_eq_zero]
split_ifs; · rfl
congr 1
symm
apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b)) fun (f, g) ↦ (f (), g ())
· aesop
· aesop
· aesop
· aesop
· rintro ⟨i, j⟩ _hij
obtain H | H := le_or_gt n j
· aesop
rw [if_pos H, if_pos]
· rfl
refine ⟨?_, fun hh ↦ H.not_ge ?_⟩
· rintro ⟨⟩
simpa [Finsupp.single_eq_same] using le_of_lt H
· simpa [Finsupp.single_eq_same] using hh ()
