hasFPowerSeriesOnBall_bilinear — Mathlib

English

The HasFPowerSeriesOnBall instance for the bilinear function x ↦ f x.1 x.2 exists with the radius ∞, reflecting global analyticity in both variables.

Русский

Существование HasFPowerSeriesOnBall для билинейной функции x ↦ f x.1 x.2 с радиусом ∞ отражает глобальную аналитичность по обеим переменным.

LaTeX

$$$ HasFPowerSeriesOnBall (\lambda x : E×F => f x.1 x.2) (f.fpowerSeriesBilinear x) x \infty$$$

Lean4

protected theorem hasFPowerSeriesOnBall_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    HasFPowerSeriesOnBall (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x ∞ :=
  { r_le := by simp
    r_pos := ENNReal.coe_lt_top
    hasSum := fun _ =>
      (hasSum_nat_add_iff' 3).1 <|
        by
        simp only [Finset.sum_range_succ, Prod.fst_add, Prod.snd_add, f.map_add_add]
        simp [fpowerSeriesBilinear, hasSum_zero] }

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