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]
{s : Set E}
{v : F}
:
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 (max 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 (max 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
CPolynomialAt.fun_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 𝕜 (fun (i : E) => f i + g i) x
Eta-expanded form of CPolynomialAt.add
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
CPolynomialAt.fun_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 𝕜 (fun (i : E) => -f i) x
Eta-expanded form of CPolynomialAt.neg
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 (max 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 (max 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
CPolynomialAt.fun_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 𝕜 (fun (i : E) => f i - g i) x
Eta-expanded form of CPolynomialAt.sub
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.fun_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 𝕜 (fun (i : E) => f i + g i) s
Eta-expanded form of CPolynomialOn.add
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
theorem
CPolynomialOn.fun_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 𝕜 (fun (i : E) => f i - g i) s
Eta-expanded form of CPolynomialOn.sub
theorem
CPolynomialAt.smul
{𝕜 : 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)
(c : 𝕜)
:
CPolynomialAt 𝕜 (c • f) x
theorem
CPolynomialAt.fun_smul
{𝕜 : 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)
(c : 𝕜)
:
CPolynomialAt 𝕜 (fun (i : E) => c • f i) x
Eta-expanded form of CPolynomialAt.smul
theorem
CPolynomialOn.smul
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
(hf : CPolynomialOn 𝕜 f s)
(c : 𝕜)
:
CPolynomialOn 𝕜 (c • f) s
theorem
CPolynomialOn.fun_smul
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
(hf : CPolynomialOn 𝕜 f s)
(c : 𝕜)
:
CPolynomialOn 𝕜 (fun (i : E) => c • f i) s
Eta-expanded form of CPolynomialOn.smul
theorem
HasFiniteFPowerSeriesOnBall.prodMk
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
{n m : ℕ}
{g : E → G}
{pg : FormalMultilinearSeries 𝕜 E G}
(hf : HasFiniteFPowerSeriesOnBall f pf x n r)
(hg : HasFiniteFPowerSeriesOnBall g pg x m r)
:
theorem
HasFiniteFPowerSeriesAt.prodMk
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{x : E}
{n m : ℕ}
{g : E → G}
{pg : FormalMultilinearSeries 𝕜 E G}
(hf : HasFiniteFPowerSeriesAt f pf x n)
(hg : HasFiniteFPowerSeriesAt g pg x m)
:
theorem
CPolynomialAt.prodMk
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{x : E}
{g : E → G}
(hf : CPolynomialAt 𝕜 f x)
(hg : CPolynomialAt 𝕜 g x)
:
CPolynomialAt 𝕜 (fun (x : E) => (f x, g x)) x
theorem
CPolynomialOn.prodMk
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{s : Set E}
{g : E → G}
(hf : CPolynomialOn 𝕜 f s)
(hg : CPolynomialOn 𝕜 g s)
:
CPolynomialOn 𝕜 (fun (x : E) => (f x, g x)) 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
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
theorem
ContinuousAlternatingMap.cpolynomialAt
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
(f : E [⋀^ι]→L[𝕜] F)
{x : ι → E}
:
CPolynomialAt 𝕜 (⇑f) x
theorem
ContinuousAlternatingMap.cpolynomialOn
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
(f : E [⋀^ι]→L[𝕜] F)
{s : Set (ι → E)}
:
CPolynomialOn 𝕜 (⇑f) s
theorem
ContinuousAlternatingMap.analyticOnNhd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
(f : E [⋀^ι]→L[𝕜] F)
{s : Set (ι → E)}
:
AnalyticOnNhd 𝕜 (⇑f) s
theorem
ContinuousAlternatingMap.analyticOn
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
(f : E [⋀^ι]→L[𝕜] F)
{s : Set (ι → E)}
:
AnalyticOn 𝕜 (⇑f) s
theorem
ContinuousAlternatingMap.analyticAt
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
(f : E [⋀^ι]→L[𝕜] F)
{x : ι → E}
:
AnalyticAt 𝕜 (⇑f) x
theorem
ContinuousAlternatingMap.analyticWithinAt
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
(f : E [⋀^ι]→L[𝕜] F)
{x : ι → E}
{s : Set (ι → E)}
:
AnalyticWithinAt 𝕜 (⇑f) s x
theorem
ContinuousAlternatingMap.cpolynomialAt_smul_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
(f₀ : E →L[𝕜] F)
:
Precomposition on spaces of n-alternating maps, as a continuous linear map, is continuously
polynomial when multiplied by (card ι)!.
theorem
ContinuousAlternatingMap.cpolynomialAt_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
[CharZero 𝕜]
(f₀ : E →L[𝕜] F)
:
Precomposition on spaces of n-alternating maps, as a continuous linear map, is continuously
polynomial.
theorem
ContinuousAlternatingMap.cpolynomialOn_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
[CharZero 𝕜]
(s : Set (E →L[𝕜] F))
:
Precomposition on spaces of n-alternating maps, as a continuous linear map, is cpolynomial.
theorem
ContinuousAlternatingMap.analyticOnNhd_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
[CharZero 𝕜]
(s : Set (E →L[𝕜] F))
:
theorem
ContinuousAlternatingMap.analyticOn_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
[CharZero 𝕜]
(s : Set (E →L[𝕜] F))
:
theorem
ContinuousAlternatingMap.analyticAt_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
[CharZero 𝕜]
(f₀ : E →L[𝕜] F)
:
theorem
ContinuousAlternatingMap.analyticWithinAt_compContinuousLinearMapCLM
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
[Fintype ι]
[CharZero 𝕜]
(s : Set (E →L[𝕜] F))
(f₀ : E →L[𝕜] F)
:
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.cpolynomialOn_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
theorem
ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{x : ((i : ι) → Em i) × G}
:
CPolynomialAt 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) x
theorem
ContinuousMultilinearMap.cpolynomialOn_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{s : Set (((i : ι) → Em i) × G)}
:
CPolynomialOn 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) s
@[deprecated ContinuousMultilinearMap.cpolynomialOn_uncurry_of_linear (since := "2026-09-17")]
theorem
ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{s : Set (((i : ι) → Em i) × G)}
:
CPolynomialOn 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) s
Alias of ContinuousMultilinearMap.cpolynomialOn_uncurry_of_linear.
theorem
ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{s : Set (((i : ι) → Em i) × G)}
:
AnalyticOnNhd 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) s
theorem
ContinuousMultilinearMap.analyticOn_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{s : Set (((i : ι) → Em i) × G)}
:
AnalyticOn 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) s
theorem
ContinuousMultilinearMap.analyticAt_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{x : ((i : ι) → Em i) × G}
:
AnalyticAt 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) x
theorem
ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear
{𝕜 : 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 : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F))
{s : Set (((i : ι) → Em i) × G)}
{x : ((i : ι) → Em i) × G}
:
AnalyticWithinAt 𝕜 (fun (p : ((i : ι) → Em i) × G) => (f p.1) p.2) s x
theorem
ContinuousMultilinearMap.cpolynomialAt_apply
{𝕜 : 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 × ((i : ι) → Em i)}
:
CPolynomialAt 𝕜 (fun (p : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)) => p.1 p.2) f
theorem
ContinuousMultilinearMap.cpolynomialOn_apply
{𝕜 : 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 ι]
{s : Set (ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i))}
:
CPolynomialOn 𝕜 (fun (p : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)) => p.1 p.2) s
theorem
ContinuousMultilinearMap.analyticOnNhd_apply
{𝕜 : 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 ι]
{s : Set (ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i))}
:
AnalyticOnNhd 𝕜 (fun (p : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)) => p.1 p.2) s
theorem
ContinuousMultilinearMap.analyticOn_apply
{𝕜 : 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 ι]
{s : Set (ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i))}
:
AnalyticOn 𝕜 (fun (p : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)) => p.1 p.2) s
theorem
ContinuousMultilinearMap.analyticAt_apply
{𝕜 : 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 × ((i : ι) → Em i)}
:
AnalyticAt 𝕜 (fun (p : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)) => p.1 p.2) f
theorem
ContinuousMultilinearMap.analyticWithinAt_apply
{𝕜 : 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 ι]
{s : Set (ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i))}
{f : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)}
:
AnalyticWithinAt 𝕜 (fun (p : ContinuousMultilinearMap 𝕜 Em F × ((i : ι) → Em i)) => p.1 p.2) s f
theorem
ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap
{𝕜 : Type u_1}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
{Fm : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
[Fintype ι]
{q : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G}
:
CPolynomialAt 𝕜
(fun (p : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G) => p.2.compContinuousLinearMap p.1) q
theorem
ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap
{𝕜 : Type u_1}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
{Fm : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
[Fintype ι]
{t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)}
:
CPolynomialOn 𝕜
(fun (p : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G) => p.2.compContinuousLinearMap p.1) t
theorem
ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap
{𝕜 : Type u_1}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
{Fm : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
[Fintype ι]
{t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)}
:
AnalyticOnNhd 𝕜
(fun (p : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G) => p.2.compContinuousLinearMap p.1) t
theorem
ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap
{𝕜 : Type u_1}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
{Fm : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
[Fintype ι]
{t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)}
:
AnalyticOn 𝕜
(fun (p : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G) => p.2.compContinuousLinearMap p.1) t
theorem
ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap
{𝕜 : Type u_1}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
{Fm : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
[Fintype ι]
{q : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G}
:
AnalyticAt 𝕜
(fun (p : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G) => p.2.compContinuousLinearMap p.1) q
theorem
ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap
{𝕜 : Type u_1}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{ι : Type u_5}
{Em : ι → Type u_6}
{Fm : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (Em i)]
[(i : ι) → NormedSpace 𝕜 (Em i)]
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
[Fintype ι]
{t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)}
{q : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G}
:
AnalyticWithinAt 𝕜
(fun (p : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G) => p.2.compContinuousLinearMap p.1) t q
theorem
ContinuousAlternatingMap.cpolynomialAt_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
{f : E [⋀^ι]→L[𝕜] F × (ι → E)}
:
CPolynomialAt 𝕜 (fun (p : E [⋀^ι]→L[𝕜] F × (ι → E)) => p.1 p.2) f
theorem
ContinuousAlternatingMap.cpolynomialOn_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
{s : Set (E [⋀^ι]→L[𝕜] F × (ι → E))}
:
CPolynomialOn 𝕜 (fun (p : E [⋀^ι]→L[𝕜] F × (ι → E)) => p.1 p.2) s
theorem
ContinuousAlternatingMap.analyticOnNhd_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
{s : Set (E [⋀^ι]→L[𝕜] F × (ι → E))}
:
AnalyticOnNhd 𝕜 (fun (p : E [⋀^ι]→L[𝕜] F × (ι → E)) => p.1 p.2) s
theorem
ContinuousAlternatingMap.analyticOn_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
{s : Set (E [⋀^ι]→L[𝕜] F × (ι → E))}
:
AnalyticOn 𝕜 (fun (p : E [⋀^ι]→L[𝕜] F × (ι → E)) => p.1 p.2) s
theorem
ContinuousAlternatingMap.analyticAt_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
{f : E [⋀^ι]→L[𝕜] F × (ι → E)}
:
AnalyticAt 𝕜 (fun (p : E [⋀^ι]→L[𝕜] F × (ι → E)) => p.1 p.2) f
theorem
ContinuousAlternatingMap.analyticWithinAt_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_5}
[Fintype ι]
{f : E [⋀^ι]→L[𝕜] F × (ι → E)}
{s : Set (E [⋀^ι]→L[𝕜] F × (ι → E))}
:
AnalyticWithinAt 𝕜 (fun (p : E [⋀^ι]→L[𝕜] F × (ι → E)) => p.1 p.2) s f