LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Analytic.Constructions

`Finset.analyticAt_prod` theorem Finset.analyticAt_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A} {c : E} (N : Finset α), (∀ n ∈ N, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (fun z => N.prod fun n => f n z) c This theorem states that a finite product of analytic functions is also an analytic function. More precisely, given a nontrivially normed field `𝕜`, a normed space `E`, a normed commutative ring `A` (with `𝕜` as its scalar field), a set `N` of type `α`, and a function `f` from `α` to the set of functions from `E` to `A`, if each function `f n` (for `n` in `N`) is analytic at a point `c` in `E`, then the function that maps `z` in `E` to the product (over `N`) of `f n z` is also analytic at `c`. In mathematical terms, if $f_n:E\rightarrow A$ is analytic at $c$ for each $n$ in a finite set $N$, then the function $g: E\rightarrow A$ defined by $g(z) = \prod_{n\in N} f_n(z)$ is also analytic at $c$. More concisely: A finite product of analytic functions from a normed space to a normed commutative ring is itself an analytic function.
`analyticAt_inv` theorem analyticAt_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_7} [inst_1 : NontriviallyNormedField 𝕝] [inst_2 : NormedAlgebra 𝕜 𝕝] {z : 𝕝}, z ≠ 0 → AnalyticAt 𝕜 Inv.inv z The theorem `analyticAt_inv` states that for any nontrivially normed field `𝕜` and any field extension `𝕝` of `𝕜` that is also a nontrivially normed field, the function that maps an element of `𝕝` to its inverse is `𝕜`-analytic at any point `z` in `𝕝` that is not the zero element. Here, a function is said to be `𝕜`-analytic at a point if it can be expressed as a convergent power series expansion at that point. Essentially, this theorem is saying that the inverse function is smooth, except at zero, in the sense that it has a power series expansion everywhere else. More concisely: For any nontrivially normed field extension 𝕝 of a nontrivially normed field 𝕜, the function mapping an element x in 𝕝, excluding the zero element, to its inverse is 𝕜-analytic at x.
`AnalyticOn.comp₂` theorem AnalyticOn.comp₂ : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E}, AnalyticOn 𝕜 h s → AnalyticOn 𝕜 f t → AnalyticOn 𝕜 g t → (∀ x ∈ t, (f x, g x) ∈ s) → AnalyticOn 𝕜 (fun x => h (f x, g x)) t The theorem `AnalyticOn.comp₂` states that for any nontrivially normed field `𝕜`, types `E`, `F`, `G`, `H` that are normed add commutative groups and normed spaces over `𝕜`, and given functions `f : E → F`, `g : E → G`, `h : F × G → H`, if `h` is analytic on a set `s` of `F × G`, and `f` and `g` are both analytic on a set `t` of `E` such that for all `x` in `t`, `(f x, g x)` is in `s`, then the function `x => h (f x, g x)` is also analytic on the set `t`. In simpler terms, this theorem asserts that the composition of analytic functions, in the context of product spaces, is itself analytic when the domain of the composite function meets certain conditions. More concisely: If functions `f : E → F`, `g : E → G`, and `h : F × G → H` are analytic on sets `t ⊆ E`, `s ⊆ F × G` with `s` containing `{(f x, g x) \| x ∈ t}`, then `x => h (f x, g x)` is analytic on `t`.
`AnalyticAt.smul` theorem AnalyticAt.smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕝 : Type u_7} [inst_5 : NontriviallyNormedField 𝕝] [inst_6 : NormedAlgebra 𝕜 𝕝] [inst_7 : NormedSpace 𝕝 F] [inst_8 : IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}, AnalyticAt 𝕜 f z → AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (fun x => f x • g x) z The theorem `AnalyticAt.smul` states that given two functions `f` and `g` from a normed space `E` to normed fields `𝕝` and `F` respectively, over a non-trivially normed field `𝕜`, if `f` and `g` are both analytic at a point `z` in `E`, then the function that maps `x` in `E` to the scalar multiple `f(x) • g(x)` in `F` is also analytic at the point `z`. Here, `𝕝` is also a normed algebra over `𝕜` and `F` is a normed space over `𝕝`, forming a scalar tower. More concisely: If `f : E -> 𝕝` and `g : E -> F` are analytic functions at a point `z` in a normed space `E` over a non-trivially normed field `𝕜`, then the function `x => f(x) • g(x)` from `E` to the normed field `𝕝` is analytic at `z`.
`AnalyticAt.mul` theorem AnalyticAt.mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {A : Type u_8} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A} {z : E}, AnalyticAt 𝕜 f z → AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (fun x => f x * g x) z The theorem `AnalyticAt.mul` states that if we have two functions `f` and `g` that are analytic at a point `z` in a normed space `E` over a nontrivially normed field `𝕜`, with values in a normed `𝕜`-algebra `A`, then the function defined by the pointwise multiplication of `f` and `g`, i.e., `(fun x => f x * g x)`, is also analytic at `z`. Here, a function is considered analytic at a point if it admits a convergent power series expansion around that point. More concisely: If `f` and `g` are analytic functions at a point `z` in a normed space `E` over a nontrivially normed field `𝕜` with values in a normed `𝕜`-algebra `A`, then their pointwise product `x => f x * g x` is also analytic at `z`.
`AnalyticAt.inv` theorem AnalyticAt.inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_7} [inst_3 : NontriviallyNormedField 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝} {x : E}, AnalyticAt 𝕜 f x → f x ≠ 0 → AnalyticAt 𝕜 (fun x => (f x)⁻¹) x The theorem `AnalyticAt.inv` states that for a non-zero function `f` from `E` to `𝕝`, where `𝕜` is a nontrivially normed field, `E` is a normed add commutative group over `𝕜`, and `𝕝` is another nontrivially normed field also forming a normed algebra over `𝕜`, if `f` is analytic at a point `x` then the function defined by the reciprocal of `f` at `x`, `(f x)⁻¹`, is also analytic at `x`, provided that `f x` is not equal to zero. More concisely: If `f` is an analytic, non-zero function from a normed add commutative group `E` to a nontrivially normed field `𝕝`, forming a normed algebra over another nontrivially normed field `𝕜`, then the reciprocal function `(f x)⁻¹` is analytic at `x` in `E` if `f x` is non-zero.
`analyticAt_mul` theorem analyticAt_mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_8} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A] (z : A × A), AnalyticAt 𝕜 (fun x => x.1 * x.2) z The theorem `analyticAt_mul` states that for any nontrivially normed field `𝕜` and any normed algebra `A` over `𝕜`, the multiplication operation in `A` is analytic at any point `z` in `A × A`. In other words, the function that takes a pair of elements from `A` and multiplies them can be represented around every point by a convergent power series. More concisely: For any nontrivially normed field 𝕜 and normed algebra A over 𝕜, the multiplication operation on A is analytic at every point in A × A.
`AnalyticOn.prod` theorem AnalyticOn.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : E → G} {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (fun x => (f x, g x)) s The theorem `AnalyticOn.prod` states that for any non-trivial normed field `𝕜`, normed additive commutative groups `E`, `F`, and `G`, and normed spaces over `𝕜` of `E`, `F`, and `G`, if we have two analytic functions `f` and `g` mapping from `E` to `F` and `G` respectively on a set `s` of `E`, then the function that sends each element of `s` to the ordered pair of `f` and `g` applied to that element is also analytic on `s`. In other words, the Cartesian product of two analytic functions is also analytic. More concisely: Given normed fields 𝕜, normed additive commutative groups E, F, and G, and normed spaces E' (over 𝕜) of E and F' (over 𝕜) of F, if f:E→F and g:E→G are analytic functions on a set s ⊆ E, then the function h:s→F×G sending x ∈ s to (f(x), g(x)) is analytic.
`AnalyticOn.div` theorem AnalyticOn.div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_7} [inst_3 : NontriviallyNormedField 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝} {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → (∀ x ∈ s, g x ≠ 0) → AnalyticOn 𝕜 (fun x => f x / g x) s The theorem `AnalyticOn.div` states that in a nontrivially normed field, if `f` and `g` are both analytic functions on a set `s` and `g` is never zero on `s`, then the function defined by the quotient of `f` and `g` (i.e., `f(x) / g(x)`) is also analytic on `s`. This theorem establishes the analyticity of the quotient of two analytic functions, subject to the condition that the denominator function is not zero. More concisely: In a nontrivially normed field, if `f` and `g` are analytic functions on a set `s` and `g` never equals zero on `s`, then the quotient function `x ↦ f(x) / g(x)` is analytic on `s`.
`AnalyticOn.along_snd` theorem AnalyticOn.along_snd : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {x : E} {s : Set (E × F)}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (fun y => f (x, y)) {y \| (x, y) ∈ s} The theorem `AnalyticOn.along_snd` states that for any nontrivially normed field `𝕜`, normed add commutative group `E`, `F`, `G` and normed space over `𝕜` of `E`, `F`, `G`, given a function `f` that maps from a product of `E` and `F` to `G`, and a set `s` of type `E x F`, if the function `f` is analytic on the set `s`, then the function that maps `y` to `f(x, y)` is analytic on the set of `y` such that `(x, y)` belongs to `s`. In other words, if a function is analytic on a product of two spaces, it remains analytic when we fix the first argument and allow the second argument to vary. More concisely: If a function is analytic on a product set in the product of two normed spaces, then the function restricting to each fiber is analytic.
`AnalyticOn.along_fst` theorem AnalyticOn.along_fst : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {s : Set (E × F)} {y : F}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (fun x => f (x, y)) {x \| (x, y) ∈ s} The theorem `AnalyticOn.along_fst` states that if a function `f` from a product of two types `E` and `F` to a type `G` is analytic on a set `s` of `E × F`, then the function obtained by fixing the second coordinate to any value `y` from `F` is analytic on the set of first coordinates `(x, y)` from `s`. Here, the function `f` and the spaces `E`, `F`, and `G` are all over a nontrivially normed field `𝕜`, and `E`, `F`, `G` are normed add commutative groups over `𝕜`. This theorem essentially says that analyticity of a function on a product space implies analyticity when one of the coordinates is fixed. More concisely: If `f` is an analytic function from a product `E × F` to `G` over a nontrivially normed field `𝕜`, then for any fixed `y` in `F`, the function `x ↦ f(x, y)` is analytic on `E`.
`AnalyticAt.prod` theorem AnalyticAt.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G}, AnalyticAt 𝕜 f e → AnalyticAt 𝕜 g e → AnalyticAt 𝕜 (fun x => (f x, g x)) e The theorem `AnalyticAt.prod` states that for any type `𝕜` which is a nontrivially normed field, types `E`, `F`, and `G` which are normed additive commutative groups over `𝕜`, if we have functions `f : E → F` and `g : E → G` that are analytic at a point `e` in `E`, then the function that maps `x` in `E` to the pair `(f x, g x)` in `F × G` is also analytic at `e`. In simpler terms, the Cartesian product of two functions that have convergent power series expansions at a point, also has a convergent power series expansion at that point. More concisely: If `𝕜` is a nontrivially normed field, `E`, `F`, and `G` are normed additive commutative groups over `𝕜`, and `f : E → F` and `g : E → G` are analytic functions at `e` in `E`, then the function `x ↦ (f x, g x)` from `E` to `F × G` is an analytic function at `e`.
`AnalyticAt.div` theorem AnalyticAt.div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_7} [inst_3 : NontriviallyNormedField 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝} {x : E}, AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → g x ≠ 0 → AnalyticAt 𝕜 (fun x => f x / g x) x The theorem `AnalyticAt.div` states that for any types `𝕜`, `E` and `𝕝` where `𝕜` and `𝕝` are nontrivially normed fields, `E` is a normed add commutative group over `𝕜` and `𝕝` is a normed algebra over `𝕜`, if we have two functions `f` and `g` from `E` to `𝕝` that are both analytic at a point `x` in `E`, and `g` at `x` is not zero, then the function defined as the ratio of `f` to `g` is also analytic at `x`. In simpler terms, if `f` and `g` are analytic functions and `g(x)` is not zero, then the function `f(x)/g(x)` is also analytic at point `x`. More concisely: If `𝕜`, `E`, and `𝕝` are nontrivially normed fields with `𝕝` being a normed algebra over `𝕜`, and `f` and `g` are analytic functions from `E` to `𝕝` such that `g(x) ≠ 0`, then the quotient function `x ↦ f(x) / g(x)` is analytic at `x`.
`analyticOn_inv` theorem analyticOn_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_7} [inst_1 : NontriviallyNormedField 𝕝] [inst_2 : NormedAlgebra 𝕜 𝕝], AnalyticOn 𝕜 (fun z => z⁻¹) {z \| z ≠ 0} The theorem `analyticOn_inv` states that the function `x⁻¹` (the reciprocal function) is analytic on the set of all points which are not zero. This is true for any non-trivially normed field `𝕜` and `𝕝`, where `𝕝` is a normed algebra over `𝕜`. In other words, for each point in the set excluding zero, the reciprocal function has a Taylor series expansion around that point. More concisely: For any non-trivially normed field `𝕜` and normed algebra `𝕝` over `𝕜`, the reciprocal function `x⁻¹` is analytic on the set of all non-zero elements in `𝕝`.
`AnalyticOn.pow` theorem AnalyticOn.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {A : Type u_8} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A} {s : Set E}, AnalyticOn 𝕜 f s → ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => f x ^ n) s This theorem, named `AnalyticOn.pow`, states that for any nontrivially normed field `𝕜`, an additively commutative normed group `E`, a normed space `𝕜 E`, a normed ring `A`, a normed algebra `𝕜 A`, a function `f` from `E` to `A`, and a set `s` of `E`, if the function `f` is analytic on the set `s`, then for any natural number `n`, the function that maps `x` in `E` to the `n`th power of `f(x)` in `A` is also analytic on the set `s`. In mathematical terms, this is saying that powers of analytic functions in a normed `𝕜`-algebra are also analytic. More concisely: If `f` is an analytic function from a normed group `E` to a normed algebra `𝕜A` over a nontrivially normed field `𝕜`, then the `n`th power `x ↦ f(x) ^ n` is also an analytic function from `E` to `𝕜A`.
`AnalyticOn.mul` theorem AnalyticOn.mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {A : Type u_8} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A} {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (fun x => f x * g x) s This theorem states that the multiplication of two analytic functions, which are valued in a normed `𝕜`-algebra, is also an analytic function. More specifically, given a nontrivially normed field `𝕜`, a normed additive commutative group `E`, an associated normed space `𝕜E`, a normed ring `A`, a normed algebra `𝕜A`, two functions `f` and `g` from `E` to `A`, and a set `s` of `E` values; if `f` and `g` are both analytic on `s`, then the function that maps `x` in `E` to the product of `f(x)` and `g(x)` in `A` is also analytic on `s`. More concisely: Given two analytic functions from a normed additive commutative group to a normed `𝕜`-algebra over a nontrivially normed field `𝕜`, their product is also an analytic function.
`AnalyticOn.smul` theorem AnalyticOn.smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕝 : Type u_7} [inst_5 : NontriviallyNormedField 𝕝] [inst_6 : NormedAlgebra 𝕜 𝕝] [inst_7 : NormedSpace 𝕝 F] [inst_8 : IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (fun x => f x • g x) s The theorem `AnalyticOn.smul` states that, for any set `s` of elements of type `E`, and any two functions `f` and `g` from `E` to types `𝕝` and `F`, respectively, if `f` and `g` are both analytic on `s`, then their scalar multiplication function (i.e., the function that, for each `x` in `E`, maps `x` to `f(x) * g(x)`) is also analytic on `s`. This theorem assumes that `𝕜` and `𝕝` form non-trivially normed fields, `E` and `F` form normed additive commutative groups, `𝕜` and `𝕝` are scalar fields for `E` and `F`, and `𝕜`, `𝕝` and `F` form a scalar tower, which means that the scalar multiplication in `F` by `𝕜` through `𝕝` is compatible with the scalar multiplication by `𝕝`. More concisely: If `s` is a set of elements from normed additive commutative groups `E` and `F` carrying the structures of normed additive commutative groups and scalar towers over non-trivially normed fields `𝕜` and `𝕝`, respectively, then the scalar multiplication function `x => f(x) * g(x)` is analytic on `s` for any two analytic functions `f : E -> 𝕝` and `g : E -> F`.
`analyticAt_smul` theorem analyticAt_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_7} [inst_3 : NontriviallyNormedField 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] [inst_5 : NormedSpace 𝕝 E] [inst_6 : IsScalarTower 𝕜 𝕝 E] (z : 𝕝 × E), AnalyticAt 𝕜 (fun x => x.1 • x.2) z The theorem `analyticAt_smul` asserts that scalar multiplication is analytic in both its variables. In other words, for any non-trivially normed fields 𝕜 and 𝕝, normed additive commutative group E, and given that 𝕝 is a normed 𝕜-algebra, E is a normed 𝕝-space, and 𝕜, 𝕝, E form a scalar tower, if we take an ordered pair `z` from 𝕝 × E, then the function `f(x)` that multiplies the elements of `x` (i.e., `x.1 • x.2`) is analytic at `z`. This means that there exists a convergent power series expansion around `z` for this function. The theorem note also mentions the possibility of replacing 𝕜' with a "normed module" so that a different theorem `analyticAt_mul` becomes a special case of this theorem, but this has not been implemented yet. More concisely: For any non-trivially normed fields 𝕜 and 𝕝, and a normed additive commutative group E that is a normed 𝕝-space over the scalar tower (𝕜, 𝕝, E), the function `f(x)` defined as `x.1 • x.2` is analytic at any point `z` in 𝕝 × E.
`AnalyticAt.comp₂` theorem AnalyticAt.comp₂ : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {h : F × G → H} {f : E → F} {g : E → G} {x : E}, AnalyticAt 𝕜 h (f x, g x) → AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (fun x => h (f x, g x)) x The theorem `AnalyticAt.comp₂` states that for a given non-trivially normed field `𝕜` and normed add commutative groups `E`, `F`, `G`, `H` with `𝕜` as their scalar field, if a function `h` from product space `F × G` to `H` is analytic at a point `(f x, g x)`, and the functions `f` and `g` from `E` to `F` and `G` respectively, are analytic at a point `x`, then the composition function `(fun x => h (f x, g x))` which maps `x` to `h (f x, g x)` is also analytic at the point `x`. In other words, the analyticity is preserved under function composition in product spaces. More concisely: If functions `f` and `g` are analytic at a point `x` in normed add commutative groups `E` and `F`, `G`, respectively, over a non-trivially normed field `𝕜`, and the function `h` from `F × G` to `H` is analytic at `(f x, g x)`, then the composition function `(fun x => h (f x, g x))` is analytic at `x` in `E`.
`Finset.analyticOn_sum` theorem Finset.analyticOn_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : α → E → F} {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOn 𝕜 (f n) s) → AnalyticOn 𝕜 (fun z => N.sum fun n => f n z) s This theorem states that finite sums of analytic functions are also analytic. More specifically, for any non-trivially normed field `𝕜` and normed additive commutative groups `E` and `F` (with `E` being a normed space over `𝕜` and similarly for `F`), if we have a function `f` from some set `α` to the set of functions from `E` to `F`, and a set `s` of type `E`, then if every function `f n` is analytic on `s` for all `n` in a finite set `N`, their finite sum is also analytic on `s`. Here, a function is said to be analytic on a set if it is analytic around every point of the set. More concisely: If `f` is a function from a set `α` to the set of functions from a normed space `E` to a normed space `F`, and each `f(n)` is analytic on a set `s` for a finite set of indices `N`, then their finite sum is analytic on `s`.
`Finset.analyticOn_prod` theorem Finset.analyticOn_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A} {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOn 𝕜 (f n) s) → AnalyticOn 𝕜 (fun z => N.prod fun n => f n z) s The theorem `Finset.analyticOn_prod` states that the finite product of analytic functions is also analytic. More specifically, for any type `α`, a type `𝕜` which forms a non-trivial normed field, a type `E` which forms a normed additive commutative group as well as a normed space over `𝕜`, and a type `A` that forms a normed commutative ring and a normed algebra over `𝕜`, if `f` is a function from `α` to `E → A` and `s` is a set of elements of type `E`, then for any finite set `N` of elements of type `α`, if each function `f n` for `n` in `N` is analytic on `s`, then the function which maps `z` to the product of `f n z` for `n` in `N` is also analytic on `s`. More concisely: The finite product of analytic functions, defined over a non-trivial normed field `𝕜`, from a type `α` to a normed commutative ring and algebra `A` over `𝕜`, is analytic if each component function is analytic on a given set `s` in `E`.
`AnalyticOn.inv` theorem AnalyticOn.inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_7} [inst_3 : NontriviallyNormedField 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝} {s : Set E}, AnalyticOn 𝕜 f s → (∀ x ∈ s, f x ≠ 0) → AnalyticOn 𝕜 (fun x => (f x)⁻¹) s The theorem `AnalyticOn.inv` states that for a function `f : E → 𝕝`, defined over a non-trivial normed field `𝕝` and a normed algebra over another non-trivial normed field `𝕜`, if the function `f` is analytic on a set `s` and none of the function values on this set are zero, then the function defined by the reciprocal of `f`, i.e., `x ↦ (f x)⁻¹`, is also analytic on the set `s`. In simpler terms, the reciprocal of an analytic function, that does not take the value zero, is also analytic on the same domain. More concisely: If `f : E → 𝕝` is an analytic function on a non-empty set `s` in a non-trivial normed field `𝕝` over another non-trivial normed field `𝕜`, such that `f(x) ≠ 0` for all `x ∈ s`, then the function `x ↦ (f x)⁻¹` is also analytic on `s`.
`AnalyticAt.pow` theorem AnalyticAt.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {A : Type u_8} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A} {z : E}, AnalyticAt 𝕜 f z → ∀ (n : ℕ), AnalyticAt 𝕜 (fun x => f x ^ n) z This theorem states that for any given non-trivially normed field `𝕜`, normed additive commutative group `E`, and a normed `𝕜`-algebra `A`, if a function `f : E → A` is analytic at a point `z` in `E`, then the function `f` raised to any natural number power `n` is also analytic at that point `z`. In other words, powers of analytic functions are also analytic. This is established within the context of complex analysis and algebra where analyticity involves convergence of a power series expansion around a given point. More concisely: If `f : E -> A` is an analytic function from a normed additive commutative group `E` to a normed `𝕜`-algebra `A` at a point `z in E`, then for every natural number `n`, the `n`-th power `f ^ n` of `f` is also analytic at `z`.
`AnalyticAt.along_snd` theorem AnalyticAt.along_snd : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {p : E × F}, AnalyticAt 𝕜 f p → AnalyticAt 𝕜 (fun y => f (p.1, y)) p.2 The theorem `AnalyticAt.along_snd` states that if a function `f` of type `E × F → G` is analytic at a point `p` in the product space `E × F`, then the function obtained by fixing the first coordinate of `p` and letting the second coordinate vary is also analytic at the second coordinate of `p`. Here, `𝕜` is a nontrivially normed field, and `E`, `F`, and `G` are normed spaces over `𝕜`. This theorem is essentially stating that analyticity in a product space implies analyticity when considering each coordinate separately. More concisely: If `f : E × F → G` is analytic at `(e, f)` in `E × F` over a nontrivially normed field, then the function `g(x) := f(e, x)` is analytic at `x = f` in `F`.
`AnalyticAt.along_fst` theorem AnalyticAt.along_fst : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {p : E × F}, AnalyticAt 𝕜 f p → AnalyticAt 𝕜 (fun x => f (x, p.2)) p.1 This theorem, referred to as `AnalyticAt.along_fst`, states that if a function `f` is analytic at a point `p` in the product space of `E` and `F`, then the function that takes an element `x` of `E` to `f(x, p.2)` (i.e., maps `x` to `f` evaluated at the pair `(x, p.2)`) is analytic at `p.1`. In other words, an analytic function on a product space remains analytic when evaluated along fixed values of the second component of the domain. Here, the term "analytic" is used to indicate that the function admits a convergent power series expansion around the given point. More concisely: If a function `f : E × F → ℝ` is analytic at `(p.1, p.2)` in the product space `E × F`, then the function `x ↦ f(x, p.2)` is analytic at `p.1` in `E`.
`FormalMultilinearSeries.radius_prod_eq_min` theorem FormalMultilinearSeries.radius_prod_eq_min : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G), (p.prod q).radius = min p.radius q.radius This theorem states that for any nontrivially normed field 𝕜 and normed space E, F, G, the radius of the Cartesian product of two formal multilinear series (p and q) over these fields and spaces, is the minimum of the radii of p and q. In the context of analysis on normed spaces, this result provides a rule for the radius of convergence when combining series in this specific way. More concisely: The radius of convergence of the Cartesian product of two normed multilinear series over a nontrivially normed field is the minimum of their individual radii of convergence.
`Finset.analyticAt_sum` theorem Finset.analyticAt_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : α → E → F} {c : E} (N : Finset α), (∀ n ∈ N, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (fun z => N.sum fun n => f n z) c This theorem states that if we have a finite set of functions, all of which are analytic at a point `c`, then the sum of these functions is also analytic at that point `c`. Here, a function is considered analytic at a point if it can be expressed as a convergent power series around that point. This property is being defined for functions from a normed space over a nontrivially normed field to another such normed space. The theorem is a standard result in complex analysis and is fundamental to many further results in analysis and differential equations. More concisely: If `{f_i : X → Y}` is a finite family of analytic functions at point `c` in the normed spaces X and Y over a nontrivially normed field, then their sum `∑ i, f_i` is also analytic at point `c`.

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Analytic.Constructions

`Finset.analyticAt_prod`

`analyticAt_inv`

theorem analyticAt_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_7} [inst_1 : NontriviallyNormedField 𝕝] [inst_2 : NormedAlgebra 𝕜 𝕝] {z : 𝕝}, z ≠ 0 → AnalyticAt 𝕜 Inv.inv z

`AnalyticOn.comp₂`

`AnalyticAt.smul`

`AnalyticAt.mul`

`AnalyticAt.inv`

`analyticAt_mul`

theorem analyticAt_mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_8} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A] (z : A × A), AnalyticAt 𝕜 (fun x => x.1 * x.2) z

`AnalyticOn.prod`

`AnalyticOn.div`

`AnalyticOn.along_snd`

`AnalyticOn.along_fst`

`AnalyticAt.prod`

`AnalyticAt.div`

`analyticOn_inv`

theorem analyticOn_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_7} [inst_1 : NontriviallyNormedField 𝕝] [inst_2 : NormedAlgebra 𝕜 𝕝], AnalyticOn 𝕜 (fun z => z⁻¹) {z | z ≠ 0}

`AnalyticOn.pow`

`AnalyticOn.mul`

`AnalyticOn.smul`

`analyticAt_smul`

`AnalyticAt.comp₂`

`Finset.analyticOn_sum`

`Finset.analyticOn_prod`

`AnalyticOn.inv`

`AnalyticAt.pow`

`AnalyticAt.along_snd`

`AnalyticAt.along_fst`

`FormalMultilinearSeries.radius_prod_eq_min`

`Finset.analyticAt_sum`