hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear

English

The uncurry of a continuous linear map into multilinear maps yields a C-polynomial on a product set.

Русский

Неокурри полином непрерывного линейного отображения в многолинейные отображения образует C-полином на произведении наборов.

LaTeX

$$CPolynomialOn 𝕜 (fun p => f p.1 p.2) s$$

Lean4

protected theorem hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear :
    HasFiniteFPowerSeriesOnBall (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) f.toFormalMultilinearSeriesOfMultilinear 0
      (Fintype.card (Option ι) + 1) ⊤ :=
  by
  apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top ?_
  · intro m hm
    apply dif_neg
    exact Nat.ne_of_lt hm
  · intro y _
    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
    · rw [toFormalMultilinearSeriesOfMultilinear, dif_pos rfl]; rfl
    · intro m _ ne; rw [toFormalMultilinearSeriesOfMultilinear, dif_neg ne.symm]; rfl

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