Mathlib.Analysis.Analytic.CPolynomial

hasFiniteFPowerSeriesOnBall_const theorem

{c : F} {e : E} : HasFiniteFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e 1 ⊤

Full source

theorem hasFiniteFPowerSeriesOnBall_const {c : F} {e : E} :
    HasFiniteFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e 1 ⊤ :=
  ⟨hasFPowerSeriesOnBall_const, fun n hn ↦ constFormalMultilinearSeries_apply (id hn : 0 < n).ne'⟩

Finite Power Series Expansion of Constant Function on Entire Space

Informal description

For any constant function $f(x) = c$ where $c \in F$, the formal multilinear series associated with $f$ is the constant formal multilinear series $\text{constFormalMultilinearSeries}_{\mathbb{K}}(E, c)$. This series has a finite power series expansion on the entire space (represented by the ball of radius 1 centered at any point $e \in E$ with the trivial filter $\top$).

hasFiniteFPowerSeriesAt_const theorem

{c : F} {e : E} : HasFiniteFPowerSeriesAt (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e 1

Full source

theorem hasFiniteFPowerSeriesAt_const {c : F} {e : E} :
    HasFiniteFPowerSeriesAt (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e 1 :=
  ⟨⊤, hasFiniteFPowerSeriesOnBall_const⟩

Finite Power Series Expansion of Constant Function at Point with Radius 1

Informal description

For any constant function $f(x) = c$ where $c \in F$ and any point $e \in E$, the function $f$ has a finite power series expansion at $e$ with radius of convergence at least 1, represented by the constant formal multilinear series $\text{constFormalMultilinearSeries}_{\mathbb{K}}(E, c)$.

CPolynomialAt_const theorem

{v : F} : CPolynomialAt 𝕜 (fun _ => v) x

Full source

theorem CPolynomialAt_const {v : F} : CPolynomialAt 𝕜 (fun _ => v) x :=
  ⟨constFormalMultilinearSeries 𝕜 E v, 1, hasFiniteFPowerSeriesAt_const⟩

Constant Functions are Continuously Polynomial at Every Point

Informal description

For any constant function $f(x) = v$ where $v \in F$, the function $f$ is continuously polynomial at every point $x \in E$.

CPolynomialOn_const theorem

{v : F} {s : Set E} : CPolynomialOn 𝕜 (fun _ => v) s

Full source

theorem CPolynomialOn_const {v : F} {s : Set E} : CPolynomialOn 𝕜 (fun _ => v) s :=
  fun _ _ => CPolynomialAt_const

Constant Functions are Continuously Polynomial on Any Subset

Informal description

For any constant function $f(x) = v$ where $v \in F$ and any subset $s \subseteq E$, the function $f$ is continuously polynomial on $s$.

HasFiniteFPowerSeriesOnBall.add theorem

 (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
  HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r

Full source

theorem HasFiniteFPowerSeriesOnBall.add (hf : HasFiniteFPowerSeriesOnBall f pf x n r)
    (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
    HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r :=
  ⟨hf.1.add hg.1, fun N hN ↦ by
    rw [Pi.add_apply, hf.finite _ ((le_max_left n m).trans hN),
        hg.finite _ ((le_max_right n m).trans hN), zero_add]⟩

Sum of Finite Formal Power Series Expansions on a Ball

Informal description

Let $f$ and $g$ be functions with finite formal power series expansions on a ball centered at $x$ with radius $r$, represented by $pf$ and $pg$ with degrees $n$ and $m$ respectively. Then the sum $f + g$ has a finite formal power series expansion on the same ball, represented by $pf + pg$ with degree $\max(n, m)$.

HasFiniteFPowerSeriesAt.add theorem

 (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :
  HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

Full source

theorem HasFiniteFPowerSeriesAt.add (hf : HasFiniteFPowerSeriesAt f pf x n)
    (hg : HasFiniteFPowerSeriesAt g pg x m) :
    HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m) := by
  rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
  exact ⟨r, hr.1.add hr.2⟩

Sum of Finite Formal Power Series Expansions at a Point

Informal description

Let $f$ and $g$ be functions with finite formal power series expansions at a point $x$, represented by $pf$ and $pg$ with degrees $n$ and $m$ respectively. Then the sum $f + g$ has a finite formal power series expansion at $x$, represented by $pf + pg$ with degree $\max(n, m)$.

CPolynomialAt.add theorem

(hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) : CPolynomialAt 𝕜 (f + g) x

Full source

theorem CPolynomialAt.add (hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) :
    CPolynomialAt 𝕜 (f + g) x :=
  let ⟨_, _, hpf⟩ := hf
  let ⟨_, _, hqf⟩ := hg
  (hpf.add hqf).cpolynomialAt

Sum of Continuously Polynomial Functions at a Point is Continuously Polynomial

Informal description

Let $f$ and $g$ be functions that are continuously polynomial at a point $x$ over a field $\mathbb{K}$. Then the sum $f + g$ is also continuously polynomial at $x$ over $\mathbb{K}$.

HasFiniteFPowerSeriesOnBall.neg theorem

(hf : HasFiniteFPowerSeriesOnBall f pf x n r) : HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r

Full source

theorem HasFiniteFPowerSeriesOnBall.neg (hf : HasFiniteFPowerSeriesOnBall f pf x n r) :
    HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r :=
  ⟨hf.1.neg, fun m hm ↦ by rw [Pi.neg_apply, hf.finite m hm, neg_zero]⟩

Negation Preserves Finite Formal Power Series Expansion on a Ball

Informal description

Let $f$ be a function defined on a ball centered at $x$ with radius $r$, admitting a finite formal power series expansion $pf$ at $x$ of order $n$. Then the negation of $f$, denoted $-f$, also admits a finite formal power series expansion $-pf$ at $x$ of the same order $n$ on the same ball.

HasFiniteFPowerSeriesAt.neg theorem

(hf : HasFiniteFPowerSeriesAt f pf x n) : HasFiniteFPowerSeriesAt (-f) (-pf) x n

Full source

theorem HasFiniteFPowerSeriesAt.neg (hf : HasFiniteFPowerSeriesAt f pf x n) :
    HasFiniteFPowerSeriesAt (-f) (-pf) x n :=
  let ⟨_, hrf⟩ := hf
  hrf.neg.hasFiniteFPowerSeriesAt

Negation Preserves Finite Formal Power Series Expansion at a Point

Informal description

Let $f$ be a function admitting a finite formal power series expansion $pf$ at a point $x$ of order $n$. Then the negation of $f$, denoted $-f$, also admits a finite formal power series expansion $-pf$ at $x$ of the same order $n$.

CPolynomialAt.neg theorem

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

Full source

theorem CPolynomialAt.neg (hf : CPolynomialAt 𝕜 f x) : CPolynomialAt 𝕜 (-f) x :=
  let ⟨_, _, hpf⟩ := hf
  hpf.neg.cpolynomialAt

Negation preserves continuous polynomiality at a point

Informal description

Let $\mathbb{K}$ be a field, $f$ a function, and $x$ a point such that $f$ is continuously polynomial at $x$ over $\mathbb{K}$. Then the negation of $f$, $-f$, is also continuously polynomial at $x$ over $\mathbb{K}$.

HasFiniteFPowerSeriesOnBall.sub theorem

 (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
  HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r

Full source

theorem HasFiniteFPowerSeriesOnBall.sub (hf : HasFiniteFPowerSeriesOnBall f pf x n r)
    (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
    HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Finite Formal Power Series Expansions on a Ball

Informal description

Let $f$ and $g$ be functions with finite formal power series expansions on a ball centered at $x$ with radius $r$, represented by $pf$ and $pg$ with degrees $n$ and $m$ respectively. Then the difference $f - g$ has a finite formal power series expansion on the same ball, represented by $pf - pg$ with degree $\max(n, m)$.

HasFiniteFPowerSeriesAt.sub theorem

 (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :
  HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)

Full source

theorem HasFiniteFPowerSeriesAt.sub (hf : HasFiniteFPowerSeriesAt f pf x n)
    (hg : HasFiniteFPowerSeriesAt g pg x m) :
    HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m) := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Finite Formal Power Series Expansions at a Point

Informal description

Let $f$ and $g$ be functions with finite formal power series expansions at a point $x$, represented by $pf$ and $pg$ with degrees $n$ and $m$ respectively. Then the difference $f - g$ has a finite formal power series expansion at $x$, represented by $pf - pg$ with degree $\max(n, m)$.

CPolynomialAt.sub theorem

(hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) : CPolynomialAt 𝕜 (f - g) x

Full source

theorem CPolynomialAt.sub (hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) :
    CPolynomialAt 𝕜 (f - g) x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Continuously Polynomial Functions at a Point is Continuously Polynomial

Informal description

Let $\mathbb{K}$ be a field, and let $f$ and $g$ be functions that are continuously polynomial at a point $x$ over $\mathbb{K}$. Then the difference $f - g$ is also continuously polynomial at $x$ over $\mathbb{K}$.

CPolynomialOn.add theorem

{s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : CPolynomialOn 𝕜 g s) : CPolynomialOn 𝕜 (f + g) s

Full source

theorem CPolynomialOn.add {s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : CPolynomialOn 𝕜 g s) :
    CPolynomialOn 𝕜 (f + g) s :=
  fun z hz => (hf z hz).add (hg z hz)

Sum of Continuously Polynomial Functions on a Set is Continuously Polynomial

Informal description

Let $f$ and $g$ be functions defined on a set $s \subseteq E$ that are continuously polynomial over a field $\mathbb{K}$ on $s$. Then the sum $f + g$ is also continuously polynomial over $\mathbb{K}$ on $s$.

CPolynomialOn.sub theorem

{s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : CPolynomialOn 𝕜 g s) : CPolynomialOn 𝕜 (f - g) s

Full source

theorem CPolynomialOn.sub {s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : CPolynomialOn 𝕜 g s) :
    CPolynomialOn 𝕜 (f - g) s :=
  fun z hz => (hf z hz).sub (hg z hz)

Difference of Continuously Polynomial Functions on a Set is Continuously Polynomial

Informal description

Let $\mathbb{K}$ be a field, $E$ be a vector space over $\mathbb{K}$, and $s \subseteq E$ be a subset. If $f$ and $g$ are functions that are continuously polynomial on $s$ over $\mathbb{K}$, then their difference $f - g$ is also continuously polynomial on $s$ over $\mathbb{K}$.

ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall theorem

: HasFiniteFPowerSeriesOnBall f f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤

Full source

protected theorem hasFiniteFPowerSeriesOnBall :
    HasFiniteFPowerSeriesOnBall f f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤ :=
  .mk' (fun _ hm ↦ dif_neg (Nat.succ_le_iff.mp hm).ne) ENNReal.zero_lt_top fun y _ ↦ by
    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
    · rw [toFormalMultilinearSeries, dif_pos rfl]; rfl
    · intro m _ ne; rw [toFormalMultilinearSeries, dif_neg ne.symm]; rfl

Finite Formal Power Series Expansion of Continuous Multilinear Maps

Informal description

Let $f$ be a continuous multilinear map. Then $f$ has a finite formal power series expansion on the entire space, represented by its associated formal multilinear series $f.\text{toFormalMultilinearSeries}$, centered at $0$ with radius of convergence at least $\text{card}(\iota) + 1$, where $\iota$ is the indexing type of the multilinear map.

ContinuousMultilinearMap.cpolynomialAt theorem

: CPolynomialAt 𝕜 f x

Full source

lemma cpolynomialAt  : CPolynomialAt 𝕜 f x :=
  f.hasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem
    (by simp only [Metric.emetric_ball_top, Set.mem_univ])

Continuous Multilinear Maps are Locally Continuously Polynomial

Informal description

For any continuous multilinear map $f$ over a field $\mathbb{K}$ and any point $x$ in its domain, $f$ is continuously polynomial at $x$.

ContinuousMultilinearMap.cpolynomialOn theorem

: CPolynomialOn 𝕜 f s

Full source

lemma cpolynomialOn : CPolynomialOn 𝕜 f s := fun _ _ ↦ f.cpolynomialAt

Continuous Multilinear Maps are Continuously Polynomial on Subsets

Informal description

For any continuous multilinear map $f$ over a field $\mathbb{K}$ and any subset $s$ of its domain, $f$ is continuously polynomial on $s$.

ContinuousMultilinearMap.analyticOnNhd theorem

: AnalyticOnNhd 𝕜 f s

Full source

lemma analyticOnNhd : AnalyticOnNhd 𝕜 f s := f.cpolynomialOn.analyticOnNhd

Continuous Multilinear Maps are Analytic on Neighborhoods of Subsets

Informal description

For any continuous multilinear map $f$ over a field $\mathbb{K}$ and any subset $s$ of its domain, $f$ is analytic on a neighborhood of $s$.

ContinuousMultilinearMap.analyticOn theorem

: AnalyticOn 𝕜 f s

Full source

lemma analyticOn : AnalyticOn 𝕜 f s := f.analyticOnNhd.analyticOn

Analyticity of Continuous Multilinear Maps on Subsets

Informal description

For any continuous multilinear map $f$ over a field $\mathbb{K}$ and any subset $s$ of its domain, $f$ is analytic on $s$.

ContinuousMultilinearMap.analyticAt theorem

: AnalyticAt 𝕜 f x

Full source

lemma analyticAt : AnalyticAt 𝕜 f x := f.cpolynomialAt.analyticAt

Continuous Multilinear Maps are Analytic at Every Point

Informal description

For any continuous multilinear map $f$ over a field $\mathbb{K}$ and any point $x$ in its domain, $f$ is analytic at $x$.

ContinuousMultilinearMap.analyticWithinAt theorem

: AnalyticWithinAt 𝕜 f s x

Full source

lemma analyticWithinAt : AnalyticWithinAt 𝕜 f s x := f.analyticAt.analyticWithinAt

Analyticity of Continuous Multilinear Maps Within a Subset at a Point

Informal description

For any continuous multilinear map $f$ over a field $\mathbb{K}$, any subset $s$ of its domain, and any point $x \in s$, the function $f$ is analytic at $x$ within $s$.

ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear definition

: FormalMultilinearSeries 𝕜 (G × (Π i, Em i)) F

Full source

/-- Formal multilinear series associated to a linear map into multilinear maps. -/
noncomputable def toFormalMultilinearSeriesOfMultilinear :
    FormalMultilinearSeries 𝕜 (G × (Π i, Em i)) F :=
  fun n ↦ if h : Fintype.card (Option ι) = n then
    (f.continuousMultilinearMapOption).domDomCongr (Fintype.equivFinOfCardEq h)
  else 0

Formal multilinear series of a linear map into multilinear maps

Informal description

The formal multilinear series associated to a continuous linear map $ f $ from $ G $ to continuous multilinear maps on $ \Pi_i E_i $ is defined as follows: for each degree $ n $, if $ n $ equals the cardinality of $ \text{Option} \iota $ (where $ \iota $ indexes the family $ E_i $), then the $ n $-th term of the series is obtained by reindexing the domain of $ f $ using the equivalence induced by the equality of cardinalities; otherwise, the term is zero.

ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear theorem

 :
  HasFiniteFPowerSeriesOnBall (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) f.toFormalMultilinearSeriesOfMultilinear 0
    (Fintype.card (Option ι) + 1) ⊤

Full source

protected theorem hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear :
    HasFiniteFPowerSeriesOnBall (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2)
      f.toFormalMultilinearSeriesOfMultilinear 0 (Fintype.card (Option ι) + 1) ⊤ := by
  apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top  ?_
  · intro m hm
    apply dif_neg
    exact Nat.ne_of_lt hm
  · intro y _
    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
    · rw [toFormalMultilinearSeriesOfMultilinear, dif_pos rfl]; rfl
    · intro m _ ne; rw [toFormalMultilinearSeriesOfMultilinear, dif_neg ne.symm]; rfl

Finite Power Series Expansion of Uncurried Linear-Multilinear Map

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed spaces over a field $\mathbb{K}$, and let $F$ be another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ has a finite formal power series expansion centered at $0$ with radius of convergence $\infty$. The degree of this power series is at most $\text{card}(\text{Option } \iota) + 1$, where $\text{Option } \iota$ is the indexing set $\iota$ extended by one element.

ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear theorem

: CPolynomialAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x

Full source

lemma cpolynomialAt_uncurry_of_multilinear :
    CPolynomialAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
  f.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear.cpolynomialAt_of_mem
    (by simp only [Metric.emetric_ball_top, Set.mem_univ])

Continuous Polynomiality of Uncurried Linear-Multilinear Maps

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed spaces over a field $\mathbb{K}$, and let $F$ be another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ is continuously polynomial at every point $x \in G \times (\Pi_{i \in \iota} E_i)$.

ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear theorem

: CPolynomialOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s

Full source

lemma cpolyomialOn_uncurry_of_multilinear :
    CPolynomialOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
  fun _ _ ↦ f.cpolynomialAt_uncurry_of_multilinear

Continuous Polynomiality of Uncurried Linear-Multilinear Maps on Subsets

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed spaces over a field $\mathbb{K}$, and let $F$ be another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ is continuously polynomial on any subset $s \subseteq G \times (\Pi_{i \in \iota} E_i)$.

ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear theorem

: AnalyticOnNhd 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s

Full source

lemma analyticOnNhd_uncurry_of_multilinear :
    AnalyticOnNhd 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
  f.cpolyomialOn_uncurry_of_multilinear.analyticOnNhd

Analyticity of Uncurried Linear-Multilinear Maps on Neighborhoods of Subsets

Informal description

Let $\mathbb{K}$ be a field, $G$ and $E_i$ (for $i \in \iota$) be normed spaces over $\mathbb{K}$, and $F$ another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ is analytic on a neighborhood of any subset $s \subseteq G \times (\Pi_{i \in \iota} E_i)$.

ContinuousLinearMap.analyticOn_uncurry_of_multilinear theorem

: AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s

Full source

lemma analyticOn_uncurry_of_multilinear :
    AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
  f.analyticOnNhd_uncurry_of_multilinear.analyticOn

Analyticity of Uncurried Linear-Multilinear Maps on Subsets

Informal description

Let $\mathbb{K}$ be a field, $G$ and $E_i$ (for $i \in \iota$) be normed spaces over $\mathbb{K}$, and $F$ another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ is analytic on any subset $s \subseteq G \times (\Pi_{i \in \iota} E_i)$.

ContinuousLinearMap.analyticAt_uncurry_of_multilinear theorem

: AnalyticAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x

Full source

lemma analyticAt_uncurry_of_multilinear : AnalyticAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
  f.cpolynomialAt_uncurry_of_multilinear.analyticAt

Analyticity of Uncurried Linear-Multilinear Maps at a Point

Informal description

Let $\mathbb{K}$ be a field, $G$ and $E_i$ (for $i \in \iota$) be normed spaces over $\mathbb{K}$, and $F$ another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ is analytic at every point $x \in G \times (\Pi_{i \in \iota} E_i)$.

ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear theorem

: AnalyticWithinAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s x

Full source

lemma analyticWithinAt_uncurry_of_multilinear :
    AnalyticWithinAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s x :=
  f.analyticAt_uncurry_of_multilinear.analyticWithinAt

Analyticity Within a Set of Uncurried Linear-Multilinear Maps at a Point

Informal description

Let $\mathbb{K}$ be a field, $G$ and $E_i$ (for $i \in \iota$) be normed spaces over $\mathbb{K}$, and $F$ another normed space. Given a continuous linear map $f \colon G \to \text{ContinuousMultilinearMap}(\mathbb{K}, (E_i)_{i \in \iota}, F)$, the uncurried function $(g, (e_i)_{i \in \iota}) \mapsto f(g)((e_i)_{i \in \iota})$ is analytic at the point $x \in G \times (\Pi_{i \in \iota} E_i)$ within the set $s \subseteq G \times (\Pi_{i \in \iota} E_i)$.