hasFiniteFPowerSeriesOnBall — Mathlib

English

For a bilinear map f: E →L[𝕜] F →L[𝕜] G and m: Fin 2 → E × F, the uncurry operation yields f.uncurryBilinear m = f (m 0).1 (m 1).2.

Русский

Для билинейного отображения f: E →L[𝕜] F →L[𝕜] G и m: Fin 2 → E × F, выполняется f.uncurryBilinear m = f (m 0).1 (m 1).2.

LaTeX

$$$ f.uncurryBilinear(m) = f\bigl(m(0)\!\!\!\_1\bigr)\bigl(m(1)\!\!\!\_2\bigr) $$$

Lean4

protected theorem hasFiniteFPowerSeriesOnBall (f : E →L[𝕜] F) (x : E) :
    HasFiniteFPowerSeriesOnBall f (f.fpowerSeries x) x 2 ∞
    where
  r_le := by simp
  r_pos := ENNReal.coe_lt_top
  hasSum := fun _ => (hasSum_nat_add_iff' 2).1 <| by simp [Finset.sum_range_succ, hasSum_zero, fpowerSeries]
  finite := by
    intro m hm
    match m with
    | 0 | 1 => linarith
    | n + 2 => simp [fpowerSeries]

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