Properties of continuously polynomial functions #
We expand the API around continuously polynomial functions. Notably, we show that this class is stable under the usual operations (addition, subtraction, negation).
We also prove that continuous multilinear maps are continuously polynomial, and so are continuous linear maps into continuous multilinear maps. In particular, such maps are analytic.
theorem
hasFiniteFPowerSeriesOnBall_const
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{c : F}
{e : E}
:
HasFiniteFPowerSeriesOnBall (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e 1 ⊤
theorem
hasFiniteFPowerSeriesAt_const
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{c : F}
{e : E}
:
HasFiniteFPowerSeriesAt (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e 1
theorem
CPolynomialAt_const
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{v : F}
:
CPolynomialAt 𝕜 (fun (x : E) => v) x
theorem
CPolynomialOn_const
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{v : F}
{s : Set E}
:
CPolynomialOn 𝕜 (fun (x : E) => v) s
theorem
HasFiniteFPowerSeriesOnBall.add
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{pf pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
{n m : ℕ}
(hf : HasFiniteFPowerSeriesOnBall f pf x n r)
(hg : HasFiniteFPowerSeriesOnBall g pg x m r)
:
HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (n ⊔ m) r
theorem
HasFiniteFPowerSeriesAt.add
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{pf pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
{n m : ℕ}
(hf : HasFiniteFPowerSeriesAt f pf x n)
(hg : HasFiniteFPowerSeriesAt g pg x m)
:
HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (n ⊔ m)
theorem
CPolynomialAt.add
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{x : E}
(hf : CPolynomialAt 𝕜 f x)
(hg : CPolynomialAt 𝕜 g x)
:
CPolynomialAt 𝕜 (f + g) x
theorem
HasFiniteFPowerSeriesOnBall.neg
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
{n : ℕ}
(hf : HasFiniteFPowerSeriesOnBall f pf x n r)
:
HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r
theorem
HasFiniteFPowerSeriesAt.neg
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{x : E}
{n : ℕ}
(hf : HasFiniteFPowerSeriesAt f pf x n)
:
HasFiniteFPowerSeriesAt (-f) (-pf) x n
theorem
CPolynomialAt.neg
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
(hf : CPolynomialAt 𝕜 f x)
:
CPolynomialAt 𝕜 (-f) x
theorem
HasFiniteFPowerSeriesOnBall.sub
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{pf pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
{n m : ℕ}
(hf : HasFiniteFPowerSeriesOnBall f pf x n r)
(hg : HasFiniteFPowerSeriesOnBall g pg x m r)
:
HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (n ⊔ m) r
theorem
HasFiniteFPowerSeriesAt.sub
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{pf pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
{n m : ℕ}
(hf : HasFiniteFPowerSeriesAt f pf x n)
(hg : HasFiniteFPowerSeriesAt g pg x m)
:
HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (n ⊔ m)
theorem
CPolynomialAt.sub
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{x : E}
(hf : CPolynomialAt 𝕜 f x)
(hg : CPolynomialAt 𝕜 g x)
:
CPolynomialAt 𝕜 (f - g) x
theorem
CPolynomialOn.add
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{s : Set E}
(hf : CPolynomialOn 𝕜 f s)
(hg : CPolynomialOn 𝕜 g s)
:
CPolynomialOn 𝕜 (f + g) s
theorem
CPolynomialOn.sub
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{s : Set E}
(hf : CPolynomialOn 𝕜 f s)
(hg : CPolynomialOn 𝕜 g s)
:
CPolynomialOn 𝕜 (f - g) s
Continuous multilinear maps #
We show that continuous multilinear maps are continuously polynomial, and therefore analytic.
theorem
ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
:
HasFiniteFPowerSeriesOnBall (⇑f) f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤
theorem
ContinuousMultilinearMap.cpolynomialAt
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{x : (i : ι) → Em i}
:
CPolynomialAt 𝕜 (⇑f) x
theorem
ContinuousMultilinearMap.cpolynomialOn
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{s : Set ((i : ι) → Em i)}
:
CPolynomialOn 𝕜 (⇑f) s
@[deprecated ContinuousMultilinearMap.cpolynomialOn (since := "2025-02-15")]
theorem
ContinuousMultilinearMap.cpolyomialOn
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{s : Set ((i : ι) → Em i)}
:
CPolynomialOn 𝕜 (⇑f) s
Alias of ContinuousMultilinearMap.cpolynomialOn.
theorem
ContinuousMultilinearMap.analyticOnNhd
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{s : Set ((i : ι) → Em i)}
:
AnalyticOnNhd 𝕜 (⇑f) s
theorem
ContinuousMultilinearMap.analyticOn
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{s : Set ((i : ι) → Em i)}
:
AnalyticOn 𝕜 (⇑f) s
theorem
ContinuousMultilinearMap.analyticAt
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{x : (i : ι) → Em i}
:
AnalyticAt 𝕜 (⇑f) x
theorem
ContinuousMultilinearMap.analyticWithinAt
{𝕜 : Type u_1}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 Em F)
{x : (i : ι) → Em i}
{s : Set ((i : ι) → Em i)}
:
AnalyticWithinAt 𝕜 (⇑f) s x
Continuous linear maps into continuous multilinear maps #
We show that a continuous linear map into continuous multilinear maps is continuously polynomial (as a function of two variables, i.e., uncurried). Therefore, it is also analytic.
noncomputable def
ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
:
FormalMultilinearSeries 𝕜 (G × ((i : ι) → Em i)) F
Formal multilinear series associated to a linear map into multilinear maps.
Equations
- f.toFormalMultilinearSeriesOfMultilinear n = if h : Fintype.card (Option ι) = n then ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq h) f.continuousMultilinearMapOption else 0
Instances For
theorem
ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
:
HasFiniteFPowerSeriesOnBall (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) f.toFormalMultilinearSeriesOfMultilinear 0
(Fintype.card (Option ι) + 1) ⊤
theorem
ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
{x : G × ((i : ι) → Em i)}
:
CPolynomialAt 𝕜 (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) x
theorem
ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
{s : Set (G × ((i : ι) → Em i))}
:
CPolynomialOn 𝕜 (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) s
theorem
ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
{s : Set (G × ((i : ι) → Em i))}
:
AnalyticOnNhd 𝕜 (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) s
theorem
ContinuousLinearMap.analyticOn_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
{s : Set (G × ((i : ι) → Em i))}
:
AnalyticOn 𝕜 (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) s
theorem
ContinuousLinearMap.analyticAt_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
{x : G × ((i : ι) → Em i)}
:
AnalyticAt 𝕜 (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) x
theorem
ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[Fintype ι]
(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
{s : Set (G × ((i : ι) → Em i))}
{x : G × ((i : ι) → Em i)}
:
AnalyticWithinAt 𝕜 (fun (p : G × ((i : ι) → Em i)) => (f p.1) p.2) s x