Mathlib.Analysis.Analytic.ChangeOrigin

Module docstring

{"# Changing origin in a power series

If a function is analytic in a disk D(x, R), then it is analytic in any disk contained in that one. Indeed, one can write $$ f (x + y + z) = \sum{n} pn (y + z)^n = \sum{n, k} \binom{n}{k} pn y^{n-k} z^k = \sum{k} \Bigl(\sum{n} \binom{n}{k} pn y^{n-k}\Bigr) z^k. $$ The corresponding power series has thus a k-th coefficient equal to $\sum{n} \binom{n}{k} p_n y^{n-k}$. In the general case where pₙ is a multilinear map, this has to be interpreted suitably: instead of having a binomial coefficient, one should sum over all possible subsets s of Fin n of cardinality k, and attribute z to the indices in s and y to the indices outside of s.

In this file, we implement this. The new power series is called p.changeOrigin y. Then, we check its convergence and the fact that its sum coincides with the original sum. The outcome of this discussion is that the set of points where a function is analytic is open. All these arguments require the target space to be complete, as otherwise the series might not converge.

Main results

In a complete space, if a function admits a power series in a ball, then it is analytic at any point y of this ball, and the power series there can be expressed in terms of the initial power series p as p.changeOrigin y. See HasFPowerSeriesOnBall.changeOrigin. It follows in particular that the set of points at which a given function is analytic is open, see isOpen_analyticAt. "}

FormalMultilinearSeries.changeOriginSeriesTerm definition

(k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : E [×l]→L[𝕜] E [×k]→L[𝕜] F

Full source

/-- A term of `FormalMultilinearSeries.changeOriginSeries`.

Given a formal multilinear series `p` and a point `x` in its ball of convergence,
`p.changeOrigin x` is a formal multilinear series such that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Each term of `p.changeOrigin x`
is itself an analytic function of `x` given by the series `p.changeOriginSeries`. Each term in
`changeOriginSeries` is the sum of `changeOriginSeriesTerm`'s over all `s` of cardinality `l`.
The definition is such that `p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) =
p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))`
-/
def changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    E[×l]→L[𝕜] E[×k]→L[𝕜] F :=
  let a := ContinuousMultilinearMap.curryFinFinset 𝕜 E F hs
    (by rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right])
  a (p (k + l))

Change of origin term in a formal multilinear series

Informal description

For a formal multilinear series `p` and given natural numbers `k`, `l`, a finite subset `s` of `Fin (k + l)` with cardinality `l`, the term `p.changeOriginSeriesTerm k l s hs` is a multilinear map from `E^l` to the space of multilinear maps from `E^k` to `F`. This term is constructed by currying the `(k + l)`-th term of `p` with respect to the partition given by `s` and its complement. More precisely, when applied to constant functions `x` and `y`, it satisfies: $$ p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs\ (\lambda \_, x)\ (\lambda \_, y) = p (k + l) (s.\text{piecewise} (\lambda \_, x) (\lambda \_, y)) $$ where `s.piecewise` assigns `x` to indices in `s` and `y` to others.

FormalMultilinearSeries.changeOriginSeriesTerm_apply theorem

 (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E) :
  (p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y) = p (k + l) (s.piecewise (fun _ => x) fun _ => y)

Full source

theorem changeOriginSeriesTerm_apply (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l)
    (x y : E) :
    (p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y) =
      p (k + l) (s.piecewise (fun _ => x) fun _ => y) :=
  ContinuousMultilinearMap.curryFinFinset_apply_const _ _ _ _ _

Evaluation of Change of Origin Term in Formal Multilinear Series

Informal description

For any natural numbers $k$ and $l$, any finite subset $s$ of $\text{Fin}(k + l)$ with cardinality $l$, and vectors $x, y \in E$, the application of the change of origin term $p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs$ to the constant functions $\lambda \_.\, x$ and $\lambda \_.\, y$ equals the $(k + l)$-th term of the formal multilinear series $p$ evaluated at the piecewise constant function $s.\text{piecewise}\, (\lambda \_.\, x)\, (\lambda \_.\, y)$. In symbols: $$ p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs\ (\lambda \_.\, x)\ (\lambda \_.\, y) = p (k + l) (s.\text{piecewise}\, (\lambda \_.\, x)\, (\lambda \_.\, y)) $$

FormalMultilinearSeries.norm_changeOriginSeriesTerm theorem

(k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖

Full source

@[simp]
theorem norm_changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖ := by
  simp only [changeOriginSeriesTerm, LinearIsometryEquiv.norm_map]

Norm Equality for Change of Origin Term in Formal Multilinear Series

Informal description

For a formal multilinear series $p$, natural numbers $k$ and $l$, a finite subset $s$ of $\text{Fin}(k + l)$ with cardinality $l$, the operator norm of the change of origin term $\|p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs\|$ is equal to the operator norm of the $(k + l)$-th term of $p$, i.e., $$\|p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs\| = \|p (k + l)\|.$$

FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm theorem

 (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊

Full source

@[simp]
theorem nnnorm_changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊ := by
  simp only [changeOriginSeriesTerm, LinearIsometryEquiv.nnnorm_map]

Equality of Non-Negative Norms for Change of Origin Term in Formal Multilinear Series

Informal description

For any natural numbers $k$ and $l$, and any finite subset $s$ of $\text{Fin}(k + l)$ with cardinality $l$, the non-negative norm of the change of origin term $p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs$ is equal to the non-negative norm of the $(k + l)$-th term of the formal multilinear series $p$, i.e., $\|p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs\|_{\mathbb{N}} = \|p (k + l)\|_{\mathbb{N}}$.

FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le theorem

 (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E) :
  ‖p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

Full source

theorem nnnorm_changeOriginSeriesTerm_apply_le (k l : ℕ) (s : Finset (Fin (k + l)))
    (hs : s.card = l) (x y : E) :
    ‖p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y‖₊ ≤
      ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k := by
  rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]
  apply ContinuousMultilinearMap.le_of_opNNNorm_le
  apply ContinuousMultilinearMap.le_opNNNorm

Norm Bound for Change of Origin Term Evaluation: $\|p_{k+l,s}(x^l, y^k)\| \leq \|p_{k+l}\| \cdot \|x\|^l \cdot \|y\|^k$

Informal description

For any natural numbers $k$ and $l$, any finite subset $s$ of $\text{Fin}(k + l)$ with cardinality $l$, and any vectors $x, y \in E$, the non-negative norm of the evaluation of the change of origin term satisfies: \[ \|p.\text{changeOriginSeriesTerm}\ k\ l\ s\ hs\ (\lambda \_, x)\ (\lambda \_, y)\|_{\mathbb{R}_{\geq 0}} \leq \|p (k + l)\|_{\mathbb{R}_{\geq 0}} \cdot \|x\|_{\mathbb{R}_{\geq 0}}^l \cdot \|y\|_{\mathbb{R}_{\geq 0}}^k. \]

FormalMultilinearSeries.changeOriginSeries definition

(k : ℕ) : FormalMultilinearSeries 𝕜 E (E [×k]→L[𝕜] F)

Full source

/-- The power series for `f.changeOrigin k`.

Given a formal multilinear series `p` and a point `x` in its ball of convergence,
`p.changeOrigin x` is a formal multilinear series such that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Its `k`-th term is the sum of
the series `p.changeOriginSeries k`. -/
def changeOriginSeries (k : ℕ) : FormalMultilinearSeries 𝕜 E (E[×k]→L[𝕜] F) := fun l =>
  ∑ s : { s : Finset (Fin (k + l)) // Finset.card s = l }, p.changeOriginSeriesTerm k l s s.2

Change of origin series in a formal multilinear series

Informal description

For a formal multilinear series `p` and a natural number `k`, the series `p.changeOriginSeries k` is a formal multilinear series where the `l`-th term is the sum over all subsets `s` of `Fin (k + l)` with cardinality `l` of the terms `p.changeOriginSeriesTerm k l s hs`. This series represents the change of origin in the power series expansion. More precisely, when applied to constant functions `x` and `y`, the `l`-th term satisfies: $$ p.\text{changeOriginSeries}\ k\ l\ (\lambda \_, x)\ (\lambda \_, y) = \sum_{\substack{s \subset \text{Fin}(k + l) \\ |s| = l}} p (k + l) (s.\text{piecewise} (\lambda \_, x) (\lambda \_, y)) $$ where the sum is over all subsets `s` of `Fin (k + l)` with exactly `l` elements, and `s.piecewise` assigns `x` to indices in `s` and `y` to others.

FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum theorem

 (k l : ℕ) : ‖p.changeOriginSeries k l‖₊ ≤ ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊

Full source

theorem nnnorm_changeOriginSeries_le_tsum (k l : ℕ) :
    ‖p.changeOriginSeries k l‖₊ ≤
      ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ :=
  (nnnorm_sum_le _ (fun t => changeOriginSeriesTerm p k l (Subtype.val t) t.prop)).trans_eq <| by
    simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]

Norm Bound for Change of Origin Series in Formal Multilinear Series

Informal description

For any natural numbers $k$ and $l$, the non-negative norm of the $l$-th term of the change of origin series $\|p.\text{changeOriginSeries}\ k\ l\|_{\mathbb{N}}$ is bounded above by the sum over all subsets $s$ of $\text{Fin}(k + l)$ with cardinality $l$ of the non-negative norms $\|p (k + l)\|_{\mathbb{N}}$, i.e., $$\|p.\text{changeOriginSeries}\ k\ l\|_{\mathbb{N}} \leq \sum'_{\substack{s \subset \text{Fin}(k + l) \\ |s| = l}} \|p (k + l)\|_{\mathbb{N}}.$$

FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum theorem

 (k l : ℕ) (x : E) :
  ‖p.changeOriginSeries k l fun _ => x‖₊ ≤ ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ * ‖x‖₊ ^ l

Full source

theorem nnnorm_changeOriginSeries_apply_le_tsum (k l : ℕ) (x : E) :
    ‖p.changeOriginSeries k l fun _ => x‖₊ ≤
      ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ * ‖x‖₊ ^ l := by
  rw [NNReal.tsum_mul_right, ← Fin.prod_const]
  exact (p.changeOriginSeries k l).le_of_opNNNorm_le (p.nnnorm_changeOriginSeries_le_tsum _ _) _

Norm Bound for Change of Origin Series Applied to Constant Function

Informal description

For any natural numbers $k$ and $l$, and any vector $x \in E$, the non-negative norm of the $l$-th term of the change of origin series applied to the constant function $\lambda \_, x$ is bounded above by the sum over all subsets $s$ of $\mathrm{Fin}(k + l)$ with cardinality $l$ of the product $\|p (k + l)\|_{\mathbb{N}} \cdot \|x\|_{\mathbb{N}}^l$, i.e., $$\|p.\text{changeOriginSeries}\ k\ l\ (\lambda \_, x)\|_{\mathbb{N}} \leq \sum'_{\substack{s \subset \mathrm{Fin}(k + l) \\ |s| = l}} \|p (k + l)\|_{\mathbb{N}} \cdot \|x\|_{\mathbb{N}}^l.$$

FormalMultilinearSeries.changeOrigin definition

(x : E) : FormalMultilinearSeries 𝕜 E F

Full source

/-- Changing the origin of a formal multilinear series `p`, so that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense.
-/
def changeOrigin (x : E) : FormalMultilinearSeries 𝕜 E F :=
  fun k => (p.changeOriginSeries k).sum x

Change of origin in a formal multilinear series

Informal description

Given a formal multilinear series `p` and a point `x` in the space `E`, the series `p.changeOrigin x` is a new formal multilinear series such that the sum of `p` evaluated at `x + y` is equal to the sum of `p.changeOrigin x` evaluated at `y`, whenever this makes sense. More precisely, for any `y` in a sufficiently small neighborhood, we have: $$ \sum_{n} p_n (x + y)^{\otimes n} = \sum_{k} \left( \sum_{l} p_{k+l} \binom{k+l}{k} x^{\otimes k} y^{\otimes l} \right) $$ where the inner sum is interpreted as summing over all possible ways to distribute the variables between `x` and `y` in the multilinear map.

FormalMultilinearSeries.changeOriginIndexEquiv definition

: (Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) ≃ Σ n : ℕ, Finset (Fin n)

Full source

/-- An auxiliary equivalence useful in the proofs about
`FormalMultilinearSeries.changeOriginSeries`: the set of triples `(k, l, s)`, where `s` is a
`Finset (Fin (k + l))` of cardinality `l` is equivalent to the set of pairs `(n, s)`, where `s` is a
`Finset (Fin n)`.

The forward map sends `(k, l, s)` to `(k + l, s)` and the inverse map sends `(n, s)` to
`(n - Finset.card s, Finset.card s, s)`. The actual definition is less readable because of problems
with non-definitional equalities. -/
@[simps]
def changeOriginIndexEquiv :
    (Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) ≃ Σ n : ℕ, Finset (Fin n) where
  toFun s := ⟨s.1 + s.2.1, s.2.2⟩
  invFun s :=
    ⟨s.1 - s.2.card, s.2.card,
      ⟨s.2.map
        (finCongr <| (tsub_add_cancel_of_le <| card_finset_fin_le s.2).symm).toEmbedding,
        Finset.card_map _⟩⟩
  left_inv := by
    rintro ⟨k, l, ⟨s : Finset (Fin <| k + l), hs : s.card = l⟩⟩
    dsimp only [Subtype.coe_mk]
    -- Lean can't automatically generalize `k' = k + l - s.card`, `l' = s.card`, so we explicitly
    -- formulate the generalized goal
    suffices ∀ k' l', k' = k → l' = l → ∀ (hkl : k + l = k' + l') (hs'),
        (⟨k', l', ⟨s.map (finCongr hkl).toEmbedding, hs'⟩⟩ :
          Σk l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) = ⟨k, l, ⟨s, hs⟩⟩ by
      apply this <;> simp only [hs, add_tsub_cancel_right]
    simp
  right_inv := by
    rintro ⟨n, s⟩
    simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast]

Equivalence between index sets for change of origin in power series

Informal description

The equivalence `changeOriginIndexEquiv` establishes a bijection between two types of index sets: 1. Triples $(k, l, s)$ where $s$ is a finite subset of $\mathrm{Fin}(k + l)$ with cardinality $l$. 2. Pairs $(n, s)$ where $s$ is a finite subset of $\mathrm{Fin}(n)$. The forward map sends $(k, l, s)$ to $(k + l, s)$, while the inverse map sends $(n, s)$ to $(n - |s|, |s|, s')$ where $s'$ is a suitable embedding of $s$ into $\mathrm{Fin}(n - |s| + |s|) = \mathrm{Fin}(n)$. This equivalence is used in the construction of the power series after changing the origin.

FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm theorem

 (n t) :
  let s := changeOriginIndexEquiv.symm ⟨n, t⟩
  p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) (fun _ ↦ y) = p n (t.piecewise (fun _ ↦ x) fun _ ↦ y)

Full source

lemma changeOriginSeriesTerm_changeOriginIndexEquiv_symm (n t) :
    let s := changeOriginIndexEquiv.symm ⟨n, t⟩
    p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) (fun _ ↦ y) =
    p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) := by
  have : ∀ (m) (hm : n = m), p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) =
      p m ((t.map (finCongr hm).toEmbedding).piecewise (fun _ ↦ x) fun _ ↦ y) := by
    rintro m rfl
    simp +unfoldPartialApp [Finset.piecewise]
  simp_rw [changeOriginSeriesTerm_apply, eq_comm]; apply this

Evaluation of Change-of-Origin Term via Index Equivalence

Informal description

Let $p$ be a formal multilinear series, $x, y \in E$, $n \in \mathbb{N}$, and $t$ be a finite subset of $\mathrm{Fin}(n)$. Let $s = \mathrm{changeOriginIndexEquiv}^{-1}(n, t)$. Then the change of origin term satisfies: $$ p.\mathrm{changeOriginSeriesTerm}\, s.1\, s.2.1\, s.2.2\, s.2.2.2\, (\lambda \_.\, x)\, (\lambda \_.\, y) = p n (t.\mathrm{piecewise}\, (\lambda \_.\, x)\, (\lambda \_.\, y)) $$ where $s.1$, $s.2.1$, etc. are the components of the triple $s = (k, l, s')$ obtained from the inverse equivalence.

FormalMultilinearSeries.changeOriginSeries_summable_aux₁ theorem

 {r r' : ℝ≥0} (hr : (r + r' : ℝ≥0∞) < p.radius) :
  Summable fun s : Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l } => ‖p (s.1 + s.2.1)‖₊ * r ^ s.2.1 * r' ^ s.1

Full source

theorem changeOriginSeries_summable_aux₁ {r r' : ℝ≥0} (hr : (r + r' : ℝ≥0∞) < p.radius) :
    Summable fun s : Σk l : ℕ, { s : Finset (Fin (k + l)) // s.card = l } =>
      ‖p (s.1 + s.2.1)‖₊ * r ^ s.2.1 * r' ^ s.1 := by
  rw [← changeOriginIndexEquiv.symm.summable_iff]
  dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst,
    changeOriginIndexEquiv_symm_apply_snd_fst]
  have : ∀ n : ℕ,
      HasSum (fun s : Finset (Fin n) => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card))
        (‖p n‖₊ * (r + r') ^ n) := by
    intro n
    -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails?
    convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
    · ext1 s
      rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
    rw [← Fin.sum_pow_mul_eq_add_pow]
    exact (hasSum_fintype _).mul_left _
  refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩
  simp only [(this _).tsum_eq]
  exact p.summable_nnnorm_mul_pow hr

Summability of Change-of-Origin Series Coefficients

Informal description

Let $p$ be a formal multilinear series with radius of convergence $R$, and let $r, r' \in \mathbb{R}_{\geq 0}$ be such that $r + r' < R$ in the extended non-negative reals. Then the series \[ \sum_{(k, l, s) \in \Sigma} \|p(k + l)\| \cdot r^l \cdot r'^k \] is summable, where $\Sigma$ is the set of triples $(k, l, s)$ with $s$ a finite subset of $\mathrm{Fin}(k + l)$ of cardinality $l$.

FormalMultilinearSeries.changeOriginSeries_summable_aux₂ theorem

 (hr : (r : ℝ≥0∞) < p.radius) (k : ℕ) :
  Summable fun s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l } => ‖p (k + s.1)‖₊ * r ^ s.1

Full source

theorem changeOriginSeries_summable_aux₂ (hr : (r : ℝ≥0∞) < p.radius) (k : ℕ) :
    Summable fun s : Σl : ℕ, { s : Finset (Fin (k + l)) // s.card = l } =>
      ‖p (k + s.1)‖₊ * r ^ s.1 := by
  rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩
  simpa only [mul_inv_cancel_right₀ (pow_pos h0 _).ne'] using
    ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹

Summability of Change-of-Origin Series Coefficients for Fixed Degree $k$

Informal description

Let $p$ be a formal multilinear series with radius of convergence $R$, and let $r \in \mathbb{R}_{\geq 0}$ be such that $r < R$ in the extended non-negative reals. For any natural number $k$, the series \[ \sum_{(l, s) \in \Sigma} \|p(k + l)\| \cdot r^l \] is summable, where $\Sigma$ is the set of pairs $(l, s)$ with $s$ a finite subset of $\mathrm{Fin}(k + l)$ of cardinality $l$.

FormalMultilinearSeries.changeOriginSeries_summable_aux₃ theorem

{r : ℝ≥0} (hr : ↑r < p.radius) (k : ℕ) : Summable fun l : ℕ => ‖p.changeOriginSeries k l‖₊ * r ^ l

Full source

theorem changeOriginSeries_summable_aux₃ {r : ℝ≥0} (hr : ↑r < p.radius) (k : ℕ) :
    Summable fun l : ℕ => ‖p.changeOriginSeries k l‖₊ * r ^ l := by
  refine NNReal.summable_of_le
    (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2
  simp only [NNReal.tsum_mul_right]
  exact mul_le_mul' (p.nnnorm_changeOriginSeries_le_tsum _ _) le_rfl

Summability of Change-of-Origin Series for Fixed Degree $k$ with Radius $r < R$

Informal description

Let $p$ be a formal multilinear series with radius of convergence $R$, and let $r \in \mathbb{R}_{\geq 0}$ be such that $r < R$. For any natural number $k$, the series \[ \sum_{l=0}^\infty \|p.\text{changeOriginSeries}\ k\ l\| \cdot r^l \] is summable.

FormalMultilinearSeries.le_changeOriginSeries_radius theorem

(k : ℕ) : p.radius ≤ (p.changeOriginSeries k).radius

Full source

theorem le_changeOriginSeries_radius (k : ℕ) : p.radius ≤ (p.changeOriginSeries k).radius :=
  ENNReal.le_of_forall_nnreal_lt fun _r hr =>
    le_radius_of_summable_nnnorm _ (p.changeOriginSeries_summable_aux₃ hr k)

Radius Comparison for Change-of-Origin Series: $R \leq R_{\text{changeOriginSeries}}$

Informal description

For any formal multilinear series $p$ and any natural number $k$, the radius of convergence of $p$ is less than or equal to the radius of convergence of the change-of-origin series $p.\text{changeOriginSeries}\ k$.

FormalMultilinearSeries.nnnorm_changeOrigin_le theorem

 (k : ℕ) (h : (‖x‖₊ : ℝ≥0∞) < p.radius) :
  ‖p.changeOrigin x k‖₊ ≤ ∑' s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1

Full source

theorem nnnorm_changeOrigin_le (k : ℕ) (h : (‖x‖₊ : ℝ≥0∞) < p.radius) :
    ‖p.changeOrigin x k‖₊ ≤
      ∑' s : Σl : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1 := by
  refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x
  have := p.changeOriginSeries_summable_aux₂ h k
  refine HasSum.sigma this.hasSum fun l => ?_
  exact ((NNReal.summable_sigma.1 this).1 l).hasSum

Norm Bound for Changed-Origin Series Coefficients

Informal description

For any natural number $k$ and any vector $x$ in a normed space $E$ with $\|x\| < R$ (where $R$ is the radius of convergence of the formal multilinear series $p$), the norm of the $k$-th coefficient of the changed-origin series $p.\text{changeOrigin}(x)$ is bounded by the sum over all pairs $(l, s)$ where $s$ is a subset of $\text{Fin}(k + l)$ with cardinality $l$ of the product $\|p(k + l)\| \cdot \|x\|^l$. In other words: $$\|p.\text{changeOrigin}(x)_k\| \leq \sum_{l=0}^\infty \sum_{\substack{s \subset \text{Fin}(k + l) \\ |s| = l}} \|p(k + l)\| \cdot \|x\|^l.$$

FormalMultilinearSeries.changeOrigin_radius theorem

: p.radius - ‖x‖₊ ≤ (p.changeOrigin x).radius

Full source

/-- The radius of convergence of `p.changeOrigin x` is at least `p.radius - ‖x‖`. In other words,
`p.changeOrigin x` is well defined on the largest ball contained in the original ball of
convergence. -/
theorem changeOrigin_radius : p.radius - ‖x‖₊ ≤ (p.changeOrigin x).radius := by
  refine ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_
  rw [lt_tsub_iff_right, add_comm] at hr
  have hr' : (‖x‖₊ : ℝ≥0∞) < p.radius := (le_add_right le_rfl).trans_lt hr
  apply le_radius_of_summable_nnnorm
  have : ∀ k : ℕ,
      ‖p.changeOrigin x k‖₊ * r ^ k ≤
        (∑' s : Σl : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1) *
          r ^ k :=
    fun k => mul_le_mul_right' (p.nnnorm_changeOrigin_le k hr') (r ^ k)
  refine NNReal.summable_of_le this ?_
  simpa only [← NNReal.tsum_mul_right] using
    (NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr)).2

Lower Bound on Radius of Convergence for Changed-Origin Series: $R - \|x\| \leq R_{\text{changeOrigin}(x)}$

Informal description

For any formal multilinear series $p$ with radius of convergence $R$ and any vector $x$ in a normed space $E$, the radius of convergence of the changed-origin series $p.\text{changeOrigin}(x)$ is at least $R - \|x\|$. In other words, the power series $p.\text{changeOrigin}(x)$ is well-defined on any ball of radius $r < R - \|x\|$ centered at the origin.

FormalMultilinearSeries.derivSeries definition

: FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)

Full source

/-- `derivSeries p` is a power series for `fderiv 𝕜 f` if `p` is a power series for `f`,
see `HasFPowerSeriesOnBall.fderiv`. -/
def derivSeries : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) :=
  (continuousMultilinearCurryFin1 𝕜 E F : (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F)
    |>.compFormalMultilinearSeries (p.changeOriginSeries 1)

Power series for the Fréchet derivative

Informal description

The power series `derivSeries p` is constructed from the formal multilinear series `p` by first applying the change of origin series with `k = 1` (i.e., `p.changeOriginSeries 1`), and then composing with the continuous multilinear curry operation that converts 1-linear maps from `E` to `F` into continuous linear maps from `E` to `F`. More precisely, if `p` represents a power series expansion of a function `f` around a point, then `derivSeries p` represents the power series expansion of the Fréchet derivative of `f` at that point.

FormalMultilinearSeries.radius_le_radius_derivSeries theorem

: p.radius ≤ p.derivSeries.radius

Full source

theorem radius_le_radius_derivSeries : p.radius ≤ p.derivSeries.radius := by
  apply (p.le_changeOriginSeries_radius 1).trans (radius_le_of_le (fun n ↦ ?_))
  apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
  apply mul_le_of_le_one_left (norm_nonneg  _)
  exact ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)

Radius Comparison: $R_p \leq R_{\text{derivSeries}\, p}$

Informal description

For any formal multilinear series $p$, the radius of convergence of $p$ is less than or equal to the radius of convergence of its derivative series $\text{derivSeries}\, p$.

FormalMultilinearSeries.derivSeries_eq_zero theorem

{n : ℕ} (hp : p (n + 1) = 0) : p.derivSeries n = 0

Full source

theorem derivSeries_eq_zero {n : ℕ} (hp : p (n + 1) = 0) : p.derivSeries n = 0 := by
  suffices p.changeOriginSeries 1 n = 0 by ext v; simp [derivSeries, this]
  apply Finset.sum_eq_zero (fun s hs ↦ ?_)
  ext v
  have : p (1 + n) = 0 := p.congr_zero (by abel) hp
  simp [changeOriginSeriesTerm, ContinuousMultilinearMap.curryFinFinset_apply,
    ContinuousMultilinearMap.zero_apply, this]

Vanishing of Derivative Series Term when Higher Term Vanishes: $p_{n+1} = 0 \Rightarrow (\text{derivSeries}\, p)_n = 0$

Informal description

For any natural number $n$, if the $(n+1)$-th term $p_{n+1}$ of the formal multilinear series $p$ is zero, then the $n$-th term of the derivative series $\text{derivSeries}\, p$ is also zero.

FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin theorem

(k : ℕ) (hr : 0 < p.radius) : HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius

Full source

theorem hasFPowerSeriesOnBall_changeOrigin (k : ℕ) (hr : 0 < p.radius) :
    HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius :=
  have := p.le_changeOriginSeries_radius k
  ((p.changeOriginSeries k).hasFPowerSeriesOnBall (hr.trans_le this)).mono hr this

Power Series Expansion of Change-of-Origin Function: $x \mapsto p.\text{changeOrigin}\, x\, k$

Informal description

For any natural number $k$ and any formal multilinear series $p$ with positive radius of convergence $R > 0$, the function $x \mapsto p.\text{changeOrigin}\, x\, k$ has a power series expansion given by $p.\text{changeOriginSeries}\, k$ on the ball of radius $R$ centered at $0$. More precisely, for all $x$ with $\|x\| < R$, we have: $$ p.\text{changeOrigin}\, x\, k = \sum_{l=0}^\infty (p.\text{changeOriginSeries}\, k)_l (x^{\otimes l}) $$ where the series converges absolutely and uniformly on compact subsets of the ball.

FormalMultilinearSeries.changeOrigin_eval theorem

(h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius) : (p.changeOrigin x).sum y = p.sum (x + y)

Full source

/-- Summing the series `p.changeOrigin x` at a point `y` gives back `p (x + y)`. -/
theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius) :
    (p.changeOrigin x).sum y = p.sum (x + y) := by
  have radius_pos : 0 < p.radius := lt_of_le_of_lt (zero_le _) h
  have x_mem_ball : x ∈ EMetric.ball (0 : E) p.radius :=
    mem_emetric_ball_zero_iff.2 ((le_add_right le_rfl).trans_lt h)
  have y_mem_ball : y ∈ EMetric.ball (0 : E) (p.changeOrigin x).radius := by
    refine mem_emetric_ball_zero_iff.2 (lt_of_lt_of_le ?_ p.changeOrigin_radius)
    rwa [lt_tsub_iff_right, add_comm]
  have x_add_y_mem_ball : x + y ∈ EMetric.ball (0 : E) p.radius := by
    refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ h)
    exact mod_cast nnnorm_add_le x y
  set f : (Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) → F := fun s =>
    p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) fun _ => y
  have hsf : Summable f := by
    refine .of_nnnorm_bounded _ (p.changeOriginSeries_summable_aux₁ h) ?_
    rintro ⟨k, l, s, hs⟩
    dsimp only [Subtype.coe_mk]
    exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _
  have hf : HasSum f ((p.changeOrigin x).sum y) := by
    refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf
    · dsimp only [f]
      refine ContinuousMultilinearMap.hasSum_eval ?_ _
      have := (p.hasFPowerSeriesOnBall_changeOrigin k radius_pos).hasSum x_mem_ball
      rw [zero_add] at this
      refine HasSum.sigma_of_hasSum this (fun l => ?_) ?_
      · simp only [changeOriginSeries, ContinuousMultilinearMap.sum_apply]
        apply hasSum_fintype
      · refine .of_nnnorm_bounded _
          (p.changeOriginSeries_summable_aux₂ (mem_emetric_ball_zero_iff.1 x_mem_ball) k)
            fun s => ?_
        refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_
        simp
  refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_)
  refine HasSum.sigma_of_hasSum
    (p.hasSum x_add_y_mem_ball) (fun n => ?_) (changeOriginIndexEquiv.symm.summable_iff.2 hsf)
  rw [← Pi.add_def, (p n).map_add_univ (fun _ => x) fun _ => y]
  simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm]
  exact hasSum_fintype (fun c => f (changeOriginIndexEquiv.symm ⟨n, c⟩))

Sum of Changed-Origin Series Equals Original Series at Translated Point: $\sum (p.\text{changeOrigin}\, x)_k y^k = p(x + y)$

Informal description

Let $p$ be a formal multilinear series with radius of convergence $R$, and let $x, y$ be vectors in the underlying normed space such that $\|x\| + \|y\| < R$ (measured in the extended non-negative reals). Then the sum of the changed-origin series $p.\text{changeOrigin}(x)$ evaluated at $y$ equals the sum of the original series $p$ evaluated at $x + y$, i.e., \[ \sum_{k=0}^\infty (p.\text{changeOrigin}\, x)_k (y^{\otimes k}) = \sum_{n=0}^\infty p_n ((x + y)^{\otimes n}). \]

FormalMultilinearSeries.analyticAt_changeOrigin theorem

(p : FormalMultilinearSeries 𝕜 E F) (rp : p.radius > 0) (n : ℕ) : AnalyticAt 𝕜 (fun x ↦ p.changeOrigin x n) 0

Full source

/-- Power series terms are analytic as we vary the origin -/
theorem analyticAt_changeOrigin (p : FormalMultilinearSeries 𝕜 E F) (rp : p.radius > 0) (n : ℕ) :
    AnalyticAt 𝕜 (fun x ↦ p.changeOrigin x n) 0 :=
  (FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin p n rp).analyticAt

Analyticity of Change-of-Origin Terms in Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series over a field $\mathbb{K}$ with values in a normed space $F$, and let $E$ be a normed space over $\mathbb{K}$. If the radius of convergence $R$ of $p$ is positive ($R > 0$), then for any natural number $n$, the function $x \mapsto p.\text{changeOrigin}\, x\, n$ is analytic at the origin $0 \in E$.

HasFPowerSeriesWithinOnBall.changeOrigin theorem

 (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : ‖y‖ₑ < r) (hy : x + y ∈ insert x s) :
  HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖ₑ)

Full source

/-- If a function admits a power series expansion `p` within a set `s` on a ball `B (x, r)`, then
it also admits a power series on any subball of this ball (even with a different center provided
it belongs to `s`), given by `p.changeOrigin`. -/
theorem HasFPowerSeriesWithinOnBall.changeOrigin (hf : HasFPowerSeriesWithinOnBall f p s x r)
    (h : ‖y‖ₑ < r) (hy : x + y ∈ insert x s) :
    HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖ₑ) where
  r_le := by
    apply le_trans _ p.changeOrigin_radius
    exact tsub_le_tsub hf.r_le le_rfl
  r_pos := by simp [h]
  hasSum {z} h'z hz := by
    have : f (x + y + z) =
        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
      rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
      rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
      · have : insertinsert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
        rw [insert_eq_of_mem hy] at this
        apply this
        simpa [add_assoc] using h'z
      exact mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)
    rw [this]
    apply (p.changeOrigin y).hasSum
    refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz
    exact tsub_le_tsub hf.r_le le_rfl

Power Series Expansion at Translated Center: $f$ has power series $p.\text{changeOrigin}\, y$ at $x + y$ with radius $r - \|y\|$

Informal description

Let $f$ be a function defined on a subset $s$ of a normed space $E$ over a field $\mathbb{K}$, and suppose $f$ admits a power series expansion $p$ centered at $x \in E$ with radius of convergence $r > 0$ within $s$. For any $y \in E$ such that $\|y\| < r$ and $x + y \in s \cup \{x\}$, the function $f$ also admits a power series expansion given by $p.\text{changeOrigin}\, y$ centered at $x + y$ with radius of convergence at least $r - \|y\|$ within $s$.

HasFPowerSeriesOnBall.changeOrigin theorem

 (hf : HasFPowerSeriesOnBall f p x r) (h : (‖y‖₊ : ℝ≥0∞) < r) :
  HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ‖y‖₊)

Full source

/-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a
power series on any subball of this ball (even with a different center), given by `p.changeOrigin`.
-/
theorem HasFPowerSeriesOnBall.changeOrigin (hf : HasFPowerSeriesOnBall f p x r)
    (h : (‖y‖₊ : ℝ≥0∞) < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ‖y‖₊) := by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
  exact hf.changeOrigin h (by simp)

Power Series Expansion at Translated Center: $f$ has power series $p.\text{changeOrigin}\, y$ at $x + y$ with radius $r - \|y\|$

Informal description

Let $f$ be a function defined on a normed space $E$ over a field $\mathbb{K}$ that admits a power series expansion $p$ centered at $x \in E$ with radius of convergence $r > 0$. For any $y \in E$ with $\|y\| < r$, the function $f$ also admits a power series expansion given by $p.\text{changeOrigin}\, y$ centered at $x + y$ with radius of convergence at least $r - \|y\|$.

HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem theorem

(hf : HasFPowerSeriesWithinOnBall f p s x r) (h : y ∈ insert x s ∩ EMetric.ball x r) : AnalyticWithinAt 𝕜 f s y

Full source

/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
it is analytic at every point of this ball. -/
theorem HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem
    (hf : HasFPowerSeriesWithinOnBall f p s x r)
    (h : y ∈ insert x s ∩ EMetric.ball x r) : AnalyticWithinAt 𝕜 f s y := by
  have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h.2
  have := hf.changeOrigin this (by simpa using h.1)
  rw [add_sub_cancel] at this
  exact this.analyticWithinAt

Analyticity Within Ball for Functions with Power Series Expansion

Informal description

Let $f$ be a function defined on a subset $s$ of a normed space $E$ over a field $\mathbb{K}$, and suppose $f$ admits a power series expansion $p$ centered at $x \in E$ with radius of convergence $r > 0$ within $s$. For any point $y$ in the intersection of the ball $B(x, r)$ and the set $s \cup \{x\}$, the function $f$ is analytic at $y$ within $s$.

HasFPowerSeriesOnBall.analyticAt_of_mem theorem

(hf : HasFPowerSeriesOnBall f p x r) (h : y ∈ EMetric.ball x r) : AnalyticAt 𝕜 f y

Full source

/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
it is analytic at every point of this ball. -/
theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p x r)
    (h : y ∈ EMetric.ball x r) : AnalyticAt 𝕜 f y := by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  rw [← analyticWithinAt_univ]
  exact hf.analyticWithinAt_of_mem (by simpa using h)

Analyticity at Points Within Convergence Ball

Informal description

Let $f$ be a function defined on a normed space $E$ over a field $\mathbb{K}$ that admits a power series expansion $p$ centered at $x \in E$ with radius of convergence $r > 0$. For any point $y$ in the open ball $B(x, r)$, the function $f$ is analytic at $y$.

HasFPowerSeriesWithinOnBall.analyticOn theorem

(hf : HasFPowerSeriesWithinOnBall f p s x r) : AnalyticOn 𝕜 f (insert x s ∩ EMetric.ball x r)

Full source

theorem HasFPowerSeriesWithinOnBall.analyticOn (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    AnalyticOn 𝕜 f (insertinsert x s ∩ EMetric.ball x r) :=
  fun _ hy ↦ ((analyticWithinAt_insert (y := x)).2 (hf.analyticWithinAt_of_mem hy)).mono
    inter_subset_left

Analyticity of Power Series Expansion Within Ball Intersection

Informal description

HasFPowerSeriesOnBall.analyticOnNhd theorem

(hf : HasFPowerSeriesOnBall f p x r) : AnalyticOnNhd 𝕜 f (EMetric.ball x r)

Full source

theorem HasFPowerSeriesOnBall.analyticOnNhd (hf : HasFPowerSeriesOnBall f p x r) :
    AnalyticOnNhd 𝕜 f (EMetric.ball x r) :=
  fun _y hy => hf.analyticAt_of_mem hy

Analyticity of Power Series Expansion on Open Ball

Informal description

Let $f$ be a function defined on a normed space $E$ over a field $\mathbb{K}$ that admits a power series expansion $p$ centered at $x \in E$ with radius of convergence $r > 0$. Then $f$ is analytic on the open ball $B(x, r)$.

isOpen_analyticAt theorem

: IsOpen {x | AnalyticAt 𝕜 f x}

Full source

/-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such
that `f` is analytic at `x` is open. -/
theorem isOpen_analyticAt : IsOpen { x | AnalyticAt 𝕜 f x } := by
  rw [isOpen_iff_mem_nhds]
  rintro x ⟨p, r, hr⟩
  exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy

Openness of the Set of Analytic Points

Informal description

For any function $f$ from a normed vector space to a Banach space over a field $\mathbb{K}$, the set of points $x$ where $f$ is analytic is open.

AnalyticAt.eventually_analyticAt theorem

(h : AnalyticAt 𝕜 f x) : ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y

Full source

theorem AnalyticAt.eventually_analyticAt (h : AnalyticAt 𝕜 f x) :
    ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y :=
  (isOpen_analyticAt 𝕜 f).mem_nhds h

Local Analyticity Propagation Theorem

Informal description

If a function $f$ is analytic at a point $x$ in a normed vector space over a field $\mathbb{K}$, then $f$ is analytic at every point $y$ in some neighborhood of $x$.

AnalyticAt.exists_mem_nhds_analyticOnNhd theorem

(h : AnalyticAt 𝕜 f x) : ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s

Full source

theorem AnalyticAt.exists_mem_nhds_analyticOnNhd (h : AnalyticAt 𝕜 f x) :
    ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s :=
  h.eventually_analyticAt.exists_mem

Existence of Analytic Neighborhood Around Analytic Point

Informal description

If a function $f$ is analytic at a point $x$ in a normed vector space over a field $\mathbb{K}$, then there exists a neighborhood $s$ of $x$ such that $f$ is analytic on $s$.

AnalyticAt.exists_ball_analyticOnNhd theorem

(h : AnalyticAt 𝕜 f x) : ∃ r : ℝ, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r)

Full source

/-- If we're analytic at a point, we're analytic in a nonempty ball -/
theorem AnalyticAt.exists_ball_analyticOnNhd (h : AnalyticAt 𝕜 f x) :
    ∃ r : ℝ, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r) :=
  Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h

Existence of Analytic Ball Around Analytic Point

Informal description

If a function $f$ is analytic at a point $x$ in a normed vector space over a field $\mathbb{K}$, then there exists a positive radius $r > 0$ such that $f$ is analytic on the open ball centered at $x$ with radius $r$.