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
analyticOnNhd_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}
:
AnalyticOnNhd 𝕜 (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
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
Addition, negation, subtraction, scalar multiplication #
theorem
HasFPowerSeriesWithinOnBall.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{pf 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 g : E → F}
{pf 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 g : E → F}
{pf 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 g : E → F}
{pf 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 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 g : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
(hg : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (f + g) x
theorem
AnalyticAt.fun_add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
(hg : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (fun (i : E) => f i + g i) x
Eta-expanded form of AnalyticAt.add
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
AnalyticAt.fun_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 𝕜 (fun (i : E) => -f i) x
Eta-expanded form of AnalyticAt.neg
@[simp]
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}
:
theorem
HasFPowerSeriesWithinOnBall.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{pf 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 g : E → F}
{pf 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 g : E → F}
{pf 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 g : E → F}
{pf 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 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 g : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
(hg : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (f - g) x
theorem
AnalyticAt.fun_sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{x : E}
(hf : AnalyticAt 𝕜 f x)
(hg : AnalyticAt 𝕜 g x)
:
AnalyticAt 𝕜 (fun (i : E) => f i - g i) x
Eta-expanded form of AnalyticAt.sub
theorem
HasFPowerSeriesWithinOnBall.const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : HasFPowerSeriesWithinOnBall f pf s x r)
:
HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r
theorem
HasFPowerSeriesOnBall.const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : HasFPowerSeriesOnBall f pf x r)
:
HasFPowerSeriesOnBall (c • f) (c • pf) x r
theorem
HasFPowerSeriesWithinAt.const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : HasFPowerSeriesWithinAt f pf s x)
:
HasFPowerSeriesWithinAt (c • f) (c • pf) s x
theorem
HasFPowerSeriesAt.const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : HasFPowerSeriesAt f pf x)
:
HasFPowerSeriesAt (c • f) (c • pf) x
theorem
AnalyticWithinAt.const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : AnalyticWithinAt 𝕜 f s x)
:
AnalyticWithinAt 𝕜 (c • f) s x
theorem
AnalyticAt.const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : AnalyticAt 𝕜 f x)
:
AnalyticAt 𝕜 (c • f) x
theorem
AnalyticAt.fun_const_smul
{𝕜 : 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}
{c : 𝕜}
(hf : AnalyticAt 𝕜 f x)
:
AnalyticAt 𝕜 (fun (i : E) => c • f i) x
Eta-expanded form of AnalyticAt.const_smul
theorem
AnalyticOn.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (f + g) s
theorem
AnalyticOnNhd.add
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{s : Set E}
(hf : AnalyticOnNhd 𝕜 f s)
(hg : AnalyticOnNhd 𝕜 g s)
:
AnalyticOnNhd 𝕜 (f + g) 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
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
:
AnalyticOnNhd 𝕜 (-f) 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 g : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜 f s)
(hg : AnalyticOn 𝕜 g s)
:
AnalyticOn 𝕜 (f - g) s
theorem
AnalyticOnNhd.sub
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f g : E → F}
{s : Set E}
(hf : AnalyticOnNhd 𝕜 f s)
(hg : AnalyticOnNhd 𝕜 g s)
:
AnalyticOnNhd 𝕜 (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 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)
:
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 s : ENNReal}
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G}
(hf : HasFPowerSeriesOnBall f p e r)
(hg : HasFPowerSeriesOnBall g q e 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
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 within a set is analytic.
theorem
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
(hg : AnalyticOnNhd 𝕜 g s)
:
AnalyticOnNhd 𝕜 (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
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 h s)
(fa : AnalyticOnNhd 𝕜 f t)
(ga : AnalyticOnNhd 𝕜 g t)
(m : ∀ x ∈ t, (f x, g x) ∈ s)
:
AnalyticOnNhd 𝕜 (fun (x : E) => h (f x, g x)) t
AnalyticOnNhd.comp 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 : Set.MapsTo (fun (y : E) => (f y, g y)) t s)
:
AnalyticOn 𝕜 (fun (x : E) => h (f x, g x)) t
AnalyticOn.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)
:
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)
:
theorem
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
:
Analytic functions on products are analytic in the first coordinate
theorem
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
:
Alias of AnalyticOnNhd.curry_left.
Analytic functions on products are analytic in the first coordinate
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)
:
theorem
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
:
Analytic functions on products are analytic in the second coordinate
theorem
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
:
Alias of AnalyticOnNhd.curry_right.
Analytic functions on products are analytic in the second coordinate
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)
:
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 : ι)
:
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)
:
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)}
:
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}
:
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}
:
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}
:
theorem
AnalyticOnNhd.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 : ι), AnalyticOnNhd 𝕜 (f i) s)
:
AnalyticOnNhd 𝕜 (fun (x : E) (x_1 : ι) => f x_1 x) s
theorem
analyticOnNhd_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}
:
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 𝕜 (f • g) z
Scalar multiplication of one analytic function by another.
theorem
AnalyticAt.fun_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 (i : E) => f i • g i) z
Eta-expanded form of AnalyticAt.smul
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
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
(hg : AnalyticOnNhd 𝕜 g s)
:
AnalyticOnNhd 𝕜 (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 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 g : E → A}
{z : E}
(hf : AnalyticAt 𝕜 f z)
(hg : AnalyticAt 𝕜 g z)
:
AnalyticAt 𝕜 (f * g) z
Multiplication of analytic functions (valued in a normed 𝕜-algebra) is analytic.
theorem
AnalyticAt.fun_mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f g : E → A}
{z : E}
(hf : AnalyticAt 𝕜 f z)
(hg : AnalyticAt 𝕜 g z)
:
AnalyticAt 𝕜 (fun (i : E) => f i * g i) z
Eta-expanded form of AnalyticAt.mul
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 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
AnalyticOnNhd.mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A : Type u_8}
[NormedRing A]
[NormedAlgebra 𝕜 A]
{f g : E → A}
{s : Set E}
(hf : AnalyticOnNhd 𝕜 f s)
(hg : AnalyticOnNhd 𝕜 g s)
:
AnalyticOnNhd 𝕜 (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 𝕜 (f ^ n) s z
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticWithinAt.fun_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 (i : E) => f i ^ n) s z
Eta-expanded form of AnalyticWithinAt.pow
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 𝕜 (f ^ n) z
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticAt.fun_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 (i : E) => f i ^ n) z
Eta-expanded form of AnalyticAt.pow
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 𝕜 (f ^ n) s
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticOn.fun_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 (i : E) => f i ^ n) s
Eta-expanded form of AnalyticOn.pow
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticOnNhd.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 : AnalyticOnNhd 𝕜 f s)
(n : ℕ)
:
AnalyticOnNhd 𝕜 (f ^ n) s
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticOnNhd.fun_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 : AnalyticOnNhd 𝕜 f s)
(n : ℕ)
:
AnalyticOnNhd 𝕜 (fun (i : E) => f i ^ n) s
Eta-expanded form of AnalyticOnNhd.pow
Powers of analytic functions (into a normed 𝕜-algebra) are analytic.
theorem
AnalyticWithinAt.zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{s : Set E}
{n : ℤ}
(hf : AnalyticWithinAt 𝕜 f s z)
(hn : 0 ≤ n)
:
AnalyticWithinAt 𝕜 (f ^ n) s z
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticWithinAt.fun_zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{s : Set E}
{n : ℤ}
(hf : AnalyticWithinAt 𝕜 f s z)
(hn : 0 ≤ n)
:
AnalyticWithinAt 𝕜 (fun (i : E) => f i ^ n) s z
Eta-expanded form of AnalyticWithinAt.zpow_nonneg
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticAt.zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{n : ℤ}
(hf : AnalyticAt 𝕜 f z)
(hn : 0 ≤ n)
:
AnalyticAt 𝕜 (f ^ n) z
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticAt.fun_zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{n : ℤ}
(hf : AnalyticAt 𝕜 f z)
(hn : 0 ≤ n)
:
AnalyticAt 𝕜 (fun (i : E) => f i ^ n) z
Eta-expanded form of AnalyticAt.zpow_nonneg
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticOn.zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(hf : AnalyticOn 𝕜 f s)
(hn : 0 ≤ n)
:
AnalyticOn 𝕜 (f ^ n) s
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticOn.fun_zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(hf : AnalyticOn 𝕜 f s)
(hn : 0 ≤ n)
:
AnalyticOn 𝕜 (fun (i : E) => f i ^ n) s
Eta-expanded form of AnalyticOn.zpow_nonneg
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticOnNhd.zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(hf : AnalyticOnNhd 𝕜 f s)
(hn : 0 ≤ n)
:
AnalyticOnNhd 𝕜 (f ^ n) s
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
theorem
AnalyticOnNhd.fun_zpow_nonneg
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(hf : AnalyticOnNhd 𝕜 f s)
(hn : 0 ≤ n)
:
AnalyticOnNhd 𝕜 (fun (i : E) => f i ^ n) s
Eta-expanded form of AnalyticOnNhd.zpow_nonneg
ZPowers of analytic functions (into a normed field over 𝕜) are analytic if the exponent is
nonnegative.
Restriction of scalars #
theorem
HasFPowerSeriesWithinOnBall.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{p : FormalMultilinearSeries 𝕜' E F}
{x : E}
{s : Set E}
{r : ENNReal}
(hf : HasFPowerSeriesWithinOnBall f p s x r)
:
theorem
HasFPowerSeriesOnBall.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{p : FormalMultilinearSeries 𝕜' E F}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesOnBall f p x r)
:
theorem
HasFPowerSeriesWithinAt.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{p : FormalMultilinearSeries 𝕜' E F}
{x : E}
{s : Set E}
(hf : HasFPowerSeriesWithinAt f p s x)
:
theorem
HasFPowerSeriesAt.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{p : FormalMultilinearSeries 𝕜' E F}
{x : E}
(hf : HasFPowerSeriesAt f p x)
:
theorem
AnalyticWithinAt.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{x : E}
{s : Set E}
(hf : AnalyticWithinAt 𝕜' f s x)
:
AnalyticWithinAt 𝕜 f s x
theorem
AnalyticAt.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{x : E}
(hf : AnalyticAt 𝕜' f x)
:
AnalyticAt 𝕜 f x
theorem
AnalyticOn.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{s : Set E}
(hf : AnalyticOn 𝕜' f s)
:
AnalyticOn 𝕜 f s
theorem
AnalyticOnNhd.restrictScalars
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_9}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{f : E → F}
{s : Set E}
(hf : AnalyticOnNhd 𝕜' f s)
:
AnalyticOnNhd 𝕜 f s
Inversion is 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_eq_ofScalars
(𝕜 : Type u_9)
(A : Type u_10)
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
:
The geometric series as an ofScalars series.
theorem
formalMultilinearSeries_geometric_apply_norm_le
(𝕜 : Type u_9)
(A : Type u_10)
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
(n : ℕ)
:
theorem
formalMultilinearSeries_geometric_apply_norm
(𝕜 : Type u_9)
(A : Type u_10)
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
[NormOneClass A]
(n : ℕ)
:
theorem
one_le_formalMultilinearSeries_geometric_radius
(𝕜 : Type u_9)
[NontriviallyNormedField 𝕜]
(A : Type u_10)
[NormedRing A]
[NormedAlgebra 𝕜 A]
:
theorem
formalMultilinearSeries_geometric_radius
(𝕜 : Type u_9)
[NontriviallyNormedField 𝕜]
(A : Type u_10)
[NormedRing A]
[NormOneClass A]
[NormedAlgebra 𝕜 A]
:
theorem
hasFPowerSeriesOnBall_inverse_one_sub
(𝕜 : Type u_9)
[NontriviallyNormedField 𝕜]
(A : Type u_10)
[NormedRing A]
[NormedAlgebra 𝕜 A]
[HasSummableGeomSeries A]
:
HasFPowerSeriesOnBall (fun (x : A) => Ring.inverse (1 - x)) (formalMultilinearSeries_geometric 𝕜 A) 0 1
theorem
analyticAt_inverse_one_sub
(𝕜 : Type u_9)
[NontriviallyNormedField 𝕜]
(A : Type u_10)
[NormedRing A]
[NormedAlgebra 𝕜 A]
[HasSummableGeomSeries A]
:
AnalyticAt 𝕜 (fun (x : A) => Ring.inverse (1 - x)) 0
theorem
analyticAt_inverse
{𝕜 : Type u_9}
[NontriviallyNormedField 𝕜]
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[HasSummableGeomSeries A]
(z : Aˣ)
:
AnalyticAt 𝕜 Ring.inverse ↑z
If A is a normed algebra over 𝕜 with summable geometric series, then inversion on A is
analytic at any unit.
theorem
analyticOnNhd_inverse
{𝕜 : Type u_9}
[NontriviallyNormedField 𝕜]
{A : Type u_10}
[NormedRing A]
[NormedAlgebra 𝕜 A]
[HasSummableGeomSeries A]
:
AnalyticOnNhd 𝕜 Ring.inverse {x : A | IsUnit x}
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
analyticOnNhd_inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
:
x⁻¹ is analytic away from zero
theorem
analyticOn_inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
:
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 𝕜 f⁻¹ s x
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticWithinAt.fun_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 (i : E) => (f i)⁻¹) s x
Eta-expanded form of AnalyticWithinAt.inv
(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 𝕜 f⁻¹ x
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticAt.fun_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 (i : E) => (f i)⁻¹) x
Eta-expanded form of AnalyticAt.inv
(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 𝕜 f⁻¹ s
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticOn.fun_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 (i : E) => (f i)⁻¹) s
Eta-expanded form of AnalyticOn.inv
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticOnNhd.inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
(fa : AnalyticOnNhd 𝕜 f s)
(f0 : ∀ x ∈ s, f x ≠ 0)
:
AnalyticOnNhd 𝕜 f⁻¹ s
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticOnNhd.fun_inv
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
(fa : AnalyticOnNhd 𝕜 f s)
(f0 : ∀ x ∈ s, f x ≠ 0)
:
AnalyticOnNhd 𝕜 (fun (i : E) => (f i)⁻¹) s
Eta-expanded form of AnalyticOnNhd.inv
(f x)⁻¹ is analytic away from f x = 0
theorem
AnalyticWithinAt.zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{s : Set E}
{n : ℤ}
(h₁f : AnalyticWithinAt 𝕜 f s z)
(h₂f : f z ≠ 0)
:
AnalyticWithinAt 𝕜 (f ^ n) s z
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticWithinAt.fun_zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{s : Set E}
{n : ℤ}
(h₁f : AnalyticWithinAt 𝕜 f s z)
(h₂f : f z ≠ 0)
:
AnalyticWithinAt 𝕜 (fun (i : E) => f i ^ n) s z
Eta-expanded form of AnalyticWithinAt.zpow
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticAt.zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{n : ℤ}
(h₁f : AnalyticAt 𝕜 f z)
(h₂f : f z ≠ 0)
:
AnalyticAt 𝕜 (f ^ n) z
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticAt.fun_zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{z : E}
{n : ℤ}
(h₁f : AnalyticAt 𝕜 f z)
(h₂f : f z ≠ 0)
:
AnalyticAt 𝕜 (fun (i : E) => f i ^ n) z
Eta-expanded form of AnalyticAt.zpow
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticOn.zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(h₁f : AnalyticOn 𝕜 f s)
(h₂f : ∀ z ∈ s, f z ≠ 0)
:
AnalyticOn 𝕜 (f ^ n) s
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticOn.fun_zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(h₁f : AnalyticOn 𝕜 f s)
(h₂f : ∀ z ∈ s, f z ≠ 0)
:
AnalyticOn 𝕜 (fun (i : E) => f i ^ n) s
Eta-expanded form of AnalyticOn.zpow
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticOnNhd.zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(h₁f : AnalyticOnNhd 𝕜 f s)
(h₂f : ∀ z ∈ s, f z ≠ 0)
:
AnalyticOnNhd 𝕜 (f ^ n) s
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
AnalyticOnNhd.fun_zpow
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f : E → 𝕝}
{s : Set E}
{n : ℤ}
(h₁f : AnalyticOnNhd 𝕜 f s)
(h₂f : ∀ z ∈ s, f z ≠ 0)
:
AnalyticOnNhd 𝕜 (fun (i : E) => f i ^ n) s
Eta-expanded form of AnalyticOnNhd.zpow
ZPowers of analytic functions (into a normed field over 𝕜) are analytic away from the zeros.
theorem
analyticAt_iff_analytic_fun_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}
(h₁f : AnalyticAt 𝕜 f z)
(h₂f : f z ≠ 0)
:
theorem
analyticAt_iff_analytic_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}
(h₁f : AnalyticAt 𝕜 f z)
(h₂f : f z ≠ 0)
:
theorem
analyticAt_iff_analytic_fun_mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f g : E → 𝕝}
{z : E}
(h₁f : AnalyticAt 𝕜 f z)
(h₂f : f z ≠ 0)
:
theorem
analyticAt_iff_analytic_mul
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f g : E → 𝕝}
{z : E}
(h₁f : AnalyticAt 𝕜 f z)
(h₂f : f z ≠ 0)
:
theorem
AnalyticWithinAt.div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f 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 g : E → 𝕝}
{x : E}
(fa : AnalyticAt 𝕜 f x)
(ga : AnalyticAt 𝕜 g x)
(g0 : g x ≠ 0)
:
AnalyticAt 𝕜 (f / g) x
f x / g x is analytic away from g x = 0
theorem
AnalyticAt.fun_div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f g : E → 𝕝}
{x : E}
(fa : AnalyticAt 𝕜 f x)
(ga : AnalyticAt 𝕜 g x)
(g0 : g x ≠ 0)
:
AnalyticAt 𝕜 (fun (i : E) => f i / g i) x
Eta-expanded form of AnalyticAt.div
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 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
theorem
AnalyticOnNhd.div
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕝 : Type u_7}
[NontriviallyNormedField 𝕝]
[NormedAlgebra 𝕜 𝕝]
{f g : E → 𝕝}
{s : Set E}
(fa : AnalyticOnNhd 𝕜 f s)
(ga : AnalyticOnNhd 𝕜 g s)
(g0 : ∀ x ∈ s, g x ≠ 0)
:
AnalyticOnNhd 𝕜 (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_fun_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.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 𝕜 (∑ n ∈ N, f n) s c
Finite sums of analytic functions are analytic
theorem
Finset.analyticAt_fun_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.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 𝕜 (∑ n ∈ N, f n) c
Finite sums of analytic functions are analytic
theorem
Finset.analyticOn_fun_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.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 𝕜 (∑ n ∈ N, f n) s
Finite sums of analytic functions are analytic
theorem
Finset.analyticOnNhd_fun_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, AnalyticOnNhd 𝕜 (f n) s)
:
AnalyticOnNhd 𝕜 (fun (z : E) => ∑ n ∈ N, f n z) s
Finite sums of analytic functions are analytic
theorem
Finset.analyticOnNhd_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, AnalyticOnNhd 𝕜 (f n) s)
:
AnalyticOnNhd 𝕜 (∑ n ∈ N, f n) s
Finite sums of analytic functions are analytic
theorem
Finset.analyticWithinAt_fun_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.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 𝕜 (∏ n ∈ N, f n) s c
Finite products of analytic functions are analytic
theorem
Finset.analyticAt_fun_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.analyticAt_prod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{α : Type u_9}
{A : Type u_10}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
{f : α → E → A}
{c : E}
(N : Finset α)
(h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c)
:
AnalyticAt 𝕜 (∏ n ∈ N, f n) c
Finite products of analytic functions are analytic
theorem
Finset.analyticOn_fun_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
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 𝕜 (∏ n ∈ N, f n) s
Finite products of analytic functions are analytic
theorem
Finset.analyticOnNhd_fun_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, AnalyticOnNhd 𝕜 (f n) s)
:
AnalyticOnNhd 𝕜 (fun (z : E) => ∏ n ∈ N, f n z) s
Finite products of analytic functions are analytic
theorem
Finset.analyticOnNhd_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, AnalyticOnNhd 𝕜 (f n) s)
:
AnalyticOnNhd 𝕜 (∏ n ∈ N, f n) s
Finite products of analytic functions are analytic
theorem
analyticAt_finprod
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{α : Type u_9}
{A : Type u_10}
[NormedCommRing A]
[NormedAlgebra 𝕜 A]
{f : α → E → A}
{c : E}
(h : ∀ (a : α), AnalyticAt 𝕜 (f a) c)
:
AnalyticAt 𝕜 (∏ᶠ (n : α), f n) c
Finproducts of analytic functions are analytic
Unshifting #
theorem
HasFPowerSeriesWithinOnBall.unshift
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → E →L[𝕜] F}
{pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)}
{s : Set E}
{x : E}
{r : ENNReal}
{z : F}
(hf : HasFPowerSeriesWithinOnBall f pf s x r)
:
HasFPowerSeriesWithinOnBall (fun (y : E) => z + (f y) (y - x)) (pf.unshift z) s x r
theorem
HasFPowerSeriesOnBall.unshift
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → E →L[𝕜] F}
{pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)}
{x : E}
{r : ENNReal}
{z : F}
(hf : HasFPowerSeriesOnBall f pf x r)
:
HasFPowerSeriesOnBall (fun (y : E) => z + (f y) (y - x)) (pf.unshift z) x r
theorem
HasFPowerSeriesWithinAt.unshift
{𝕜 : Type u_2}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → E →L[𝕜] F}
{pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)}
{s : Set E}
{x : E}
{z : F}
(hf : HasFPowerSeriesWithinAt f pf s x)
:
HasFPowerSeriesWithinAt (fun (y : E) => z + (f y) (y - x)) (pf.unshift z) s x
Composition with a linear map #
theorem
HasFPowerSeriesWithinOnBall.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{pf : FormalMultilinearSeries 𝕜 F G}
{s : Set F}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesWithinOnBall f pf s (u x) r)
:
HasFPowerSeriesWithinOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) (⇑u ⁻¹' s) x (r / ‖u‖ₑ)
theorem
HasFPowerSeriesOnBall.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{pf : FormalMultilinearSeries 𝕜 F G}
{x : E}
{r : ENNReal}
(hf : HasFPowerSeriesOnBall f pf (u x) r)
:
HasFPowerSeriesOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) x (r / ‖u‖ₑ)
theorem
HasFPowerSeriesAt.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{pf : FormalMultilinearSeries 𝕜 F G}
{x : E}
(hf : HasFPowerSeriesAt f pf (u x))
:
HasFPowerSeriesAt (f ∘ ⇑u) (pf.compContinuousLinearMap u) x
theorem
HasFPowerSeriesWithinAt.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{pf : FormalMultilinearSeries 𝕜 F G}
{s : Set F}
{x : E}
(hf : HasFPowerSeriesWithinAt f pf s (u x))
:
HasFPowerSeriesWithinAt (f ∘ ⇑u) (pf.compContinuousLinearMap u) (⇑u ⁻¹' s) x
theorem
AnalyticAt.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{x : E}
(hf : AnalyticAt 𝕜 f (u x))
:
AnalyticAt 𝕜 (f ∘ ⇑u) x
theorem
AnalyticAtWithin.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{s : Set F}
{x : E}
(hf : AnalyticWithinAt 𝕜 f s (u x))
:
AnalyticWithinAt 𝕜 (f ∘ ⇑u) (⇑u ⁻¹' s) x
theorem
AnalyticOn.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{s : Set F}
(hf : AnalyticOn 𝕜 f s)
:
AnalyticOn 𝕜 (f ∘ ⇑u) (⇑u ⁻¹' s)
theorem
AnalyticOnNhd.compContinuousLinearMap
{𝕜 : 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]
{u : E →L[𝕜] F}
{f : F → G}
{s : Set F}
(hf : AnalyticOnNhd 𝕜 f s)
:
AnalyticOnNhd 𝕜 (f ∘ ⇑u) (⇑u ⁻¹' s)