English
If f and g have HasFPowerSeriesWithinOnBall expansions on balls with radii r and s, then the pair (f, g) has an expansion on the ball with radius min(r, s).
Русский
Если у f и g есть разложения в шаре радиусов r и s, то пара (f,g) имеет разложение на шаре с радиусом min(r,s).
LaTeX
$$$\text{HasFPowerSeriesWithinOnBall}(f, pf, s, x, r) \land \text{HasFPowerSeriesWithinOnBall}(g, qf, s, x, r) \Rightarrow \text{HasFPowerSeriesWithinOnBall}(x \mapsto (f(x), g(x)), pf \cdot qf, s, x, \min(r, r))$$$
Lean4
theorem prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {t : Set E} {p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinOnBall f p t e r)
(hg : HasFPowerSeriesWithinOnBall g q t e s) :
HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) t e (min r s)
where
r_le := by
rw [p.radius_prod_eq_min]
exact min_le_min hf.r_le hg.r_le
r_pos := lt_min hf.r_pos hg.r_pos
hasSum := by
intro y h'y hy
simp_rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.prod_apply]
refine (hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)
· exact EMetric.mem_ball.mpr (lt_of_lt_of_le hy (min_le_left _ _))
· exact EMetric.mem_ball.mpr (lt_of_lt_of_le hy (min_le_right _ _))
