Various ways to combine analytic functions #
We show that the following are analytic:
- Cartesian products of analytic functions
- Arithmetic on analytic functions:
mul,smul,inv,div - Finite sums and products:
Finset.sum,Finset.prod
Constants are analytic #
theorem
hasFPowerSeriesOnBall_const
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{c : F}
{e : E}
:
HasFPowerSeriesOnBall (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤
theorem
hasFPowerSeriesAt_const
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{c : F}
{e : E}
:
HasFPowerSeriesAt (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e
theorem
analyticAt_const
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{v : F}
{x : E}
:
AnalyticAt 𝕜 (fun (x : E) => v) x
theorem
analyticOn_const
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{v : F}
{s : Set E}
:
AnalyticOn 𝕜 (fun (x : E) => v) s
theorem
analyticWithinAt_const
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{v : F}
{s : Set E}
{x : E}
:
AnalyticWithinAt 𝕜 (fun (x : E) => v) s x
theorem
analyticWithinOn_const
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{v : F}
{s : Set E}
:
AnalyticWithinOn 𝕜 (fun (x : E) => v) s
Addition, negation, subtraction #
theorem
HasFPowerSeriesWithinOnBall.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{s : Set E}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesWithinOnBall f pf s x r)
(hg : HasFPowerSeriesWithinOnBall g pg s x r)
:
HasFPowerSeriesWithinOnBall (f + g) (pf + pg) s x r
theorem
HasFPowerSeriesOnBall.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesOnBall f pf x r)
(hg : HasFPowerSeriesOnBall g pg x r)
:
HasFPowerSeriesOnBall (f + g) (pf + pg) x r
theorem
HasFPowerSeriesWithinAt.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{s : Set E}
{x : E}
(hf : HasFPowerSeriesWithinAt f pf s x)
(hg : HasFPowerSeriesWithinAt g pg s x)
:
HasFPowerSeriesWithinAt (f + g) (pf + pg) s x
theorem
HasFPowerSeriesAt.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
(hf : HasFPowerSeriesAt f pf x)
(hg : HasFPowerSeriesAt g pg x)
:
HasFPowerSeriesAt (f + g) (pf + pg) x
theorem
AnalyticWithinAt.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{s : Set E}
{x : E}
(hf : AnalyticWithinAt 𝕜 f s x)
(hg : AnalyticWithinAt 𝕜 g s x)
:
AnalyticWithinAt 𝕜 (f + g) s x
theorem
AnalyticAt.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
(hg : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (f + g) x
theorem
HasFPowerSeriesWithinOnBall.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{s : Set E}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesWithinOnBall f pf s x r)
:
HasFPowerSeriesWithinOnBall (-f) (-pf) s x r
theorem
HasFPowerSeriesOnBall.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesOnBall f pf x r)
:
HasFPowerSeriesOnBall (-f) (-pf) x r
theorem
HasFPowerSeriesWithinAt.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{s : Set E}
{x : E}
(hf : HasFPowerSeriesWithinAt f pf s x)
:
HasFPowerSeriesWithinAt (-f) (-pf) s x
theorem
HasFPowerSeriesAt.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{x : E}
(hf : HasFPowerSeriesAt f pf x)
:
HasFPowerSeriesAt (-f) (-pf) x
theorem
AnalyticWithinAt.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
{x : E}
(hf : AnalyticWithinAt 𝕜 f s x)
:
AnalyticWithinAt 𝕜 (-f) s x
theorem
AnalyticAt.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
:
AnalyticAt 𝕜 (-f) x
theorem
HasFPowerSeriesWithinOnBall.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{s : Set E}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesWithinOnBall f pf s x r)
(hg : HasFPowerSeriesWithinOnBall g pg s x r)
:
HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r
theorem
HasFPowerSeriesOnBall.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesOnBall f pf x r)
(hg : HasFPowerSeriesOnBall g pg x r)
:
HasFPowerSeriesOnBall (f - g) (pf - pg) x r
theorem
HasFPowerSeriesWithinAt.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{s : Set E}
{x : E}
(hf : HasFPowerSeriesWithinAt f pf s x)
(hg : HasFPowerSeriesWithinAt g pg s x)
:
HasFPowerSeriesWithinAt (f - g) (pf - pg) s x
theorem
HasFPowerSeriesAt.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{pf : FormalMultilinearSeries 𝕜 E F}
{pg : FormalMultilinearSeries 𝕜 E F}
{x : E}
(hf : HasFPowerSeriesAt f pf x)
(hg : HasFPowerSeriesAt g pg x)
:
HasFPowerSeriesAt (f - g) (pf - pg) x
theorem
AnalyticWithinAt.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{s : Set E}
{x : E}
(hf : AnalyticWithinAt 𝕜 f s x)
(hg : AnalyticWithinAt 𝕜 g s x)
:
AnalyticWithinAt 𝕜 (f - g) s x
theorem
AnalyticAt.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
(hg : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (f - g) x
theorem
AnalyticWithinOn.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
(hg : AnalyticWithinOn 𝕜 g s)
:
AnalyticWithinOn 𝕜 (f + g) s
theorem
AnalyticOn.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (f + g) s
theorem
AnalyticWithinOn.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
:
AnalyticWithinOn 𝕜 (-f) s
theorem
AnalyticOn.neg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
:
AnalyticOn 𝕜 (-f) s
theorem
AnalyticWithinOn.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
(hg : AnalyticWithinOn 𝕜 g s)
:
AnalyticWithinOn 𝕜 (f - g) s
theorem
AnalyticOn.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{g : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (f - g) s
Cartesian products are analytic #
theorem
FormalMultilinearSeries.radius_prod_eq_min
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(p : FormalMultilinearSeries 𝕜 E F)
(q : FormalMultilinearSeries 𝕜 E G)
:
The radius of the Cartesian product of two formal series is the minimum of their radii.
theorem
HasFPowerSeriesWithinOnBall.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{e : E}
{f : E → F}
{g : E → G}
{r : ENNReal}
{s : ENNReal}
{t : Set E}
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G}
(hf : HasFPowerSeriesWithinOnBall f p t e r)
(hg : HasFPowerSeriesWithinOnBall g q t e s)
:
HasFPowerSeriesWithinOnBall (fun (x : E) => (f x, g x)) (p.prod q) t e (min r s)
theorem
HasFPowerSeriesOnBall.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{e : E}
{f : E → F}
{g : E → G}
{r : ENNReal}
{s : ENNReal}
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G}
(hf : HasFPowerSeriesOnBall f p e r)
(hg : HasFPowerSeriesOnBall g q e s)
:
HasFPowerSeriesOnBall (fun (x : E) => (f x, g x)) (p.prod q) e (min r s)
theorem
HasFPowerSeriesWithinAt.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{e : E}
{f : E → F}
{g : E → G}
{s : Set E}
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G}
(hf : HasFPowerSeriesWithinAt f p s e)
(hg : HasFPowerSeriesWithinAt g q s e)
:
HasFPowerSeriesWithinAt (fun (x : E) => (f x, g x)) (p.prod q) s e
theorem
HasFPowerSeriesAt.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{e : E}
{f : E → F}
{g : E → G}
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G}
(hf : HasFPowerSeriesAt f p e)
(hg : HasFPowerSeriesAt g q e)
:
HasFPowerSeriesAt (fun (x : E) => (f x, g x)) (p.prod q) e
theorem
AnalyticWithinAt.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{e : E}
{f : E → F}
{g : E → G}
{s : Set E}
(hf : AnalyticWithinAt 𝕜 f s e)
(hg : AnalyticWithinAt 𝕜 g s e)
:
AnalyticWithinAt 𝕜 (fun (x : E) => (f x, g x)) s e
The Cartesian product of analytic functions is analytic.
theorem
AnalyticAt.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{e : E}
{f : E → F}
{g : E → G}
(hf : AnalyticAt 𝕜 f e)
(hg : AnalyticAt 𝕜 g e)
:
AnalyticAt 𝕜 (fun (x : E) => (f x, g x)) e
The Cartesian product of analytic functions is analytic.
theorem
AnalyticWithinOn.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{g : E → G}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
(hg : AnalyticWithinOn 𝕜 g s)
:
AnalyticWithinOn 𝕜 (fun (x : E) => (f x, g x)) s
The Cartesian product of analytic functions within a set is analytic.
theorem
AnalyticOn.prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{g : E → G}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (fun (x : E) => (f x, g x)) s
The Cartesian product of analytic functions is analytic.
theorem
AnalyticAt.comp₂
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{h : F × G → H}
{f : E → F}
{g : E → G}
{x : E}
(ha : AnalyticAt 𝕜 h (f x, g x))
(fa : AnalyticAt 𝕜 f x)
(ga : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (fun (x : E) => h (f x, g x)) x
AnalyticAt.comp for functions on product spaces
theorem
AnalyticWithinAt.comp₂
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{h : F × G → H}
{f : E → F}
{g : E → G}
{s : Set (F × G)}
{t : Set E}
{x : E}
(ha : AnalyticWithinAt 𝕜 h s (f x, g x))
(fa : AnalyticWithinAt 𝕜 f t x)
(ga : AnalyticWithinAt 𝕜 g t x)
(hf : Set.MapsTo (fun (y : E) => (f y, g y)) t s)
:
AnalyticWithinAt 𝕜 (fun (x : E) => h (f x, g x)) t x
AnalyticWithinAt.comp for functions on product spaces
theorem
AnalyticAt.comp₂_analyticWithinAt
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{h : F × G → H}
{f : E → F}
{g : E → G}
{x : E}
{s : Set E}
(ha : AnalyticAt 𝕜 h (f x, g x))
(fa : AnalyticWithinAt 𝕜 f s x)
(ga : AnalyticWithinAt 𝕜 g s x)
:
AnalyticWithinAt 𝕜 (fun (x : E) => h (f x, g x)) s x
AnalyticAt.comp_analyticWithinAt for functions on product spaces
theorem
AnalyticOn.comp₂
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{h : F × G → H}
{f : E → F}
{g : E → G}
{s : Set (F × G)}
{t : Set E}
(ha : AnalyticOn 𝕜 h s)
(fa : AnalyticOn 𝕜 f t)
(ga : AnalyticOn 𝕜 g t)
(m : ∀ x ∈ t, (f x, g x) ∈ s)
:
AnalyticOn 𝕜 (fun (x : E) => h (f x, g x)) t
AnalyticOn.comp for functions on product spaces
theorem
AnalyticWithinOn.comp₂
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{h : F × G → H}
{f : E → F}
{g : E → G}
{s : Set (F × G)}
{t : Set E}
(ha : AnalyticWithinOn 𝕜 h s)
(fa : AnalyticWithinOn 𝕜 f t)
(ga : AnalyticWithinOn 𝕜 g t)
(m : Set.MapsTo (fun (y : E) => (f y, g y)) t s)
:
AnalyticWithinOn 𝕜 (fun (x : E) => h (f x, g x)) t
AnalyticWithinOn.comp for functions on product spaces
theorem
AnalyticAt.curry_left
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{p : E × F}
(fa : AnalyticAt 𝕜 f p)
:
AnalyticAt 𝕜 (fun (x : E) => f (x, p.2)) p.1
Analytic functions on products are analytic in the first coordinate
theorem
AnalyticAt.along_fst
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{p : E × F}
(fa : AnalyticAt 𝕜 f p)
:
AnalyticAt 𝕜 (fun (x : E) => f (x, p.2)) p.1
Alias of AnalyticAt.curry_left.
Analytic functions on products are analytic in the first coordinate
theorem
AnalyticWithinAt.curry_left
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{s : Set (E × F)}
{p : E × F}
(fa : AnalyticWithinAt 𝕜 f s p)
:
AnalyticWithinAt 𝕜 (fun (x : E) => f (x, p.2)) {x : E | (x, p.2) ∈ s} p.1
theorem
AnalyticAt.curry_right
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{p : E × F}
(fa : AnalyticAt 𝕜 f p)
:
AnalyticAt 𝕜 (fun (y : F) => f (p.1, y)) p.2
Analytic functions on products are analytic in the second coordinate
theorem
AnalyticAt.along_snd
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{p : E × F}
(fa : AnalyticAt 𝕜 f p)
:
AnalyticAt 𝕜 (fun (y : F) => f (p.1, y)) p.2
Alias of AnalyticAt.curry_right.
Analytic functions on products are analytic in the second coordinate
theorem
AnalyticWithinAt.curry_right
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{s : Set (E × F)}
{p : E × F}
(fa : AnalyticWithinAt 𝕜 f s p)
:
AnalyticWithinAt 𝕜 (fun (y : F) => f (p.1, y)) {y : F | (p.1, y) ∈ s} p.2
theorem
AnalyticOn.curry_left
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{s : Set (E × F)}
{y : F}
(fa : AnalyticOn 𝕜 f s)
:
AnalyticOn 𝕜 (fun (x : E) => f (x, y)) {x : E | (x, y) ∈ s}
Analytic functions on products are analytic in the first coordinate
theorem
AnalyticOn.along_fst
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{s : Set (E × F)}
{y : F}
(fa : AnalyticOn 𝕜 f s)
:
AnalyticOn 𝕜 (fun (x : E) => f (x, y)) {x : E | (x, y) ∈ s}
Alias of AnalyticOn.curry_left.
Analytic functions on products are analytic in the first coordinate
theorem
AnalyticWithinOn.curry_left
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{s : Set (E × F)}
{y : F}
(fa : AnalyticWithinOn 𝕜 f s)
:
AnalyticWithinOn 𝕜 (fun (x : E) => f (x, y)) {x : E | (x, y) ∈ s}
theorem
AnalyticOn.curry_right
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{x : E}
{s : Set (E × F)}
(fa : AnalyticOn 𝕜 f s)
:
AnalyticOn 𝕜 (fun (y : F) => f (x, y)) {y : F | (x, y) ∈ s}
Analytic functions on products are analytic in the second coordinate
theorem
AnalyticOn.along_snd
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{x : E}
{s : Set (E × F)}
(fa : AnalyticOn 𝕜 f s)
:
AnalyticOn 𝕜 (fun (y : F) => f (x, y)) {y : F | (x, y) ∈ s}
Alias of AnalyticOn.curry_right.
Analytic functions on products are analytic in the second coordinate
theorem
AnalyticWithinOn.curry_right
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E × F → G}
{x : E}
{s : Set (E × F)}
(fa : AnalyticWithinOn 𝕜 f s)
:
AnalyticWithinOn 𝕜 (fun (y : F) => f (x, y)) {y : F | (x, y) ∈ s}
Analyticity in Pi spaces #
In this section, f : Π i, E → Fm i is a family of functions, i.e., each f i is a function,
from E to a space Fm i. We discuss whether the family as a whole is analytic as a function
of x : E, i.e., whether x ↦ (f 1 x, ..., f n x) is analytic from E to the product space
Π i, Fm i. This function is denoted either by fun x ↦ (fun i ↦ f i x), or fun x i ↦ f i x,
or fun x ↦ (f ⬝ x). We use the latter spelling in the statements, for readability purposes.
theorem
FormalMultilinearSeries.radius_pi_le
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
(p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i))
(i : ι)
:
(FormalMultilinearSeries.pi p).radius ≤ (p i).radius
theorem
FormalMultilinearSeries.le_radius_pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{r : ENNReal}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(h : ∀ (i : ι), r ≤ (p i).radius)
:
r ≤ (FormalMultilinearSeries.pi p).radius
theorem
FormalMultilinearSeries.radius_pi_eq_iInf
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
:
(FormalMultilinearSeries.pi p).radius = ⨅ (i : ι), (p i).radius
theorem
HasFPowerSeriesWithinOnBall.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
{r : ENNReal}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r)
(hr : 0 < r)
:
HasFPowerSeriesWithinOnBall (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) s e r
If each function in a finite family has a power series within a ball, then so does the family as a whole. Note that the positivity assumption on the radius is only needed when the family is empty.
theorem
hasFPowerSeriesWithinOnBall_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
{r : ENNReal}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(hr : 0 < r)
:
HasFPowerSeriesWithinOnBall (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) s e r ↔ ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
theorem
HasFPowerSeriesOnBall.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{r : ENNReal}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(hf : ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r)
(hr : 0 < r)
:
HasFPowerSeriesOnBall (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) e r
theorem
hasFPowerSeriesOnBall_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{r : ENNReal}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(hr : 0 < r)
:
HasFPowerSeriesOnBall (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) e r ↔ ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r
theorem
HasFPowerSeriesWithinAt.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e)
:
HasFPowerSeriesWithinAt (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) s e
theorem
hasFPowerSeriesWithinAt_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
:
HasFPowerSeriesWithinAt (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) s e ↔ ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
theorem
HasFPowerSeriesAt.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
(hf : ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e)
:
HasFPowerSeriesAt (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) e
theorem
hasFPowerSeriesAt_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}
:
HasFPowerSeriesAt (fun (x : E) (x_1 : ι) => f x_1 x) (FormalMultilinearSeries.pi p) e ↔ ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e
theorem
AnalyticWithinAt.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
(hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e)
:
AnalyticWithinAt 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s e
theorem
analyticWithinAt_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
:
AnalyticWithinAt 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s e ↔ ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e
theorem
AnalyticAt.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
(hf : ∀ (i : ι), AnalyticAt 𝕜 (f i) e)
:
AnalyticAt 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) e
theorem
analyticAt_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{e : E}
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
:
AnalyticAt 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) e ↔ ∀ (i : ι), AnalyticAt 𝕜 (f i) e
theorem
AnalyticWithinOn.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
(hf : ∀ (i : ι), AnalyticWithinOn 𝕜 (f i) s)
:
AnalyticWithinOn 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s
theorem
analyticWithinOn_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
:
AnalyticWithinOn 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s ↔ ∀ (i : ι), AnalyticWithinOn 𝕜 (f i) s
theorem
AnalyticOn.pi
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
(hf : ∀ (i : ι), AnalyticOn 𝕜 (f i) s)
:
AnalyticOn 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s
theorem
analyticOn_pi_iff
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_9}
[Fintype ι]
{Fm : ι → Type u_10}
[(i : ι) → NormedAddCommGroup (Fm i)]
[(i : ι) → NormedSpace 𝕜 (Fm i)]
{f : (i : ι) → E → Fm i}
{s : Set E}
:
AnalyticOn 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s ↔ ∀ (i : ι), AnalyticOn 𝕜 (f i) s
Arithmetic on analytic functions #
theorem
analyticAt_smul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
[NormedSpace 𝕝 E]
[IsScalarTower 𝕜 𝕝 E]
(z : 𝕝 × E)
:
AnalyticAt 𝕜 (fun (x : 𝕝 × E) => x.1 • x.2) z
Scalar multiplication is analytic (jointly in both variables). The statement is a little pedantic to allow towers of field extensions.
TODO: can we replace 𝕜' with a "normed module" in such a way that analyticAt_mul is a special
case of this?
theorem
analyticAt_mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
(z : A × A)
:
AnalyticAt 𝕜 (fun (x : A × A) => x.1 * x.2) z
Multiplication in a normed algebra over 𝕜 is analytic.
theorem
AnalyticWithinAt.smul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
[NormedSpace 𝕝 F]
[IsScalarTower 𝕜 𝕝 F]
{f : E → 𝕝}
{g : E → F}
{s : Set E}
{z : E}
(hf : AnalyticWithinAt 𝕜 f s z)
(hg : AnalyticWithinAt 𝕜 g s z)
:
AnalyticWithinAt 𝕜 (fun (x : E) => f x • g x) s z
Scalar multiplication of one analytic function by another.
theorem
AnalyticAt.smul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
[NormedSpace 𝕝 F]
[IsScalarTower 𝕜 𝕝 F]
{f : E → 𝕝}
{g : E → F}
{z : E}
(hf : AnalyticAt 𝕜 f z)
(hg : AnalyticAt 𝕜 g z)
:
AnalyticAt 𝕜 (fun (x : E) => f x • g x) z
Scalar multiplication of one analytic function by another.
theorem
AnalyticWithinOn.smul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
[NormedSpace 𝕝 F]
[IsScalarTower 𝕜 𝕝 F]
{f : E → 𝕝}
{g : E → F}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
(hg : AnalyticWithinOn 𝕜 g s)
:
AnalyticWithinOn 𝕜 (fun (x : E) => f x • g x) s
Scalar multiplication of one analytic function by another.
theorem
AnalyticOn.smul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
[NormedSpace 𝕝 F]
[IsScalarTower 𝕜 𝕝 F]
{f : E → 𝕝}
{g : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (fun (x : E) => f x • g x) s
Scalar multiplication of one analytic function by another.
theorem
AnalyticWithinAt.mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{g : E → A}
{s : Set E}
{z : E}
(hf : AnalyticWithinAt 𝕜 f s z)
(hg : AnalyticWithinAt 𝕜 g s z)
:
AnalyticWithinAt 𝕜 (fun (x : E) => f x * g x) s z
Multiplication of analytic functions (valued in a normed 𝕜-algebra) is analytic.
theorem
AnalyticAt.mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{g : E → A}
{z : E}
(hf : AnalyticAt 𝕜 f z)
(hg : AnalyticAt 𝕜 g z)
:
AnalyticAt 𝕜 (fun (x : E) => f x * g x) z
Multiplication of analytic functions (valued in a normed 𝕜-algebra) is analytic.
theorem
AnalyticWithinOn.mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{g : E → A}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
(hg : AnalyticWithinOn 𝕜 g s)
:
AnalyticWithinOn 𝕜 (fun (x : E) => f x * g x) s
Multiplication of analytic functions (valued in a normed 𝕜-algebra) is analytic.
theorem
AnalyticOn.mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{g : E → A}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (fun (x : E) => f x * g x) s
Multiplication of analytic functions (valued in a normed 𝕜-algebra) is analytic.
theorem
AnalyticWithinAt.pow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{z : E}
{s : Set E}
(hf : AnalyticWithinAt 𝕜 f s z)
(n : ℕ)
:
AnalyticWithinAt 𝕜 (fun (x : E) => f x ^ n) s z
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticAt.pow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{z : E}
(hf : AnalyticAt 𝕜 f z)
(n : ℕ)
:
AnalyticAt 𝕜 (fun (x : E) => f x ^ n) z
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticWithinOn.pow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{s : Set E}
(hf : AnalyticWithinOn 𝕜 f s)
(n : ℕ)
:
AnalyticWithinOn 𝕜 (fun (x : E) => f x ^ n) s
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticOn.pow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f : E → A}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(n : ℕ)
:
AnalyticOn 𝕜 (fun (x : E) => f x ^ n) s
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
def
formalMultilinearSeries_geometric
(𝕜 : Type u_9)
(A : Type u_10)
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
:
FormalMultilinearSeries 𝕜 A A
The geometric series 1 + x + x ^ 2 + ... as a FormalMultilinearSeries.
Equations
Instances For
theorem
formalMultilinearSeries_geometric_apply_norm
(𝕜 : Type u_9)
(A : Type u_10)
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
[NormOneClass A]
(n : ℕ)
:
‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1
theorem
formalMultilinearSeries_geometric_radius
(𝕜 : Type u_10)
[NontriviallyNormedField 𝕜]
(A : Type u_9)
[NormedRing A]
[NormOneClass A]
[NormedAlgebra 𝕜 A]
:
(formalMultilinearSeries_geometric 𝕜 A).radius = 1
theorem
hasFPowerSeriesOnBall_inv_one_sub
(𝕜 : Type u_9)
(𝕝 : Type u_10)
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
:
HasFPowerSeriesOnBall (fun (x : 𝕝) => (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1
theorem
analyticAt_inv_one_sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
(𝕝 : Type u_9)
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
:
AnalyticAt 𝕜 (fun (x : 𝕝) => (1 - x)⁻¹) 0
theorem
analyticAt_inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{z : 𝕝}
(hz : z ≠ 0)
:
AnalyticAt 𝕜 Inv.inv z
If 𝕝 is a normed field extension of 𝕜, then the inverse map 𝕝 → 𝕝 is 𝕜-analytic
away from 0.
theorem
analyticOn_inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
:
AnalyticOn 𝕜 (fun (z : 𝕝) => z⁻¹) {z : 𝕝 | z ≠ 0}
x⁻¹ is analytic away from zero
theorem
AnalyticWithinAt.inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{x : E}
{s : Set E}
(fa : AnalyticWithinAt 𝕜 f s x)
(f0 : f x ≠ 0)
:
AnalyticWithinAt 𝕜 (fun (x : E) => (f x)⁻¹) s x
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticAt.inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{x : E}
(fa : AnalyticAt 𝕜 f x)
(f0 : f x ≠ 0)
:
AnalyticAt 𝕜 (fun (x : E) => (f x)⁻¹) x
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticWithinOn.inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
(fa : AnalyticWithinOn 𝕜 f s)
(f0 : ∀ x ∈ s, f x ≠ 0)
:
AnalyticWithinOn 𝕜 (fun (x : E) => (f x)⁻¹) s
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticOn.inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
(fa : AnalyticOn 𝕜 f s)
(f0 : ∀ x ∈ s, f x ≠ 0)
:
AnalyticOn 𝕜 (fun (x : E) => (f x)⁻¹) s
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticWithinAt.div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{g : E → 𝕝}
{s : Set E}
{x : E}
(fa : AnalyticWithinAt 𝕜 f s x)
(ga : AnalyticWithinAt 𝕜 g s x)
(g0 : g x ≠ 0)
:
AnalyticWithinAt 𝕜 (fun (x : E) => f x / g x) s x
f x / g x is analytic away from g x = 0
theorem
AnalyticAt.div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{g : E → 𝕝}
{x : E}
(fa : AnalyticAt 𝕜 f x)
(ga : AnalyticAt 𝕜 g x)
(g0 : g x ≠ 0)
:
AnalyticAt 𝕜 (fun (x : E) => f x / g x) x
f x / g x is analytic away from g x = 0
theorem
AnalyticWithinOn.div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{g : E → 𝕝}
{s : Set E}
(fa : AnalyticWithinOn 𝕜 f s)
(ga : AnalyticWithinOn 𝕜 g s)
(g0 : ∀ x ∈ s, g x ≠ 0)
:
AnalyticWithinOn 𝕜 (fun (x : E) => f x / g x) s
f x / g x is analytic away from g x = 0
theorem
AnalyticOn.div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{g : E → 𝕝}
{s : Set E}
(fa : AnalyticOn 𝕜 f s)
(ga : AnalyticOn 𝕜 g s)
(g0 : ∀ x ∈ s, g x ≠ 0)
:
AnalyticOn 𝕜 (fun (x : E) => f x / g x) s
f x / g x is analytic away from g x = 0
Finite sums and products of analytic functions #
theorem
Finset.analyticWithinAt_sum
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : α → E → F}
{c : E}
{s : Set E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c)
:
AnalyticWithinAt 𝕜 (fun (z : E) => ∑ n ∈ N, f n z) s c
Finite sums of analytic functions are analytic
theorem
Finset.analyticAt_sum
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : α → E → F}
{c : E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c)
:
AnalyticAt 𝕜 (fun (z : E) => ∑ n ∈ N, f n z) c
Finite sums of analytic functions are analytic
theorem
Finset.analyticWithinOn_sum
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : α → E → F}
{s : Set E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticWithinOn 𝕜 (f n) s)
:
AnalyticWithinOn 𝕜 (fun (z : E) => ∑ n ∈ N, f n z) s
Finite sums of analytic functions are analytic
theorem
Finset.analyticOn_sum
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : α → E → F}
{s : Set E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s)
:
AnalyticOn 𝕜 (fun (z : E) => ∑ n ∈ N, f n z) s
Finite sums of analytic functions are analytic
theorem
Finset.analyticWithinAt_prod
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_9}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
{f : α → E → A}
{c : E}
{s : Set E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c)
:
AnalyticWithinAt 𝕜 (fun (z : E) => ∏ n ∈ N, f n z) s c
Finite products of analytic functions are analytic
theorem
Finset.analyticAt_prod
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_9}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
{f : α → E → A}
{c : E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c)
:
AnalyticAt 𝕜 (fun (z : E) => ∏ n ∈ N, f n z) c
Finite products of analytic functions are analytic
theorem
Finset.analyticWithinOn_prod
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_9}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
{f : α → E → A}
{s : Set E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticWithinOn 𝕜 (f n) s)
:
AnalyticWithinOn 𝕜 (fun (z : E) => ∏ n ∈ N, f n z) s
Finite products of analytic functions are analytic
theorem
Finset.analyticOn_prod
{α : Type u_1}
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_9}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
{f : α → E → A}
{s : Set E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s)
:
AnalyticOn 𝕜 (fun (z : E) => ∏ n ∈ N, f n z) s
Finite products of analytic functions are analytic