analyticOn_id
theorem analyticOn_id :
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {s : Set E}, AnalyticOn 𝕜 (fun x => x) s
The theorem `analyticOn_id` states that for any type `𝕜` which is a nontrivially normed field, any type `E` which is a normed additive commutative group on which `𝕜` acts as a normed space, and any set `s` of elements of type `E`, the identity function (i.e., the function that maps each element to itself) is analytic on the set `s`. In other words, the identity function is analytic at every point in the set. The term "analytic" here refers to the property of a function that it can be expressed as a power series in a neighborhood of each point in its domain.
More concisely: For any nontrivially normed field `𝕜`, normed additive commutative group `E` over `𝕜`, and set `s` in `E`, the identity function on `s` is analytic as a power series in `𝕜`.
|
analyticAt_fst
theorem analyticAt_fst :
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
AnalyticAt 𝕜 (fun p => p.1) p
The theorem `analyticAt_fst` states that for any non-trivially normed field `𝕜`, any normed additive commutative group `E`, any normed space over `𝕜` and `E`, any normed additive commutative group `F`, any normed space over `𝕜` and `F`, and any point `p` in the product space `E × F`, the function `fst` (which takes a pair and returns its first component) is analytic at `p`. In other words, the function `fst` admits a convergent power series expansion around `p`.
More concisely: For any non-trivially normed fields 𝕜, normed additive commutative groups E and F, and any point p in the product space E × F, the function fst, which maps (x, y) to x, is analytic at p.
|
analyticAt_snd
theorem analyticAt_snd :
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
AnalyticAt 𝕜 (fun p => p.2) p
The theorem `analyticAt_snd` states that for any type 𝕜, which forms a non-trivially normed field, and any types E and F, which are normed additive commutative groups and also form normed spaces over 𝕜, the function `snd` is analytic at any point p in the product space E × F. Here, `snd` is a function that takes a pair and returns its second component. In more mathematical terms, the function `snd` admits a convergent power series expansion around any point in the product space E × F.
More concisely: For any non-trivially normed field 𝕜 and normed additive commutative groups E and F as normed spaces over 𝕜, the function `snd` on E × F is analytic.
|
analyticAt_id
theorem analyticAt_id :
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] (z : E), AnalyticAt 𝕜 id z
The theorem `analyticAt_id` states that for any nontrivial normed field `𝕜` and any normed add commutative group `E` that is also a normed space over `𝕜`, the identity function is analytic at any point `z` in `E`. In mathematical terms, this means the identity function has a convergent power series expansion around every point in its domain.
More concisely: For any nontrivial normed field `𝕜` and normed add commutative group `E` that is also a normed space over `𝕜`, the identity function on `E` is analytic at every point in `E`.
|
analyticOn_snd
theorem analyticOn_snd :
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{s : Set (E × F)}, AnalyticOn 𝕜 (fun p => p.2) s
This theorem, `analyticOn_snd`, states that for any non-trivially normed field `𝕜`, any normed add commutative group `E`, any normed space over `𝕜` and `E`, any normed add commutative group `F`, any normed space over `𝕜` and `F`, and any set `s` of pairs `(E, F)`, the function that takes a pair `(E, F)` and returns `F` (the second element of the pair) is analytic on the set `s`. In other words, this function is analytic around every point of the set `s`.
More concisely: For any non-trivially normed field `𝕜`, and sets `s` of pairs of normed add commutative groups `(E, F)` over `𝕜`, the second projection function `λ (E, F) : F` is analytic on `s`.
|
analyticOn_fst
theorem analyticOn_fst :
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{s : Set (E × F)}, AnalyticOn 𝕜 (fun p => p.1) s
This theorem states that the `fst` function, which extracts the first component of a pair, is analytic on any set `s`. In this context, `𝕜` is a nontrivially normed field, `E` and `F` are normed additive commutative groups over `𝕜`, and `s` is a set of pairs of elements from `E` and `F`. Being analytic means that the function can be locally represented as a power series, and in this case, the theorem states this holds for any point in the set `s`.
More concisely: The function `fst`: `(E × F) → E` is analytic on any set `s ⊆ E × F` over a nontrivially normed field `𝕜`.
|
ContinuousLinearMap.analyticAt
theorem ContinuousLinearMap.analyticAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(f : E →L[𝕜] F) (x : E), AnalyticAt 𝕜 (⇑f) x
The theorem `ContinuousLinearMap.analyticAt` states that for any given continuous linear map `f` from a type `E` to another type `F` over a nontrivially normed field `𝕜`, the map `f` is analytic at any point `x` in `E`. In other words, the function `f` admits a convergent power series expansion around any point `x`.
More concisely: For any continuous linear map `f` from a nontrivially normed vector space `E` to `F` over a field `𝕜`, `f` is analytic at every point `x` in `E`, i.e., it admits a convergent power series expansion around `x`.
|