fpowerSeriesBilinear_apply_one — Mathlib

English

In the bilinear power-series expansion, all coefficients of degree n+3 and higher vanish for any n; i.e., the expansion terminates after degree 2.

Русский

В разложении билинейного ряда коэффициенты степени не выше 2 могут быть не нулевые; коэффициенты степени ≥ 3 равны нулю.

LaTeX

$$$ f.fpowerSeriesBilinear x (n+3) = 0$ for all n$$

Lean4

@[simp]
theorem fpowerSeriesBilinear_apply_one (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    fpowerSeriesBilinear f x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x) :=
  rfl

Похожие утверждения