# 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} [] [] [] (p : ) (q : ) :

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} [] [] [] {e : E} {f : EF} {g : EG} {r : ENNReal} {s : ENNReal} {p : } {q : } (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} [] [] [] {e : E} {f : EF} {g : EG} {p : } {q : } (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} [] [] [] {e : E} {f : EF} {g : EG} (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} [] [] [] {f : EF} {g : EG} {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} [] [] [] [] {h : F × GH} {f : EF} {g : EG} {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} [] [] [] [] {h : F × GH} {f : EF} {g : EG} {s : Set (F × G)} {t : Set E} (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t) (ga : AnalyticOn 𝕜 g t) (m : xt, (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} [] [] [] {f : E × FG} {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} [] [] [] {f : E × FG} {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} [] [] [] {f : E × FG} {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} [] [] [] {f : E × FG} {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} [] {𝕝 : Type u_7} [] [] [] (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} [] [] (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} [] [] {𝕝 : Type u_7} [] [] [] {f : E𝕝} {g : EF} {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} [] [] {𝕝 : Type u_7} [] [] [] {f : E𝕝} {g : EF} {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} [] {A : Type u_8} [] [] {f : EA} {g : EA} {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} [] {A : Type u_8} [] [] {f : EA} {g : EA} {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} [] {A : Type u_8} [] [] {f : EA} {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} [] {A : Type u_8} [] [] {f : EA} {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) [] [] :

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) [] [] [] (n : ) :
theorem formalMultilinearSeries_geometric_radius (𝕜 : Type u_10) (A : Type u_9) [] [] [] :
theorem hasFPowerSeriesOnBall_inv_one_sub (𝕜 : Type u_9) (𝕝 : Type u_10) [] :
HasFPowerSeriesOnBall (fun (x : 𝕝) => (1 - x)⁻¹) 0 1
theorem analyticAt_inv_one_sub {𝕜 : Type u_2} (𝕝 : Type u_9) [] :
AnalyticAt 𝕜 (fun (x : 𝕝) => (1 - x)⁻¹) 0
theorem analyticAt_inv {𝕜 : Type u_2} {𝕝 : Type u_7} [] {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} [] :
AnalyticOn 𝕜 (fun (z : 𝕝) => z⁻¹) {z : 𝕝 | z 0}

x⁻¹ is analytic away from zero

theorem AnalyticAt.inv {𝕜 : Type u_2} {E : Type u_3} [] {𝕝 : Type u_7} [] {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} [] {𝕝 : Type u_7} [] {f : E𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : xs, 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} [] {𝕝 : Type u_7} [] {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} [] {𝕝 : Type u_7} [] {f : E𝕝} {g : E𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (ga : AnalyticOn 𝕜 g s) (g0 : xs, 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} [] [] {f : αEF} {c : E} (N : ) (h : nN, 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} [] [] {f : αEF} {s : Set E} (N : ) (h : nN, 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} [] {A : Type u_9} [] [] {f : αEA} {c : E} (N : ) (h : nN, 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} [] {A : Type u_9} [] [] {f : αEA} {s : Set E} (N : ) (h : nN, AnalyticOn 𝕜 (f n) s) :
AnalyticOn 𝕜 (fun (z : E) => Finset.prod N fun (n : α) => f n z) s

Finite products of analytic functions are analytic