Mathlib.Analysis.Analytic.CPolynomialDef

HasFiniteFPowerSeriesOnBall structure

(f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E)
    (n : ℕ) (r : ℝ≥0∞) : Prop extends HasFPowerSeriesOnBall f p x r

Full source

/-- Given a function `f : E → F`, a formal multilinear series `p` and `n : ℕ`, we say that
`f` has `p` as a finite power series on the ball of radius `r > 0` around `x` if
`f (x + y) = ∑' pₘ yᵐ` for all `‖y‖ < r` and `pₙ = 0` for `n ≤ m`. -/
structure HasFiniteFPowerSeriesOnBall (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E)
    (n : ℕ) (r : ℝ≥0∞) : Prop extends HasFPowerSeriesOnBall f p x r where
  finite : ∀ (m : ℕ), n ≤ m → p m = 0

Finite power series expansion on a ball

Informal description

Given a function $f \colon E \to F$, a formal multilinear series $p$, a point $x \in E$, a natural number $n$, and an extended non-negative real number $r$, we say that $f$ has $p$ as a finite power series on the ball of radius $r$ centered at $x$ if: 1. $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for all $y$ with $\|y\| < r$ (where $p_m$ is an $m$-multilinear map), 2. $p_m = 0$ for all $m \geq n$.

HasFiniteFPowerSeriesOnBall.mk' theorem

 {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ℝ≥0∞} (finite : ∀ (m : ℕ), n ≤ m → p m = 0)
  (pos : 0 < r) (sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, p i fun _ ↦ y) = f (x + y)) :
  HasFiniteFPowerSeriesOnBall f p x n r

Full source

theorem HasFiniteFPowerSeriesOnBall.mk' {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    {n : ℕ} {r : ℝ≥0∞} (finite : ∀ (m : ℕ), n ≤ m → p m = 0) (pos : 0 < r)
    (sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i ∈ Finset.range n, p i fun _ ↦ y) = f (x + y)) :
    HasFiniteFPowerSeriesOnBall f p x n r where
  r_le := p.radius_eq_top_of_eventually_eq_zero (Filter.eventually_atTop.mpr ⟨n, finite⟩) ▸ le_top
  r_pos := pos
  hasSum hy := sum_eq _ hy ▸ hasSum_sum_of_ne_finset_zero fun m hm ↦ by
    rw [Finset.mem_range, not_lt] at hm; rw [finite m hm]; rfl
  finite := finite

Finite Power Series Expansion Criterion on a Ball

Informal description

Let $f \colon E \to F$ be a function, $p$ a formal multilinear series from $E$ to $F$, $x \in E$ a point, $n \in \mathbb{N}$ a natural number, and $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ an extended non-negative real number. Suppose that: 1. For all $m \geq n$, the $m$-th term of the series $p_m$ is zero, 2. The radius $r$ is positive ($0 < r$), 3. For all $y$ in the open ball of radius $r$ centered at $0$, the finite sum $\sum_{i=0}^{n-1} p_i(y, \ldots, y)$ equals $f(x + y)$. Then $f$ has $p$ as a finite power series expansion on the ball of radius $r$ centered at $x$, with the series truncated at order $n$.

HasFiniteFPowerSeriesAt definition

(f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (n : ℕ)

Full source

/-- Given a function `f : E → F`, a formal multilinear series `p` and `n : ℕ`, we say that
`f` has `p` as a finite power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a
neighborhood of `0`and `pₙ = 0` for `n ≤ m`. -/
def HasFiniteFPowerSeriesAt (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (n : ℕ) :=
  ∃ r, HasFiniteFPowerSeriesOnBall f p x n r

Finite power series expansion at a point

Informal description

Given a function $f \colon E \to F$, a formal multilinear series $p$, a point $x \in E$, and a natural number $n$, we say that $f$ has $p$ as a finite power series at $x$ if there exists a radius $r > 0$ such that: 1. $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for all $y$ with $\|y\| < r$ (where $p_m$ is an $m$-multilinear map), 2. $p_m = 0$ for all $m \geq n$.

HasFiniteFPowerSeriesAt.hasFPowerSeriesAt theorem

(hf : HasFiniteFPowerSeriesAt f p x n) : HasFPowerSeriesAt f p x

Full source

theorem HasFiniteFPowerSeriesAt.hasFPowerSeriesAt
    (hf : HasFiniteFPowerSeriesAt f p x n) : HasFPowerSeriesAt f p x :=
  let ⟨r, hf⟩ := hf
  ⟨r, hf.toHasFPowerSeriesOnBall⟩

Finite power series implies formal power series expansion

Informal description

If a function $f \colon E \to F$ has a finite power series expansion $p$ at a point $x \in E$ with bound $n \in \mathbb{N}$ (i.e., $p_m = 0$ for all $m \geq n$), then $f$ has $p$ as a formal power series expansion at $x$.

HasFiniteFPowerSeriesAt.finite theorem

(hf : HasFiniteFPowerSeriesAt f p x n) : ∀ m : ℕ, n ≤ m → p m = 0

Full source

theorem HasFiniteFPowerSeriesAt.finite (hf : HasFiniteFPowerSeriesAt f p x n) :
    ∀ m : ℕ, n ≤ m → p m = 0 := let ⟨_, hf⟩ := hf; hf.finite

Vanishing of Higher Terms in Finite Power Series Expansion

Informal description

Let $f \colon E \to F$ be a function with a finite power series expansion at $x \in E$ given by the formal multilinear series $p$ and bound $n \in \mathbb{N}$. Then for all $m \geq n$, the $m$-th term of the series $p_m$ is identically zero.

CPolynomialAt definition

(f : E → F) (x : E)

Full source

/-- Given a function `f : E → F`, we say that `f` is continuously polynomial (cpolynomial)
at `x` if it admits a finite power series expansion around `x`. -/
def CPolynomialAt (f : E → F) (x : E) :=
  ∃ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), HasFiniteFPowerSeriesAt f p x n

Continuously polynomial function at a point

Informal description

A function $ f \colon E \to F $ is called *continuously polynomial* at a point $ x \in E $ if there exists a formal multilinear series $ p $ and a natural number $ n $ such that $ f $ admits a finite power series expansion around $ x $ with $ p $, where $ p_m = 0 $ for all $ m \geq n $.

CPolynomialOn definition

(f : E → F) (s : Set E)

Full source

/-- Given a function `f : E → F`, we say that `f` is continuously polynomial on a set `s`
if it is continuously polynomial around every point of `s`. -/
def CPolynomialOn (f : E → F) (s : Set E) :=
  ∀ x, x ∈ s → CPolynomialAt 𝕜 f x

Continuously polynomial function on a set

Informal description

A function $ f \colon E \to F $ is called *continuously polynomial* on a set $ s \subseteq E $ if for every point $ x \in s $, the function $ f $ is continuously polynomial at $ x $. This means that around each $ x \in s $, $ f $ admits a finite power series expansion with a formal multilinear series $ p $ and a bound $ n $ such that $ p_m = 0 $ for all $ m \geq n $.

HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) : HasFiniteFPowerSeriesAt f p x n

Full source

theorem HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt
    (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    HasFiniteFPowerSeriesAt f p x n :=
  ⟨r, hf⟩

Finite power series on ball implies finite power series at point

Informal description

If a function $f \colon E \to F$ has a finite power series expansion $p$ on a ball of radius $r$ centered at $x$ with bound $n$, then $f$ has a finite power series expansion $p$ at the point $x$ with the same bound $n$.

HasFiniteFPowerSeriesAt.cpolynomialAt theorem

(hf : HasFiniteFPowerSeriesAt f p x n) : CPolynomialAt 𝕜 f x

Full source

theorem HasFiniteFPowerSeriesAt.cpolynomialAt (hf : HasFiniteFPowerSeriesAt f p x n) :
    CPolynomialAt 𝕜 f x :=
  ⟨p, n, hf⟩

Finite power series expansion implies continuously polynomial at a point

Informal description

If a function $ f \colon E \to F $ has a finite power series expansion $ p $ at a point $ x \in E $ with bound $ n $, then $ f $ is continuously polynomial at $ x $.

HasFiniteFPowerSeriesOnBall.cpolynomialAt theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) : CPolynomialAt 𝕜 f x

Full source

theorem HasFiniteFPowerSeriesOnBall.cpolynomialAt (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    CPolynomialAt 𝕜 f x :=
  hf.hasFiniteFPowerSeriesAt.cpolynomialAt

Finite power series expansion on ball implies continuously polynomial at center

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a finite power series expansion $p$ on a ball of radius $r > 0$ centered at $x \in E$ with bound $n$ (i.e., $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for $\|y\| < r$ and $p_m = 0$ for $m \geq n$), then $f$ is continuously polynomial at $x$.

CPolynomialAt.analyticAt theorem

(hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜 f x

Full source

theorem CPolynomialAt.analyticAt (hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜 f x :=
  let ⟨p, _, hp⟩ := hf
  ⟨p, hp.hasFPowerSeriesAt⟩

Continuously polynomial functions are analytic

Informal description

If a function $f \colon E \to F$ is continuously polynomial at a point $x \in E$, then $f$ is analytic at $x$.

CPolynomialAt.analyticWithinAt theorem

{s : Set E} (hf : CPolynomialAt 𝕜 f x) : AnalyticWithinAt 𝕜 f s x

Full source

theorem CPolynomialAt.analyticWithinAt {s : Set E} (hf : CPolynomialAt 𝕜 f x) :
    AnalyticWithinAt 𝕜 f s x :=
  hf.analyticAt.analyticWithinAt

Continuously polynomial functions are analytic within any subset

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function. If $f$ is continuously polynomial at a point $x \in E$, then for any subset $s \subseteq E$, the function $f$ is analytic within $s$ at $x$.

CPolynomialOn.analyticOnNhd theorem

{s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s

Full source

theorem CPolynomialOn.analyticOnNhd {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s :=
  fun x hx ↦ (hf x hx).analyticAt

Continuously Polynomial Functions are Locally Analytic

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function. If $f$ is continuously polynomial on a set $s \subseteq E$, then $f$ is analytic on some neighborhood of each point in $s$.

CPolynomialOn.analyticOn theorem

{s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s

Full source

theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s :=
  hf.analyticOnNhd.analyticOn

Continuously Polynomial Functions are Analytic on Their Domain

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function. If $f$ is continuously polynomial on a set $s \subseteq E$, then $f$ is analytic on $s$.

HasFiniteFPowerSeriesOnBall.congr theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) (hg : EqOn f g (EMetric.ball x r)) : HasFiniteFPowerSeriesOnBall g p x n r

Full source

theorem HasFiniteFPowerSeriesOnBall.congr (hf : HasFiniteFPowerSeriesOnBall f p x n r)
    (hg : EqOn f g (EMetric.ball x r)) : HasFiniteFPowerSeriesOnBall g p x n r :=
  ⟨hf.1.congr hg, hf.finite⟩

Congruence of Finite Power Series Expansions on a Ball

Informal description

Let $f, g \colon E \to F$ be functions, $p$ a formal multilinear series from $E$ to $F$, $x \in E$, $n \in \mathbb{N}$, and $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$. If $f$ has a finite power series expansion on the ball of radius $r$ centered at $x$ with bound $n$ (i.e., $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for $\|y\| < r$ and $p_m = 0$ for $m \geq n$), and $f$ and $g$ coincide on this ball, then $g$ also has the same finite power series expansion on this ball with bound $n$.

HasFiniteFPowerSeriesOnBall.of_le theorem

{m n : ℕ} (h : HasFiniteFPowerSeriesOnBall f p x n r) (hmn : n ≤ m) : HasFiniteFPowerSeriesOnBall f p x m r

Full source

theorem HasFiniteFPowerSeriesOnBall.of_le {m n : ℕ}
    (h : HasFiniteFPowerSeriesOnBall f p x n r) (hmn : n ≤ m) :
    HasFiniteFPowerSeriesOnBall f p x m r :=
  ⟨h.toHasFPowerSeriesOnBall, fun i hi ↦ h.finite i (hmn.trans hi)⟩

Finite Power Series Expansion Persists Under Degree Increase

Informal description

Let $f \colon E \to F$ be a function with a finite power series expansion $p$ on a ball of radius $r$ centered at $x \in E$, bounded by degree $n$. If $m$ is a natural number such that $n \leq m$, then $f$ also has $p$ as a finite power series expansion on the same ball, now bounded by degree $m$.

HasFiniteFPowerSeriesAt.of_le theorem

{m n : ℕ} (h : HasFiniteFPowerSeriesAt f p x n) (hmn : n ≤ m) : HasFiniteFPowerSeriesAt f p x m

Full source

theorem HasFiniteFPowerSeriesAt.of_le {m n : ℕ}
    (h : HasFiniteFPowerSeriesAt f p x n) (hmn : n ≤ m) :
    HasFiniteFPowerSeriesAt f p x m := by
  rcases h with ⟨r, hr⟩
  exact ⟨r, hr.of_le hmn⟩

Finite Power Series Expansion Persists Under Degree Increase at a Point

Informal description

Let $f \colon E \to F$ be a function with a finite power series expansion $p$ at $x \in E$, bounded by degree $n$. If $m$ is a natural number such that $n \leq m$, then $f$ also has $p$ as a finite power series expansion at $x$, now bounded by degree $m$.

HasFiniteFPowerSeriesOnBall.comp_sub theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) : HasFiniteFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) n r

Full source

/-- If a function `f` has a finite power series `p` around `x`, then the function
`z ↦ f (z - y)` has the same finite power series around `x + y`. -/
theorem HasFiniteFPowerSeriesOnBall.comp_sub (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) :
    HasFiniteFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) n r :=
  ⟨hf.1.comp_sub y, hf.finite⟩

Finite power series expansion under translation: $f(z-y)$ at $x+y$

Informal description

Let $f \colon E \to F$ have a finite power series expansion $p$ around $x$ on a ball of radius $r$, i.e., $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for $\|y\| < r$ and $p_m = 0$ for $m \geq n$. Then for any $y \in E$, the function $z \mapsto f(z - y)$ has the same finite power series expansion $p$ around $x + y$ on the ball of radius $r$.

HasFiniteFPowerSeriesOnBall.mono theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) (r'_pos : 0 < r') (hr : r' ≤ r) : HasFiniteFPowerSeriesOnBall f p x n r'

Full source

theorem HasFiniteFPowerSeriesOnBall.mono (hf : HasFiniteFPowerSeriesOnBall f p x n r)
    (r'_pos : 0 < r') (hr : r' ≤ r) : HasFiniteFPowerSeriesOnBall f p x n r' :=
  ⟨hf.1.mono r'_pos hr, hf.finite⟩

Finite Power Series Expansion is Preserved Under Ball Contraction

Informal description

Let $f \colon E \to F$ be a function with a finite power series expansion $p$ on a ball of radius $r$ centered at $x \in E$, bounded by $n \in \mathbb{N}$. For any positive radius $r'$ with $0 < r' \leq r$, the function $f$ also has the finite power series expansion $p$ on the ball of radius $r'$ centered at $x$, with the same bound $n$.

HasFiniteFPowerSeriesAt.congr theorem

(hf : HasFiniteFPowerSeriesAt f p x n) (hg : f =ᶠ[𝓝 x] g) : HasFiniteFPowerSeriesAt g p x n

Full source

theorem HasFiniteFPowerSeriesAt.congr (hf : HasFiniteFPowerSeriesAt f p x n) (hg : f =ᶠ[𝓝 x] g) :
    HasFiniteFPowerSeriesAt g p x n :=
  Exists.imp (fun _ hg ↦ ⟨hg, hf.finite⟩) (hf.hasFPowerSeriesAt.congr hg)

Local Equality Preserves Finite Power Series Expansion

Informal description

Let $f \colon E \to F$ have a finite power series expansion at $x \in E$ given by the formal multilinear series $p$ with bound $n \in \mathbb{N}$. If $g \colon E \to F$ is equal to $f$ in a neighborhood of $x$, then $g$ also has the same finite power series expansion $p$ at $x$ with bound $n$.

HasFiniteFPowerSeriesAt.eventually theorem

(hf : HasFiniteFPowerSeriesAt f p x n) : ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFiniteFPowerSeriesOnBall f p x n r

Full source

protected theorem HasFiniteFPowerSeriesAt.eventually (hf : HasFiniteFPowerSeriesAt f p x n) :
    ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFiniteFPowerSeriesOnBall f p x n r :=
  hf.hasFPowerSeriesAt.eventually.mono fun _ h ↦ ⟨h, hf.finite⟩

Local Existence of Finite Power Series Expansion for Small Radii

Informal description

Let $f \colon E \to F$ be a function with a finite power series expansion $p$ at a point $x \in E$ with bound $n \in \mathbb{N}$. Then for all sufficiently small radii $r > 0$, the function $f$ has the finite power series expansion $p$ on the ball of radius $r$ centered at $x$, with the same bound $n$.

CPolynomialAt.congr theorem

(hf : CPolynomialAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : CPolynomialAt 𝕜 g x

Full source

theorem CPolynomialAt.congr (hf : CPolynomialAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : CPolynomialAt 𝕜 g x :=
  let ⟨_, _, hpf⟩ := hf
  (hpf.congr hg).cpolynomialAt

Local equality preserves continuously polynomial property at a point

Informal description

Let $f \colon E \to F$ be continuously polynomial at a point $x \in E$. If $g \colon E \to F$ is equal to $f$ in a neighborhood of $x$, then $g$ is also continuously polynomial at $x$.

CPolynomialAt_congr theorem

(h : f =ᶠ[𝓝 x] g) : CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x

Full source

theorem CPolynomialAt_congr (h : f =ᶠ[𝓝 x] g) : CPolynomialAtCPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x :=
  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩

Local equality preserves continuously polynomial property at a point (iff version)

Informal description

Let $ f, g \colon E \to F $ be functions that are equal in a neighborhood of $ x \in E $. Then $ f $ is continuously polynomial at $ x $ if and only if $ g $ is continuously polynomial at $ x $.

CPolynomialOn.mono theorem

{s t : Set E} (hf : CPolynomialOn 𝕜 f t) (hst : s ⊆ t) : CPolynomialOn 𝕜 f s

Full source

theorem CPolynomialOn.mono {s t : Set E} (hf : CPolynomialOn 𝕜 f t) (hst : s ⊆ t) :
    CPolynomialOn 𝕜 f s :=
  fun z hz => hf z (hst hz)

Continuous polynomiality is preserved under subset restriction

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f : E \to F$ be a function. For any subsets $s, t \subseteq E$ with $s \subseteq t$, if $f$ is continuously polynomial on $t$, then $f$ is continuously polynomial on $s$.

CPolynomialOn.congr' theorem

{s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) : CPolynomialOn 𝕜 g s

Full source

theorem CPolynomialOn.congr' {s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
    CPolynomialOn 𝕜 g s :=
  fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)

Local equality preserves continuously polynomial property on a set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f, g \colon E \to F$ be functions. For any subset $s \subseteq E$, if $f$ is continuously polynomial on $s$ and $g$ is equal to $f$ in the neighborhood filter of $s$, then $g$ is also continuously polynomial on $s$.

CPolynomialOn_congr' theorem

{s : Set E} (h : f =ᶠ[𝓝ˢ s] g) : CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

Full source

theorem CPolynomialOn_congr' {s : Set E} (h : f =ᶠ[𝓝ˢ s] g) :
    CPolynomialOnCPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s :=
  ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩

Equivalence of Continuously Polynomial Property Under Local Equality on a Set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f, g \colon E \to F$ be functions. For any subset $s \subseteq E$, the functions $f$ and $g$ are equal in the neighborhood filter of $s$ if and only if $f$ is continuously polynomial on $s$ exactly when $g$ is continuously polynomial on $s$.

CPolynomialOn.congr theorem

{s : Set E} (hs : IsOpen s) (hf : CPolynomialOn 𝕜 f s) (hg : s.EqOn f g) : CPolynomialOn 𝕜 g s

Full source

theorem CPolynomialOn.congr {s : Set E} (hs : IsOpen s) (hf : CPolynomialOn 𝕜 f s)
    (hg : s.EqOn f g) : CPolynomialOn 𝕜 g s :=
  hf.congr' <| mem_nhdsSet_iff_forall.mpr
    (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)

Pointwise Equality Preserves Continuously Polynomial Property on Open Sets

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f, g \colon E \to F$ be functions. For any open subset $s \subseteq E$, if $f$ is continuously polynomial on $s$ and $f$ and $g$ are equal on $s$, then $g$ is also continuously polynomial on $s$.

CPolynomialOn_congr theorem

{s : Set E} (hs : IsOpen s) (h : s.EqOn f g) : CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

Full source

theorem CPolynomialOn_congr {s : Set E} (hs : IsOpen s) (h : s.EqOn f g) :
    CPolynomialOnCPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s :=
  ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩

Equivalence of Continuously Polynomial Property Under Pointwise Equality on Open Sets

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f, g \colon E \to F$ be functions. For any open subset $s \subseteq E$, if $f$ and $g$ are equal on $s$, then $f$ is continuously polynomial on $s$ if and only if $g$ is continuously polynomial on $s$.

ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall theorem

 (g : F →L[𝕜] G) (h : HasFiniteFPowerSeriesOnBall f p x n r) :
  HasFiniteFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x n r

Full source

/-- If a function `f` has a finite power series `p` on a ball and `g` is a continuous linear map,
then `g ∘ f` has the finite power series `g ∘ p` on the same ball. -/
theorem ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall (g : F →L[𝕜] G)
    (h : HasFiniteFPowerSeriesOnBall f p x n r) :
    HasFiniteFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x n r :=
  ⟨g.comp_hasFPowerSeriesOnBall h.1, fun m hm ↦ by
    rw [compFormalMultilinearSeries_apply, h.finite m hm]
    ext; exact map_zero g⟩

Finite Power Series Expansion under Continuous Linear Composition

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function with a finite power series expansion $p$ on a ball of radius $r$ centered at $x \in E$, bounded by $n \in \mathbb{N}$. If $g \colon F \to G$ is a continuous $\mathbb{K}$-linear map, then the composition $g \circ f$ has a finite power series expansion given by $g \circ p$ on the same ball, with the same bound $n$.

ContinuousLinearMap.comp_cpolynomialOn theorem

{s : Set E} (g : F →L[𝕜] G) (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (g ∘ f) s

Full source

/-- If a function `f` is continuously polynomial on a set `s` and `g` is a continuous linear map,
then `g ∘ f` is continuously polynomial on `s`. -/
theorem ContinuousLinearMap.comp_cpolynomialOn {s : Set E} (g : F →L[𝕜] G)
    (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (g ∘ f) s := by
  rintro x hx
  rcases h x hx with ⟨p, n, r, hp⟩
  exact ⟨g.compFormalMultilinearSeries p, n, r, g.comp_hasFiniteFPowerSeriesOnBall hp⟩

Continuous linear maps preserve continuously polynomial functions

Informal description

Let $E$, $F$, and $G$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function that is continuously polynomial on a set $s \subseteq E$. If $g \colon F \to G$ is a continuous $\mathbb{K}$-linear map, then the composition $g \circ f$ is continuously polynomial on $s$.

HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero theorem

 (hf : ∀ y ∈ EMetric.ball x r, f y = 0) (r_pos : 0 < r) (hp : ∀ n, p n = 0) : HasFiniteFPowerSeriesOnBall f p x 0 r

Full source

theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (hf : ∀ y ∈ EMetric.ball x r, f y = 0)
    (r_pos : 0 < r) (hp : ∀ n, p n = 0) : HasFiniteFPowerSeriesOnBall f p x 0 r := by
  refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
  · rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
    exact le_top
  · intro y hy
    rw [hf (x + y)]
    · convert hasSum_zero
      rw [hp, ContinuousMultilinearMap.zero_apply]
    · rwa [EMetric.mem_ball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_eq_enorm, ← EMetric.mem_ball]

Zero Function Has Trivial Finite Power Series Expansion on Ball

Informal description

Let $f \colon E \to F$ be a function that is identically zero on an extended metric ball $\{y \in E \mid \|y - x\| < r\}$ centered at $x$ with radius $r > 0$, and let $p$ be a formal multilinear series such that $p_n = 0$ for all $n \in \mathbb{N}$. Then $f$ has a finite power series expansion on this ball with bound $0$, i.e., $f$ can be expressed as the sum of the zero series on this ball.

HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero theorem

(hf : HasFiniteFPowerSeriesAt f pf x 0) : f =ᶠ[𝓝 x] 0

Full source

/-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
neighborhood of `x`. -/
theorem HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero
    (hf : HasFiniteFPowerSeriesAt f pf x 0) : f =ᶠ[𝓝 x] 0 :=
  Filter.eventuallyEq_iff_exists_mem.mpr (let ⟨r, hf⟩ := hf; ⟨EMetric.ball x r,
    EMetric.ball_mem_nhds x hf.r_pos, fun y hy ↦ hf.eq_zero_of_bound_zero y hy⟩)

Vanishing of Functions with Trivial Power Series Expansion

Informal description

If a function $f \colon E \to F$ has a finite formal power series expansion at a point $x \in E$ with all coefficients $p_m = 0$ for $m \geq 0$ (i.e., bounded by $0$), then $f$ is identically zero in a neighborhood of $x$.

HasFiniteFPowerSeriesAt.eventually_const_of_bound_one theorem

(hf : HasFiniteFPowerSeriesAt f pf x 1) : f =ᶠ[𝓝 x] (fun _ => f x)

Full source

/-- If `f` has a formal power series at x bounded by `1`, then `f` is constant equal
to `f x` in a neighborhood of `x`. -/
theorem HasFiniteFPowerSeriesAt.eventually_const_of_bound_one
    (hf : HasFiniteFPowerSeriesAt f pf x 1) : f =ᶠ[𝓝 x] (fun _ => f x) :=
  Filter.eventuallyEq_iff_exists_mem.mpr (let ⟨r, hf⟩ := hf; ⟨EMetric.ball x r,
    EMetric.ball_mem_nhds x hf.r_pos, fun y hy ↦ hf.eq_const_of_bound_one y hy⟩)

Local Constancy of Functions with Finite Power Series Bounded by One

Informal description

Let $f \colon E \to F$ be a function that admits a finite formal power series expansion at $x \in E$ bounded by $1$. Then $f$ is eventually constant in a neighborhood of $x$, with value $f(x)$. In other words, there exists a neighborhood $U$ of $x$ such that for all $y \in U$, $f(y) = f(x)$.

HasFiniteFPowerSeriesOnBall.continuousOn theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) : ContinuousOn f (EMetric.ball x r)

Full source

/-- If a function admits a finite power series expansion on a disk, then it is continuous there. -/
protected theorem HasFiniteFPowerSeriesOnBall.continuousOn
    (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    ContinuousOn f (EMetric.ball x r) := hf.1.continuousOn

Continuity of Functions with Finite Power Series Expansion on a Ball

Informal description

Let $f \colon E \to F$ be a function that admits a finite power series expansion $p$ on a ball of radius $r$ centered at $x \in E$, with $p_m = 0$ for all $m \geq n$. Then $f$ is continuous on the ball $\{y \in E \mid \|y - x\| < r\}$.

HasFiniteFPowerSeriesAt.continuousAt theorem

(hf : HasFiniteFPowerSeriesAt f p x n) : ContinuousAt f x

Full source

protected theorem HasFiniteFPowerSeriesAt.continuousAt (hf : HasFiniteFPowerSeriesAt f p x n) :
    ContinuousAt f x := hf.hasFPowerSeriesAt.continuousAt

Continuity at a Point for Functions with Finite Power Series Expansion

Informal description

Let $f \colon E \to F$ be a function that admits a finite formal power series expansion at a point $x \in E$ (i.e., there exists a formal multilinear series $p$ and a natural number $n$ such that $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for all $y$ in some neighborhood of $0$, with $p_m = 0$ for all $m \geq n$). Then $f$ is continuous at $x$.

CPolynomialAt.continuousAt theorem

(hf : CPolynomialAt 𝕜 f x) : ContinuousAt f x

Full source

protected theorem CPolynomialAt.continuousAt (hf : CPolynomialAt 𝕜 f x) : ContinuousAt f x :=
  hf.analyticAt.continuousAt

Continuity of Continuously Polynomial Functions at a Point

Informal description

If a function $f \colon E \to F$ is continuously polynomial at a point $x \in E$, then $f$ is continuous at $x$.

CPolynomialOn.continuousOn theorem

{s : Set E} (hf : CPolynomialOn 𝕜 f s) : ContinuousOn f s

Full source

protected theorem CPolynomialOn.continuousOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) :
    ContinuousOn f s :=
  hf.analyticOnNhd.continuousOn

Continuity of Continuously Polynomial Functions on a Set

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function. If $f$ is continuously polynomial on a set $s \subseteq E$, then $f$ is continuous on $s$.

CPolynomialOn.continuous theorem

{f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f

Full source

/-- Continuously polynomial everywhere implies continuous -/
theorem CPolynomialOn.continuous {f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f := by
  rw [continuous_iff_continuousOn_univ]; exact fa.continuousOn

Continuity of Globally Continuously Polynomial Functions

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function. If $f$ is continuously polynomial on the entire space $E$, then $f$ is continuous on $E$.

FormalMultilinearSeries.sum_of_finite theorem

(p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) : p.sum x = p.partialSum n x

Full source

protected theorem FormalMultilinearSeries.sum_of_finite (p : FormalMultilinearSeries 𝕜 E F)
    {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) :
    p.sum x = p.partialSum n x :=
  tsum_eq_sum fun m hm ↦ by rw [Finset.mem_range, not_lt] at hm; rw [hn m hm]; rfl

Sum of Finite Formal Multilinear Series Equals Partial Sum

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to a normed space $F$ over a field $\mathbb{K}$, and let $n$ be a natural number such that $p_m = 0$ for all $m \geq n$. Then for any $x \in E$, the sum of the series $p.\text{sum}(x)$ equals the $n$-th partial sum $p.\text{partialSum} n x$.

FormalMultilinearSeries.hasSum_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) :
  HasSum (fun n : ℕ => p n fun _ => x) (p.sum x)

Full source

/-- A finite formal multilinear series sums to its sum at every point. -/
protected theorem FormalMultilinearSeries.hasSum_of_finite (p : FormalMultilinearSeries 𝕜 E F)
    {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) :
    HasSum (fun n : ℕ => p n fun _ => x) (p.sum x) :=
  summable_of_ne_finset_zero (s := .range n)
    (fun m hm ↦ by rw [Finset.mem_range, not_lt] at hm; rw [hn m hm]; rfl)
    |>.hasSum

Convergence of Finite Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to a normed space $F$ over a field $\mathbb{K}$, and let $n$ be a natural number such that $p_m = 0$ for all $m \geq n$. Then for any $x \in E$, the series $\sum_{n=0}^\infty p_n(x, \dots, x)$ converges to $p.\text{sum}(x)$.

FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) : HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤

Full source

/-- The sum of a finite power series `p` admits `p` as a power series. -/
protected theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite
    (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) :
    HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤ where
  r_le := by rw [radius_eq_top_of_forall_image_add_eq_zero p n fun _ => hn _ (Nat.le_add_left _ _)]
  r_pos := zero_lt_top
  finite := hn
  hasSum {y} _ := by rw [zero_add]; exact p.hasSum_of_finite hn y

Finite formal multilinear series induces finite power series expansion on entire space

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to a normed space $F$ over a field $\mathbb{K}$, and let $n$ be a natural number such that $p_m = 0$ for all $m \geq n$. Then the sum of the series $p.\text{sum}$ has $p$ as a finite power series expansion on the entire space (i.e., with radius $\top$), centered at $0$ with bound $n$.

HasFiniteFPowerSeriesOnBall.sum theorem

(h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : y ∈ EMetric.ball (0 : E) r) : f (x + y) = p.sum y

Full source

theorem HasFiniteFPowerSeriesOnBall.sum (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E}
    (hy : y ∈ EMetric.ball (0 : E) r) : f (x + y) = p.sum y :=
  (h.hasSum hy).tsum_eq.symm

Finite Power Series Expansion Formula on a Ball

Informal description

Let $f \colon E \to F$ be a function with a finite formal multilinear series expansion $p$ centered at $x \in E$ up to order $n$ on a ball of radius $r$. Then for any $y$ in the ball of radius $r$ centered at $0$ in $E$, we have $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$, where $p_m = 0$ for all $m \geq n$.

FormalMultilinearSeries.continuousOn_of_finite theorem

(p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) : Continuous p.sum

Full source

/-- The sum of a finite power series is continuous. -/
protected theorem FormalMultilinearSeries.continuousOn_of_finite
    (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) :
    Continuous p.sum := by
  rw [continuous_iff_continuousOn_univ, ← Metric.emetric_ball_top]
  exact (p.hasFiniteFPowerSeriesOnBall_of_finite hn).continuousOn

Continuity of Sum Function for Finite Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to a normed space $F$ over a field $\mathbb{K}$, and let $n$ be a natural number such that $p_m = 0$ for all $m \geq n$. Then the sum function $p.\text{sum}$ is continuous on $E$.

FormalMultilinearSeries.changeOriginSeriesTerm_bound theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k l : ℕ) {s : Finset (Fin (k + l))}
  (hs : s.card = l) (hkl : n ≤ k + l) : p.changeOriginSeriesTerm k l s hs = 0

Full source

/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOriginSeriesTerm k l = 0` for `n ≤ k + l`. -/
lemma changeOriginSeriesTerm_bound (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k l : ℕ) {s : Finset (Fin (k + l))}
    (hs : s.card = l) (hkl : n ≤ k + l) :
    p.changeOriginSeriesTerm k l s hs = 0 := by
  rw [changeOriginSeriesTerm, hn _ hkl, map_zero]

Vanishing of Change-of-Origin Series Terms for Finite Multilinear Series

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and suppose $p_m = 0$ for all $m \geq n$. Then for any integers $k, l \geq 0$ with $n \leq k + l$, and any subset $s$ of $\text{Fin}(k + l)$ with cardinality $l$, the change-of-origin series term $p.\text{changeOriginSeriesTerm}\,k\,l\,s\,hs$ vanishes, where $hs$ is a proof that $s$ has cardinality $l$.

FormalMultilinearSeries.changeOriginSeries_finite_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) :
  ∀ {m : ℕ}, n ≤ k + m → p.changeOriginSeries k m = 0

Full source

/-- If `p` is a finite formal multilinear series, then so is `p.changeOriginSeries k` for every
`k` in `ℕ`. More precisely, if `p m = 0` for `n ≤ m`, then `p.changeOriginSeries k m = 0` for
`n ≤ k + m`. -/
lemma changeOriginSeries_finite_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) : ∀ {m : ℕ}, n ≤ k + m →
    p.changeOriginSeries k m = 0 := by
  intro m hm
  rw [changeOriginSeries]
  exact Finset.sum_eq_zero (fun _ _ => p.changeOriginSeriesTerm_bound hn _ _ _ hm)

Finite Bound Preservation in Change-of-Origin Series for Multilinear Series

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and suppose $p_m = 0$ for all $m \geq n$. Then for any natural number $k$, the change-of-origin series $p.\text{changeOriginSeries}\,k$ satisfies $p.\text{changeOriginSeries}\,k\,m = 0$ for all $m$ such that $n \leq k + m$.

FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) :
  (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)

Full source

lemma changeOriginSeries_sum_eq_partialSum_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) :
    (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k) := by
  ext x
  rw [partialSum, FormalMultilinearSeries.sum,
    tsum_eq_sum (f := fun m => p.changeOriginSeries k m (fun _ => x)) (s := Finset.range (n - k))]
  intro m hm
  rw [Finset.mem_range, not_lt] at hm
  rw [p.changeOriginSeries_finite_of_finite hn k (by rw [add_comm]; exact Nat.le_add_of_sub_le hm),
    ContinuousMultilinearMap.zero_apply]

Sum of Change-of-Origin Series Equals Partial Sum for Finite Multilinear Series

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and suppose $p_m = 0$ for all $m \geq n$. Then for any natural number $k$, the sum of the change-of-origin series $p.\text{changeOriginSeries}\,k$ is equal to its partial sum up to order $n - k$, i.e., \[ \sum (p.\text{changeOriginSeries}\,k) = (p.\text{changeOriginSeries}\,k).\text{partialSum}\,(n - k). \]

FormalMultilinearSeries.changeOrigin_finite_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) {k : ℕ} (hk : n ≤ k) :
  p.changeOrigin x k = 0

Full source

/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOrigin x k = 0` for `n ≤ k`. -/
lemma changeOrigin_finite_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) {k : ℕ} (hk : n ≤ k) :
    p.changeOrigin x k = 0 := by
  rw [changeOrigin, p.changeOriginSeries_sum_eq_partialSum_of_finite hn]
  apply Finset.sum_eq_zero
  intro m hm
  rw [Finset.mem_range] at hm
  rw [p.changeOriginSeries_finite_of_finite hn k (le_add_of_le_left hk),
    ContinuousMultilinearMap.zero_apply]

Vanishing of Change-of-Origin Series for Finite Multilinear Series: $p.\text{changeOrigin}\,x\,k = 0$ when $k \geq n$

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and suppose $p_m = 0$ for all $m \geq n$. Then for any natural number $k \geq n$, the change-of-origin series satisfies $p.\text{changeOrigin}\,x\,k = 0$.

FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (k : ℕ) (hn : ∀ (m : ℕ), n + k ≤ m → p m = 0) :
  HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤

Full source

theorem hasFiniteFPowerSeriesOnBall_changeOrigin (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (k : ℕ) (hn : ∀ (m : ℕ), n + k ≤ m → p m = 0) :
    HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤ :=
  (p.changeOriginSeries k).hasFiniteFPowerSeriesOnBall_of_finite
    (fun _ hm => p.changeOriginSeries_finite_of_finite hn k
    (by rw [add_comm n k]; apply add_le_add_left hm))

Finite Power Series Expansion for Change-of-Origin Function

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and let $n$ and $k$ be natural numbers such that $p_m = 0$ for all $m \geq n + k$. Then the function $y \mapsto p.\text{changeOrigin}\,y\,k$ has the change-of-origin series $p.\text{changeOriginSeries}\,k$ as its finite power series expansion on the entire space (radius $\top$), centered at $0$ with bound $n$.

FormalMultilinearSeries.changeOrigin_eval_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (x y : E) :
  (p.changeOrigin x).sum y = p.sum (x + y)

Full source

theorem changeOrigin_eval_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (x y : E) :
    (p.changeOrigin x).sum y = p.sum (x + y) := by
  let f (s : Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) : F :=
    p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) fun _ ↦ y
  have finsupp : f.support.Finite := by
    apply Set.Finite.subset (s := changeOriginIndexEquivchangeOriginIndexEquiv ⁻¹' (Sigma.fst ⁻¹' {m | m < n}))
    · apply Set.Finite.preimage (Equiv.injective _).injOn
      simp_rw [← {m | m < n}.iUnion_of_singleton_coe, preimage_iUnion, ← range_sigmaMk]
      exact finite_iUnion fun _ ↦ finite_range _
    · refine fun s ↦ Not.imp_symm fun hs ↦ ?_
      simp only [preimage_setOf_eq, changeOriginIndexEquiv_apply_fst, mem_setOf, not_lt] at hs
      dsimp only [f]
      rw [changeOriginSeriesTerm_bound p hn _ _ _ hs, ContinuousMultilinearMap.zero_apply,
        ContinuousMultilinearMap.zero_apply]
  have hfkl k l : HasSum (f ⟨k, l, ·⟩) (changeOriginSeries p k l (fun _ ↦ x) fun _ ↦ y) := by
    simp_rw [changeOriginSeries, ContinuousMultilinearMap.sum_apply]; apply hasSum_fintype
  have hfk k : HasSum (f ⟨k, ·⟩) (changeOrigin p x k fun _ ↦ y) := by
    have (m) (hm : m ∉ Finset.range n) : changeOriginSeries p k m (fun _ ↦ x) = 0 := by
      rw [Finset.mem_range, not_lt] at hm
      rw [changeOriginSeries_finite_of_finite _ hn _ (le_add_of_le_right hm),
        ContinuousMultilinearMap.zero_apply]
    rw [changeOrigin, FormalMultilinearSeries.sum,
      ContinuousMultilinearMap.tsum_eval (summable_of_ne_finset_zero this)]
    refine (summable_of_ne_finset_zero (s := Finset.range n) fun m hm ↦ ?_).hasSum.sigma_of_hasSum
      (hfkl k) (summable_of_finite_support <| finsupp.preimage sigma_mk_injective.injOn)
    rw [this m hm, ContinuousMultilinearMap.zero_apply]
  have hf : HasSum f ((p.changeOrigin x).sum y) :=
    ((p.changeOrigin x).hasSum_of_finite (fun _ ↦ changeOrigin_finite_of_finite p hn) _)
      |>.sigma_of_hasSum hfk (summable_of_finite_support finsupp)
  refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_)
  refine (p.hasSum_of_finite hn (x + y)).sigma_of_hasSum (fun n ↦ ?_)
    (changeOriginIndexEquiv.symm.summable_iff.2 hf.summable)
  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 Evaluation of Change-of-Origin Series for Finite Multilinear Series: $(p.\text{changeOrigin}\,x).\text{sum}\,y = p.\text{sum}\,(x + y)$

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and suppose $p_m = 0$ for all $m \geq n$. Then for any vectors $x, y \in E$, the sum of the change-of-origin series $p.\text{changeOrigin}\,x$ evaluated at $y$ equals the sum of the original series $p$ evaluated at $x + y$, i.e., $$(p.\text{changeOrigin}\,x).\text{sum}\,y = p.\text{sum}\,(x + y).$$

FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite theorem

 (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) :
  CPolynomialAt 𝕜 (p.changeOrigin · k) 0

Full source

/-- The terms of the formal multilinear series `p.changeOrigin` are continuously polynomial
as we vary the origin -/
theorem cpolynomialAt_changeOrigin_of_finite (p : FormalMultilinearSeries 𝕜 E F)
    {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) :
    CPolynomialAt 𝕜 (p.changeOrigin · k) 0 :=
  (p.hasFiniteFPowerSeriesOnBall_changeOrigin k fun _ h ↦ hn _ (le_self_add.trans h)).cpolynomialAt

Continuously Polynomial Property of Change-of-Origin Terms at Origin

Informal description

Let $p$ be a formal multilinear series from a normed space $E$ to $F$ over a field $\mathbb{K}$, and suppose $p_m = 0$ for all $m \geq n$. Then for any natural number $k$, the function $y \mapsto p.\text{changeOrigin}\,y\,k$ is continuously polynomial at the origin $0 \in E$.

HasFiniteFPowerSeriesOnBall.changeOrigin theorem

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

Full source

theorem HasFiniteFPowerSeriesOnBall.changeOrigin (hf : HasFiniteFPowerSeriesOnBall f p x n r)
    (h : (‖y‖₊ : ℝ≥0∞) < r) :
    HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - ‖y‖₊) where
  r_le := (tsub_le_tsub_right hf.r_le _).trans p.changeOrigin_radius
  r_pos := by simp [h]
  finite _ hm := p.changeOrigin_finite_of_finite hf.finite hm
  hasSum {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_of_finite hf.finite, add_assoc, hf.sum]
      exact mem_emetric_ball_zero_iff.2 ((enorm_add_le _ _).trans_lt hz)
    rw [this]
    apply (p.changeOrigin y).hasSum_of_finite fun _ => p.changeOrigin_finite_of_finite hf.finite

Finite Power Series Expansion under Change of Origin: $f$ has finite expansion at $x + y$ with radius $r - \|y\|$

Informal description

Let $f \colon E \to F$ be a function with a finite formal multilinear series expansion $p$ centered at $x \in E$ up to order $n$ on a ball of radius $r$. For any $y \in E$ with $\|y\| < r$, the function $f$ has a finite formal multilinear series expansion $p.\text{changeOrigin}\,y$ centered at $x + y$ up to order $n$ on the ball of radius $r - \|y\|$.

HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ EMetric.ball x r) : CPolynomialAt 𝕜 f y

Full source

/-- If a function admits a finite power series expansion `p` on an open ball `B (x, r)`, then
it is continuously polynomial at every point of this ball. -/
theorem HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem
    (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ EMetric.ball x r) :
    CPolynomialAt 𝕜 f y := by
  have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h
  have := hf.changeOrigin this
  rw [add_sub_cancel] at this
  exact this.cpolynomialAt

Continuously Polynomial Property at Points in Expansion Ball

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a finite power series expansion $p$ centered at $x \in E$ with bound $n$ on a ball of radius $r > 0$, meaning: 1. $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for all $y$ with $\|y\| < r$, 2. $p_m = 0$ for all $m \geq n$. Then for any point $y$ in the open ball $B(x, r)$, the function $f$ is continuously polynomial at $y$.

HasFiniteFPowerSeriesOnBall.cpolynomialOn theorem

(hf : HasFiniteFPowerSeriesOnBall f p x n r) : CPolynomialOn 𝕜 f (EMetric.ball x r)

Full source

theorem HasFiniteFPowerSeriesOnBall.cpolynomialOn (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    CPolynomialOn 𝕜 f (EMetric.ball x r) :=
  fun _y hy => hf.cpolynomialAt_of_mem hy

Finite Power Series Expansion Implies Continuously Polynomial on Ball

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a finite power series expansion $p$ centered at $x \in E$ with bound $n$ on a ball of radius $r > 0$, meaning: 1. $f(x + y) = \sum_{m=0}^\infty p_m(y, \ldots, y)$ for all $y$ with $\|y\| < r$, 2. $p_m = 0$ for all $m \geq n$. Then $f$ is continuously polynomial on the open ball $B(x, r)$, i.e., for every point $y \in B(x, r)$, the function $f$ is continuously polynomial at $y$.

isOpen_cpolynomialAt theorem

: IsOpen {x | CPolynomialAt 𝕜 f x}

Full source

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

Openness of the Continuously Polynomial Locus

Informal description

For any function $ f \colon E \to F $ between normed spaces over a field $\mathbb{K}$, the set of points $ x \in E $ where $ f $ is continuously polynomial is open.

CPolynomialAt.eventually_cpolynomialAt theorem

{f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∀ᶠ y in 𝓝 x, CPolynomialAt 𝕜 f y

Full source

theorem CPolynomialAt.eventually_cpolynomialAt {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) :
    ∀ᶠ y in 𝓝 x, CPolynomialAt 𝕜 f y :=
  (isOpen_cpolynomialAt 𝕜 f).mem_nhds h

Local persistence of continuously polynomial property

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is continuously polynomial at a point $x \in E$, then $f$ is continuously polynomial at all points $y$ in some neighborhood of $x$.

CPolynomialAt.exists_mem_nhds_cpolynomialOn theorem

{f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∃ s ∈ 𝓝 x, CPolynomialOn 𝕜 f s

Full source

theorem CPolynomialAt.exists_mem_nhds_cpolynomialOn {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) :
    ∃ s ∈ 𝓝 x, CPolynomialOn 𝕜 f s :=
  h.eventually_cpolynomialAt.exists_mem

Existence of a Neighborhood Where a Function is Continuously Polynomial

Informal description

Let $E$ and $F$ be normed spaces over a field $\mathbb{K}$, and let $f \colon E \to F$ be a function. If $f$ is continuously polynomial at a point $x \in E$, then there exists a neighborhood $s$ of $x$ such that $f$ is continuously polynomial on $s$.

CPolynomialAt.exists_ball_cpolynomialOn theorem

{f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∃ r : ℝ, 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r)

Full source

/-- If `f` is continuously polynomial at a point, then it is continuously polynomial in a
nonempty ball around that point. -/
theorem CPolynomialAt.exists_ball_cpolynomialOn {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) :
    ∃ r : ℝ, 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r) :=
  Metric.isOpen_iff.mp (isOpen_cpolynomialAt _ _) _ h

Existence of a Ball Where a Function is Continuously Polynomial

Informal description

Let $ E $ and $ F $ be normed spaces over a field $\mathbb{K}$, and let $ f \colon E \to F $ be a function. If $ f $ is continuously polynomial at a point $ x \in E $, then there exists a radius $ r > 0 $ such that $ f $ is continuously polynomial on the open ball $ B(x, r) $ centered at $ x $ with radius $ r $.

Main definitions