English
If HasFPowerSeriesWithinOnBall holds for all i, then HasFPowerSeriesWithinOnBall for the pi-product holds.
Русский
Если для каждого i выполняется HasFPowerSeriesWithinOnBall, то для pi-произведения тоже.
LaTeX
$$$\\forall hf: \\forall i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r \\Rightarrow HasFPowerSeriesWithinOnBall (fun x \\mapsto (f · x)) (FormalMultilinearSeries.pi p) s e r$$$
Lean4
/-- If each function in a finite family has a power series within a ball, then so does the
family as a whole. Note that the positivity assumption on the radius is only needed when
the family is empty. -/
theorem pi (hf : ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r) (hr : 0 < r) :
HasFPowerSeriesWithinOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e r
where
r_le := by
apply FormalMultilinearSeries.le_radius_pi (fun i ↦ ?_)
exact (hf i).r_le
r_pos := hr
hasSum {_} m hy := Pi.hasSum.2 (fun i ↦ (hf i).hasSum m hy)
