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

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)) (p.prod 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)) (p.prod 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.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 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 AnalyticOn.curry_left {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {f : E ร— F โ†’ G} {s : Set (E ร— F)} {y : F} (fa : AnalyticOn ๐•œ f s) :
AnalyticOn ๐•œ (fun (x : E) => f (x, y)) {x : E | (x, y) โˆˆ s}

Analytic functions on products are analytic in the first coordinate

theorem AnalyticOn.along_fst {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {f : E ร— F โ†’ G} {s : Set (E ร— F)} {y : F} (fa : AnalyticOn ๐•œ f s) :
AnalyticOn ๐•œ (fun (x : E) => f (x, y)) {x : E | (x, y) โˆˆ s}

Alias of AnalyticOn.curry_left.


Analytic functions on products are analytic in the first coordinate

theorem AnalyticOn.curry_right {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {f : E ร— F โ†’ G} {x : E} {s : Set (E ร— F)} (fa : AnalyticOn ๐•œ f s) :
AnalyticOn ๐•œ (fun (y : F) => f (x, y)) {y : F | (x, y) โˆˆ s}

Analytic functions on products are analytic in the second coordinate

theorem AnalyticOn.along_snd {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ๐•œ E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [NormedAddCommGroup G] [NormedSpace ๐•œ G] {f : E ร— F โ†’ G} {x : E} {s : Set (E ร— F)} (fa : AnalyticOn ๐•œ f s) :
AnalyticOn ๐•œ (fun (y : F) => f (x, y)) {y : F | (x, y) โˆˆ s}

Alias of AnalyticOn.curry_right.


Analytic functions on products are analytic in the second coordinate

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

The geometric series 1 + x + x ^ 2 + ... as a FormalMultilinearSeries.

Equations
Instances For
    theorem formalMultilinearSeries_geometric_radius (๐•œ : Type u_10) [NontriviallyNormedField ๐•œ] (A : Type u_9) [NormedRing A] [NormOneClass A] [NormedAlgebra ๐•œ A] :
    (formalMultilinearSeries_geometric ๐•œ A).radius = 1
    theorem hasFPowerSeriesOnBall_inv_one_sub (๐•œ : Type u_9) (๐• : Type u_10) [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•] [NormedAlgebra ๐•œ ๐•] :
    HasFPowerSeriesOnBall (fun (x : ๐•) => (1 - x)โปยน) (formalMultilinearSeries_geometric ๐•œ ๐•) 0 1
    theorem analyticAt_inv_one_sub {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] (๐• : Type u_9) [NontriviallyNormedField ๐•] [NormedAlgebra ๐•œ ๐•] :
    AnalyticAt ๐•œ (fun (x : ๐•) => (1 - x)โปยน) 0
    theorem analyticAt_inv {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] {๐• : Type u_7} [NontriviallyNormedField ๐•] [NormedAlgebra ๐•œ ๐•] {z : ๐•} (hz : z โ‰  0) :
    AnalyticAt ๐•œ Inv.inv z

    If ๐• is a normed field extension of ๐•œ, then the inverse map ๐• โ†’ ๐• is ๐•œ-analytic away from 0.

    theorem analyticOn_inv {๐•œ : Type u_2} [NontriviallyNormedField ๐•œ] {๐• : Type u_7} [NontriviallyNormedField ๐•] [NormedAlgebra ๐•œ ๐•] :
    AnalyticOn ๐•œ (fun (z : ๐•) => zโปยน) {z : ๐• | z โ‰  0}

    xโปยน is analytic away from zero

    theorem 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) => โˆ‘ n โˆˆ 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) => โˆ‘ n โˆˆ 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) => โˆ n โˆˆ 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) => โˆ n โˆˆ N, f n z) s

    Finite products of analytic functions are analytic