English
If f has a power series on a ball of radius r and for every r'>0 there exists a series on r', then the radius is top (infinite).
Русский
Если у функции f есть представление степенного ряда на шаре радиуса r и для каждого r' > 0 существует представление на r', то радиус равен бесконечности.
LaTeX
$$$\\text{HasFPowerSeriesOnBall}\\, f\\, p\\, x\\, r \\rightarrow (\\forall r' > 0, \\exists p': \\text{HasFPowerSeriesOnBall } f\\, p'\\, x\\, r') \\Rightarrow \\text{HasFPowerSeriesOnBall } f\\, p\\, x\\, \\infty.$$$
Lean4
/-- If a function `f : 𝕜 → E` has two power series representations at `x`, then the given radii in
which convergence is guaranteed may be interchanged. This can be useful when the formal multilinear
series in one representation has a particularly nice form, but the other has a larger radius. -/
theorem exchange_radius {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {r₁ r₂ : ℝ≥0∞} {x : 𝕜}
(h₁ : HasFPowerSeriesOnBall f p₁ x r₁) (h₂ : HasFPowerSeriesOnBall f p₂ x r₂) : HasFPowerSeriesOnBall f p₁ x r₂ :=
h₂.hasFPowerSeriesAt.eq_formalMultilinearSeries h₁.hasFPowerSeriesAt ▸ h₂
