# Documentation

Mathlib.Analysis.Analytic.Constructions

# Various ways to combine analytic functions #

We show that the following are analytic:

1. Cartesian products of analytic functions
2. Arithmetic on analytic functions: mul, smul, inv, div
3. Finite sums and products: Finset.sum, Finset.prod

### Cartesian products are analytic #

theorem FormalMultilinearSeries.radius_prod_eq_min {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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 HasFPowerSeriesOnBall.prod {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [NormedSpace ๐ G] {e : E} {f : E โ F} {g : E โ G} {r : ENNReal} {s : ENNReal} {p : FormalMultilinearSeries ๐ E F} {q : FormalMultilinearSeries ๐ E G} (hf : ) (hg : ) :
HasFPowerSeriesOnBall (fun (x : E) => (f x, g x)) e (min r s)
theorem HasFPowerSeriesAt.prod {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [NormedSpace ๐ G] {e : E} {f : E โ F} {g : E โ G} {p : FormalMultilinearSeries ๐ E F} {q : FormalMultilinearSeries ๐ E G} (hf : ) (hg : ) :
HasFPowerSeriesAt (fun (x : E) => (f x, g x)) e
theorem AnalyticAt.prod {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} [NormedSpace ๐ E] [NormedSpace ๐ F] [NormedSpace ๐ G] [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 AnalyticOn.compโ {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} [NormedSpace ๐ E] [NormedSpace ๐ F] [NormedSpace ๐ G] [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 AnalyticAt.along_fst {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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_snd {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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 AnalyticOn.along_fst {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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_snd {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedSpace ๐ E] [NormedSpace ๐ F] [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

### Arithmetic on analytic functions #

theorem analyticAt_smul {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {๐ : Type u_7} [] [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} [] {A : Type u_8} [] [NormedAlgebra ๐ A] (z : A ร A) :
AnalyticAt ๐ (fun (x : A ร A) => x.1 * x.2) z

Multiplication in a normed algebra over ๐ is analytic.

theorem AnalyticAt.smul {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} [NormedSpace ๐ E] [NormedSpace ๐ F] {๐ : Type u_7} [] [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 AnalyticOn.smul {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} [NormedSpace ๐ E] [NormedSpace ๐ F] {๐ : Type u_7} [] [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 AnalyticAt.mul {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {A : Type u_8} [] [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 AnalyticOn.mul {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {A : Type u_8} [] [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 AnalyticAt.pow {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {A : Type u_8} [] [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 AnalyticOn.pow {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {A : Type u_8} [] [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) [] [] [NormedAlgebra ๐ 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) [] [] [NormedAlgebra ๐ A] [] (n : โ) :
= 1
theorem formalMultilinearSeries_geometric_radius (๐ : Type u_10) [] (A : Type u_9) [] [] [NormedAlgebra ๐ A] :
theorem hasFPowerSeriesOnBall_inv_one_sub (๐ : Type u_9) (๐ : Type u_10) [] [] [NormedAlgebra ๐ ๐] :
HasFPowerSeriesOnBall (fun (x : ๐) => (1 - x)โปยน) () 0 1
theorem analyticAt_inv_one_sub {๐ : Type u_2} [] (๐ : Type u_9) [] [NormedAlgebra ๐ ๐] :
AnalyticAt ๐ (fun (x : ๐) => (1 - x)โปยน) 0
theorem analyticAt_inv {๐ : Type u_2} [] {๐ : Type u_7} [] [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} [] {๐ : Type u_7} [] [NormedAlgebra ๐ ๐] :
AnalyticOn ๐ (fun (z : ๐) => ) {z : ๐ | z โ  0}

xโปยน is analytic away from zero

theorem AnalyticAt.inv {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {๐ : Type u_7} [] [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 AnalyticOn.inv {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {๐ : Type u_7} [] [NormedAlgebra ๐ ๐] {f : E โ ๐} {s : Set E} (fa : AnalyticOn ๐ f s) (f0 : โ x โ s, f x โ  0) :
AnalyticOn ๐ (fun (x : E) => (f x)โปยน) s

xโปยน is analytic away from zero

theorem AnalyticAt.div {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {๐ : Type u_7} [] [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 AnalyticOn.div {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {๐ : Type u_7} [] [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.analyticAt_sum {ฮฑ : Type u_1} {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} [NormedSpace ๐ E] [NormedSpace ๐ F] {f : ฮฑ โ E โ F} {c : E} (N : Finset ฮฑ) (h : โ n โ N, AnalyticAt ๐ (f n) c) :
AnalyticAt ๐ (fun (z : E) => Finset.sum N fun (n : ฮฑ) => f n z) c

Finite sums of analytic functions are analytic

theorem Finset.analyticOn_sum {ฮฑ : Type u_1} {๐ : Type u_2} [] {E : Type u_3} {F : Type u_4} [NormedSpace ๐ E] [NormedSpace ๐ F] {f : ฮฑ โ E โ F} {s : Set E} (N : Finset ฮฑ) (h : โ n โ N, AnalyticOn ๐ (f n) s) :
AnalyticOn ๐ (fun (z : E) => Finset.sum N fun (n : ฮฑ) => f n z) s

Finite sums of analytic functions are analytic

theorem Finset.analyticAt_prod {ฮฑ : Type u_1} {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {A : Type u_9} [] [NormedAlgebra ๐ A] {f : ฮฑ โ E โ A} {c : E} (N : Finset ฮฑ) (h : โ n โ N, AnalyticAt ๐ (f n) c) :
AnalyticAt ๐ (fun (z : E) => Finset.prod N fun (n : ฮฑ) => f n z) c

Finite products of analytic functions are analytic

theorem Finset.analyticOn_prod {ฮฑ : Type u_1} {๐ : Type u_2} [] {E : Type u_3} [NormedSpace ๐ E] {A : Type u_9} [] [NormedAlgebra ๐ A] {f : ฮฑ โ E โ A} {s : Set E} (N : Finset ฮฑ) (h : โ n โ N, AnalyticOn ๐ (f n) s) :
AnalyticOn ๐ (fun (z : E) => Finset.prod N fun (n : ฮฑ) => f n z) s

Finite products of analytic functions are analytic