# 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.

source
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 ⊤
source
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
source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
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
source
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
source
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)
source
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
source
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
source
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.

source
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) ⊤
source
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
source
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
source
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
source
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
source
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
source
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.

source
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

source
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) ⊤
source
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
source
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
source
@[deprecated ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear (since := "2025-09-15")]
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

Alias of `ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear`.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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