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} [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) : FormalMultilinearSeries.radius (FormalMultilinearSeries.prod p q) = min (FormalMultilinearSeries.radius p) (FormalMultilinearSeries.radius q)

The radius of the Cartesian product of two formal series is the minimum of their radii.

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)) (FormalMultilinearSeries.prod p q) e (min r s)

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)) (FormalMultilinearSeries.prod p q) e

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 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 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 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

Analytic functions on products are analytic in the first 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

Analytic functions on products are analytic in the second 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}

Analytic functions on products are analytic in the first 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}

Analytic functions on products are analytic in the second coordinate

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 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 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 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 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 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 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

• formalMultilinearSeries_geometric 𝕜 A n = ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A

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.radius (formalMultilinearSeries_geometric 𝕜 A) = 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 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 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

x⁻¹ is analytic away from zero

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 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.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) => 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} [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) => 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} [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) => 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} [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) => Finset.prod N fun (n : α) => f n z) s

Finite products of analytic functions are analytic