Theorems · Theorem · complex analysis

HasFPowerSeriesOnBall.exchange_radius

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {r₁ r₂ : ENNReal} {x : 𝕜},
  HasFPowerSeriesOnBall f p₁ x r₁ → HasFPowerSeriesOnBall f p₂ x r₂ → HasFPowerSeriesOnBall f p₁ x r₂

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.

Defined in

Mathlib.Analysis.Analytic.Uniqueness

Cited by

2 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace