HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub
theorem HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E},
HasFPowerSeriesAt f p x →
(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[nhds (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
This theorem states that if a function `f` has a formal power series representation `∑ n, pₙ` at a point `x`, then the deviation of `f` at points `(y, z)` from its linear approximation given by `f y - f z - p 1 (fun _ ↦ y - z)` is dominated by the product `‖(y, z) - (x, x)‖ * ‖y - z‖` in the limit as `(y, z)` approaches `(x, x)`. This is expressed using Big O notation as `f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)`. The consequence of this theorem is that `f` is strictly differentiable at `x`.
More concisely: If a function `f` has a power series representation `∑ n, pₙ` at a point `x`, then `f` is strictly differentiable at `x`, and the deviation of `f` from its linear approximation is dominated by `‖(y, z) - (x, x)‖ * ‖y - z‖` as `(y, z)` approaches `(x, x)`. (Expressed using Big O notation: `f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)`)
|
isOpen_analyticAt
theorem isOpen_analyticAt :
∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
(f : E → F), IsOpen {x | AnalyticAt 𝕜 f x}
This theorem states that, for any function `f` from a normed vector space to a Banach space, the set of points `x` at which `f` is analytic is an open set in the topological space. Here, a function `f` is considered analytic at a point `x` if it can be represented by a convergent power series around `x`. The underlying field for the spaces is denoted by 𝕜, which is assumed to be a Nontrivially normed field. This theorem hence establishes the topological property of the set of all points where a function is analytic.
More concisely: The set of points in a normed vector space where a function from the space to a Banach space is analytic is an open set.
|
FormalMultilinearSeries.changeOrigin_radius
theorem FormalMultilinearSeries.changeOrigin_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {x : E}, p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius
This theorem states that for any formal multilinear series `p`, and any vector `x` in the domain of `p`, the radius of convergence of the series after changing the origin to `x` is at least `p.radius - ‖x‖`. In other words, the series `p.changeOrigin x` is well defined on the largest ball that is contained within the original ball of convergence. This theorem holds in any normed space over a nontrivially normed field.
More concisely: For any multilinear series `p` and vector `x` in a normed space over a nontrivially normed field, the radius of convergence of `p` after changing the origin to `x` is at least `p.radius - ‖x‖`.
|
AnalyticOn.continuous
theorem AnalyticOn.continuous :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
AnalyticOn 𝕜 f Set.univ → Continuous f
This theorem states that if a function `f` from a normed additive commutative group `E` to another normed additive commutative group `F` is analytic everywhere on the domain `E` over a nontrivially normed field `𝕜`, then the function `f` is continuous. In other words, a function that is analytic at every point in its domain is also continuous. This domain is expressed as `Set.univ`, which represents the universal set containing all elements of `E`. The field, `𝕜`, is characterized as being nontrivially normed, meaning it is a field with a norm that is not constantly zero. The groups `E` and `F` are both normed and additive commutative, a structure that allows for the addition operation and the assignment of a length or size (norm) to each vector in the group.
More concisely: If `f` is an analytic function from the normed additive commutative group `E` to the normed additive commutative group `F` over a nontrivially normed field `𝕜`, then `f` is continuous.
|
FormalMultilinearSeries.min_radius_le_radius_add
theorem FormalMultilinearSeries.min_radius_le_radius_add :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p q : FormalMultilinearSeries 𝕜 E F), min p.radius q.radius ≤ (p + q).radius
This theorem states that for any two formal multilinear series `p` and `q` over a nontrivially normed field `𝕜`, with `E` and `F` as normed additive commutative groups, and `E` and `F` as normed spaces over `𝕜`, the radius of their sum `(p + q)` is at least as large as the minimum of their individual radii. In other words, the minimum of the radii of `p` and `q` is less than or equal to the radius of their sum.
More concisely: For any two formal multilinear series $p$ and $q$ over a nontrivially normed field $\mathbb{K}$, the radius of their sum $(p + q)$ is greater than or equal to the minimum of the radii of $p$ and $q$.
|
FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius
theorem FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
↑r < p.radius → ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
The theorem `FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius` states that for a nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, and a formal multilinear series `p` from `𝕜` and `E` to `F`, if `r` is a nonnegative real number strictly less than the radius of `p`, then the norm of `pₙ` times `r` to the power of `n` tends to zero exponentially. More specifically, there exist some `0 < a < 1` and `C > 0` such that for all natural numbers `n`, the inequality `‖p n‖ * r ^ n ≤ C * a ^ n` holds.
More concisely: For a nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, and a formal multilinear series `p` from `𝕜` and `E` to `F`, if `r` is a nonnegative real number strictly less than the radius of `p`, then there exist `0 < a < 1` and `C > 0` such that `‖p(n)‖ * rⁱ(n) ≤ C * aⁱ(n)` for all natural numbers `n`.
|
FormalMultilinearSeries.le_mul_pow_of_radius_pos
theorem FormalMultilinearSeries.le_mul_pow_of_radius_pos :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F),
0 < p.radius → ∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
This theorem states that for any formal multilinear series `p` over a nontrivially normed field `𝕜`, with `E` and `F` as normed additively commutative groups and `𝕜` as their normed spaces, if the radius of `p` is positive, then there exist positive constants `C` and `r` such that the norm of the nth term of `p` (`‖p n‖`) is less than or equal to `C` times `r` raised to the power `n` for every natural number `n`. This implies that the growth of `‖pₙ‖` is at most geometric.
More concisely: For any formal multilinear series `p` over a nontrivially normed field, if its radius is positive then there exist constants `C` and `r` such that the norm of its `n`-th term is bounded by `C * r^n` for all natural numbers `n`.
|
FormalMultilinearSeries.partialSum_continuous
theorem FormalMultilinearSeries.partialSum_continuous :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
[inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
[inst_7 : TopologicalAddGroup E] [inst_8 : TopologicalAddGroup F] [inst_9 : ContinuousConstSMul 𝕜 E]
[inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), Continuous (p.partialSum n)
This theorem states that the partial sums of a formal multilinear series are continuous. More specifically, given a formal multilinear series `p` over a ring `𝕜`, with the domain being a topological additive group `E` and the codomain being another topological additive group `F`, the function that computes the `n`-th partial sum of `p` is a continuous function. Here, `E` and `F` are modules over `𝕜`, and the scalar multiplication in `E` and `F` is assumed to be continuous.
More concisely: The function that computes the `n`-th partial sum of a formal multilinear series over a ring is a continuous function between the topological additive groups of the series' domains and codomains, assuming the domain and codomain scalar multiplications are continuous.
|
FormalMultilinearSeries.changeOrigin_eval
theorem FormalMultilinearSeries.changeOrigin_eval :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
(p : FormalMultilinearSeries 𝕜 E F) {x y : E},
↑‖x‖₊ + ↑‖y‖₊ < p.radius → (p.changeOrigin x).sum y = p.sum (x + y)
This theorem states that for any Formal Multilinear Series `p` over a Nontrivially Normed Field `𝕜`, with Normed Additive Commutative Groups `E` and `F` and Normed Spaces `𝕜 E` and `𝕜 F`, and given that `F` is a Complete Space, the sum of the series `p.changeOrigin x` at a point `y` equals `p.sum (x + y)`, provided the sum of the norms of `x` and `y` is less than the radius of the Formal Multilinear Series `p`.
More concisely: For any formal multilinear series $p$ over a nontrivially normed field, if $x, y \in E$, $F$ is complete, and $\|x + y situation situation situation situation situation < \|p\|_r$, then $\sum\_{i=0}\^n p.changeOrigin x i = p.sum (x + y)$.
|
AnalyticAt.add
theorem AnalyticAt.add :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (f + g) x
The theorem `AnalyticAt.add` states that if `f` and `g` are two functions of type `E → F` that are analytic at a point `x`, then their sum `f + g` is also analytic at the same point `x`. Here, `𝕜` is a nontrivially normed field, `E` and `F` are normed add commutative groups over `𝕜`, and `E` and `F` are also normed spaces over `𝕜`. In the mathematical terms, it implies that the sum of two analytic functions is also an analytic function.
More concisely: If `f : E -> F` and `g : E -> F` are analytic functions at a point `x in E` over a nontrivially normed field `𝕜`, then their sum `f + g` is also an analytic function at `x`.
|
FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero
theorem FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), (∀ (m : ℕ), p (m + n) = 0) → p.radius = ⊤
This theorem states that for any normed fields 𝕜, normed additive commutative group E, normed space 𝕜 E, normed additive commutative group F, normed space 𝕜 F, and a given formal multilinear series 'p', if all the mth terms of the series 'p' after addition with a natural number 'n' results in zero, then the radius of convergence of the formal multilinear series 'p' is the mathematical entity 'top' (which usually represents infinity).
More concisely: If the sum of all terms of degree greater than or equal to a certain natural number in a formal multilinear series over a normed field is zero for all normed spaces involved, then the radius of convergence is infinite.
|
hasFPowerSeriesAt_iff
theorem hasFPowerSeriesAt_iff :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in nhds 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))
The theorem `hasFPowerSeriesAt_iff` states that for a function `f : 𝕜 → E` from a non-trivially normed field to a normed and commutative additive group, a formal multilinear series `p` is a power series expansion at a point `z₀` if and only if it equals the sum of `p` in a neighborhood of `z₀`. This formulation simplifies some proofs by abstracting the dependence of `HasFPowerSeriesAt` on the radius of `p`. In other words, for all points `z` in the neighborhood of 0, the sum of the elements `z^n` times the `n`-th coefficient of `p` equals the function value of `f` at `z₀ + z`.
More concisely: A formal multilinear series is a power series expansion at a point in a non-trivially normed field if and only if it equals the sum of scaled series coefficients and function evaluations at that point in a neighborhood of the point.
|
FormalMultilinearSeries.isLittleO_of_lt_radius
theorem FormalMultilinearSeries.isLittleO_of_lt_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
↑r < p.radius → ∃ a ∈ Set.Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun x => a ^ x
This theorem states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F`, any normed space over `𝕜` of `E` and `F`, and any formal multilinear series `p` from `𝕜` to `E` to `F`, if `r` is a nonnegative real number strictly smaller than the radius of convergence of `p`, then the sequence `‖p n‖ * ↑r ^ n` tends to zero exponentially fast. In other words, there exists a number `a` strictly between 0 and 1 such that the rate of decay of `‖p n‖ * ↑r ^ n` as `n` goes to infinity is at least as fast as that of `a ^ n`.
More concisely: For any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F`, normed space `X` over `𝕜` of `E` and `F`, and multilinear series `p` from `𝕜` to `E` to `F`, if `r` is a strict radius of convergence and `a` is a number strictly between 0 and 1, then `‖p n‖ * ↑r ^ n` decreases exponentially faster than `a ^ n` as `n` goes to infinity.
|
HasFPowerSeriesOnBall.image_sub_sub_deriv_le
theorem HasFPowerSeriesOnBall.image_sub_sub_deriv_le :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal},
HasFPowerSeriesOnBall f p x r →
r' < r →
∃ C,
∀ y ∈ EMetric.ball x r',
∀ z ∈ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
This theorem states that if a function `f` has a formal power series `∑ n, pₙ` on a ball of radius `r`, then for any `y, z` in a smaller ball of radius `r'`, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`, for some constant `C`. That is, the difference between the function values at `y` and `z` and the first term of the power series expansion is controlled by the distances of `y` and `z` to the center of the ball, and the distance between `y` and `z` itself. This theorem is related to the estimate of the error when approximating a function by its formal power series in a ball in a normed space.
More concisely: Given a function `f` with a formal power series `∑ n, pₙ` on a ball of radius `r`, there exists a constant `C` such that for all `y, z` in a smaller ball of radius `r'`, the norm of `f y - f z - p 1 (fun _ ↦ y - z)` is bounded by `C * (max ‖y - x‖, ‖z - x‖) * ‖y - z‖`.
|
FormalMultilinearSeries.hasFPowerSeriesOnBall
theorem FormalMultilinearSeries.hasFPowerSeriesOnBall :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
(p : FormalMultilinearSeries 𝕜 E F), 0 < p.radius → HasFPowerSeriesOnBall p.sum p 0 p.radius
This theorem states that in a complete space, if we have a power series `p` that converges, the sum of this power series also admits `p` as a power series within the radius of convergence. This property is not straightforward because it requires verification of the convergence of the series. The theorem is applicable to a broad range of types `𝕜`, `E`, and `F`, which represent a non-trivially normed field, a normed add commutative group, and a normed space, respectively. The type `F` is also required to be a complete space.
More concisely: In a complete normed space, a convergent power series is equal to its sum as power series within the radius of convergence.
|
ContinuousLinearMap.comp_hasFPowerSeriesOnBall
theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[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}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (g : F →L[𝕜] G),
HasFPowerSeriesOnBall f p x r → HasFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x r
This theorem states that if a function `f` has a power series `p` on a specific ball in a nontrivially normed field, and if `g` is a linear transformation, then the composition of `g` and `f` also has a power series on that same ball. The power series for the composite function is given by the composition of `g` and the power series `p`. This holds for all types `𝕜`, `E`, `F`, and `G` such that `𝕜` is a nontrivially normed field, `E`, `F`, and `G` are normed add commutative groups, and `E`, `F`, and `G` are normed spaces over `𝕜`.
More concisely: If `f : E → F` has a power series `p` on a ball in the nontrivially normed field `𝕜`, then the composition `g ∘ f` has a power series equal to `g ∘ p` on that ball, where `g : G → H` is a linear transformation.
|
FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius
theorem FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, ↑r < p.radius → ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
This theorem states that for a given formal multilinear series `p` over a nontrivially normed field `𝕜` with source normed additive commutative group `E` and target normed additive commutative group `F`, if `r` (a nonnegative real number) is strictly smaller than the radius of `p`, then the norm of the `n`th term of `p` multiplied by `r` to the power of `n` is bounded. Specifically, there exists a positive constant `C` such that for all natural numbers `n`, the norm of the `n`th term of `p` multiplied by `r` to the power of `n` is less than or equal to `C`.
More concisely: For a formal multilinear series $p$ over a nontrivially normed field $\mathbb{K}$ with source and target normed additive commutative groups $E$ and $F$, respectively, there exists a constant $C$ such that for all natural numbers $n$, the norm of the $n$th term of $p$ multiplied by $r^n$ is bounded by $C$, where $r$ is a real number strictly smaller than the radius of $p$.
|
FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius
theorem FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
0 < r → ↑r < p.radius → ∃ C > 0, ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
This theorem states that for a given formal multilinear series `p` over a nontrivial normed field `𝕜`, with spaces `E` and `F` equipped with a normed group structure and a normed space structure over `𝕜`, if `r` is a positive real number that is strictly smaller than the radius of convergence of `p`, then there exists a positive constant `C` such that for each natural number `n`, the norm of the `n`th term of the series is less than or equal to `C` divided by `r` to the power of `n`. In other words, the size of the terms of the series decreases at least as quickly as `r^n` for `n` large enough.
More concisely: For a formal multilinear series `p` over a nontrivial normed field `𝕜`, if `r` is a radius of convergence strictly smaller than `p`, then there exists a constant `C` such that for all natural numbers `n`, the norm of the `n`-th term of `p` is bounded by `C / r^n`.
|
HasFPowerSeriesOnBall.analyticAt_of_mem
theorem HasFPowerSeriesOnBall.analyticAt_of_mem :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
{f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r → y ∈ EMetric.ball x r → AnalyticAt 𝕜 f y
This theorem states that if a function `f` from a normed space `E` to a complete space `F` over a nontrivially normed field `𝕜` has a power series expansion `p` on an open ball `B(x, r)`, then `f` is analytic at every point `y` within this ball. In mathematical terms, if `f : E → F` admits a power series expansion on an open ball centered at `x` with radius `r`, then `f` is analytic at any point `y` such that the extended metric distance from `y` to `x` is less than `r`.
More concisely: If a function `f : E → F` from a normed space `E` to a complete space `F` over a nontrivially normed field `𝕜` has a power series expansion on an open ball `B(x, r)` in `E`, then `f` is analytic on `B(x, r)`.
|
HasFPowerSeriesOnBall.mono
theorem HasFPowerSeriesOnBall.mono :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal},
HasFPowerSeriesOnBall f p x r → 0 < r' → r' ≤ r → HasFPowerSeriesOnBall f p x r'
The theorem `HasFPowerSeriesOnBall.mono` states that for any types `𝕜`, `E`, and `F`, where `𝕜` is a nontrivially normed field, `E` and `F` are normed add commutative groups and `E`, `F` are also normed spaces over `𝕜`. Consider a function `f` from `E` to `F`, a formal multilinear series `p` of types `𝕜`, `E`, and `F`, and points `x` in `E` and `r`, `r'` in the extended nonnegative reals `ENNReal`. If `f` has a power series expansion `p` on a ball in `E` centered at `x` with radius `r`, and `r'` is a nonnegative real number that is less than or equal to `r` and greater than zero, then `f` also has a power series expansion `p` on a ball in `E` centered at `x` with radius `r'`.
More concisely: If `f : E → F` is a function with a power series expansion on the ball `B(x, r)` in the normed spaces `E` and `F` over the nontrivially normed field `𝕜`, then `f` also has a power series expansion on the smaller ball `B(x, r')` for any `r' < r > 0`.
|
HasFPowerSeriesAt.apply_eq_zero
theorem HasFPowerSeriesAt.apply_eq_zero :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F} {x : E},
HasFPowerSeriesAt 0 p x → ∀ (n : ℕ) (y : E), ((p n) fun x => y) = 0
This theorem states that if a formal multilinear series `p` represents the zero function at a point `x` in a normed vector space `E`, then the terms `p n (fun i ↦ y)` in the sum of the series are zero for any natural number `n` and any element `y` of `E`. Here, `𝕜` is a nontrivial normed field, `E` and `F` are normed vector spaces over `𝕜`, and `p` is a formal multilinear series from `E` to `F`.
More concisely: If a multilinear series `p` from a normed vector space `E` to another normed vector space `F` over a nontrivial normed field `𝕜` represents the zero function at a point `x` in `E`, then for all natural numbers `n` and elements `y` in `E`, the terms `p n (fun i ↦ y)` in the series expansion of `p` are zero.
|
HasFPowerSeriesOnBall.continuousOn
theorem HasFPowerSeriesOnBall.continuousOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r → ContinuousOn f (EMetric.ball x r)
The theorem `HasFPowerSeriesOnBall.continuousOn` states that for any function `f` mapping from a normed space `E` over a nontrivially normed field `𝕜` to a normed space `F` over the same field, if the function `f` has a power series expansion `p` on a disk in `E` centered at a point `x` with a non-negative extended real number radius `r`, then the function `f` is continuous on the disk. Here, the disk is defined as the set of all points whose extended metric distance to the center `x` is less than the radius `r`.
More concisely: If a function `f` from a normed space `E` to a normed space `F` over a nontrivially normed field has a convergent power series expansion on the disk centered at `x` with radius `r`, then `f` is continuous on the disk.
|
FormalMultilinearSeries.analyticAt_changeOrigin
theorem FormalMultilinearSeries.analyticAt_changeOrigin :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
(p : FormalMultilinearSeries 𝕜 E F), p.radius > 0 → ∀ (n : ℕ), AnalyticAt 𝕜 (fun x => p.changeOrigin x n) 0
This theorem states that for any formal multilinear series `p` from a normed space `E` over a nontrivially normed field `𝕜` to a normed space `F`, if the radius of `p` is greater than zero, then the function defined by changing the origin of `p` to `x` and taking the nth term is analytic at zero. Here, a function is said to be analytic at a point if it admits a convergent power series expansion around that point. The analytic nature of the function is maintained as we vary the origin. This is applicable in the setting where `F` is a complete space.
More concisely: If `p` is a formal multilinear series from a normed space `E` over a nontrivially normed field `𝕜` to a complete normed space `F` with positive radius, then the function `x ↦ p(x - origin) coefficients[n] p(x)` is analytic at `origin`.
|
HasFPowerSeriesAt.congr
theorem HasFPowerSeriesAt.congr :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E},
HasFPowerSeriesAt f p x → (nhds x).EventuallyEq f g → HasFPowerSeriesAt g p x
The theorem `HasFPowerSeriesAt.congr` states that for any nontrivially normed field `𝕜`, normed additive commutative groups `E` and `F`, normed spaces over `𝕜` for `E` and `F`, and functions `f` and `g` from `E` to `F`, together with a formal multilinear series `p` and an element `x` of `E`, if `f` has a power series representation `p` at `x`, and `f` equals `g` in a neighborhood of `x`, then `g` also has the power series representation `p` at `x`. This theorem essentially says that local equality of functions in a neighborhood implies the same power series representation.
More concisely: If `nontrivially normed fields 𝕜`, normed additive commutative groups `E` and `F`, normed spaces over `𝕜` for `E` and `F`, functions `f: E → F` and `g: E → F`, formal multilinear series `p`, and element `x` in `E` satisfy `f = g` in a neighborhood of `x` and `f` has power series representation `p` at `x`, then `g` also has power series representation `p` at `x`.
|
HasFPowerSeriesOnBall.analyticAt
theorem HasFPowerSeriesOnBall.analyticAt :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal}, HasFPowerSeriesOnBall f p x r → AnalyticAt 𝕜 f x
This theorem states that for any given function `f` mapping from a normed vector space `E` to another normed vector space `F` over a nontrivially normed field `𝕜`, if `f` has a formal power series expansion `p` on an open ball centered at `x` with radius `r` (which is an extended nonnegative real number), then `f` is analytic at `x`. This defines the notion of local analyticity, i.e., the function `f` is locally represented by a power series.
More concisely: Given a function `f` from a normed vector space `E` to another normed vector space `F` over a nontrivially normed field `𝕜`, if `f` has a convergent power series expansion `p` on an open ball centered at `x` in `E` with radius `r`, then `f` is analytic at `x`.
|
HasFPowerSeriesAt.isBigO_sub_partialSum_pow
theorem HasFPowerSeriesAt.isBigO_sub_partialSum_pow :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E},
HasFPowerSeriesAt f p x → ∀ (n : ℕ), (fun y => f (x + y) - p.partialSum n y) =O[nhds 0] fun y => ‖y‖ ^ n
This theorem states that for a Taylor formula of an analytic function in the context of big O notation (`IsBigO`), given a nontrivially normed field `𝕜`, normed additive commutative groups `E` and `F` which are also normed spaces over `𝕜`, a function `f : E → F`, a formal multilinear series `p : FormalMultilinearSeries 𝕜 E F`, and a point `x : E`. If `f` has a power series at point `x` which is represented by `p`, then for any natural number `n`, the function `(fun y => f (x + y) - p.partialSum n y)` is big O of the function `(fun y => ‖y‖ ^ n)` with respect to the neighborhood of 0. In simpler terms, the error between the function value and its n-th partial sum from the Taylor series is bounded by the n-th power of the distance to the point of expansion, as the distance tends to 0.
More concisely: Given an analytic function `f` with a power series expansion `p` at point `x` in normed spaces `E` and `F` over a nontrivially normed field `𝕜`, the error between `f(x+y)` and `p.partialSum n y` is big O of `‖y‖^n` as `y` approaches 0.
|
HasFPowerSeriesOnBall.changeOrigin
theorem HasFPowerSeriesOnBall.changeOrigin :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
{f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r → ↑‖y‖₊ < r → HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖y‖₊)
Given a function `f` that admits a power series expansion `p` on a ball `B(x, r)` in a normed space, the theorem states that `f` also admits a power series on any subball of `B(x, r)`, even if the center of the subball is different. The new power series is given by `p.changeOrigin y` where `y` is the center of the new subball. The new subball has radius `r - ||y||₊` and is centered at `x + y`. This holds for any nontrivially normed field `𝕜`, normed add commutative groups `E` and `F` and normed spaces `E` and `F` over `𝕜`, provided that `F` is complete.
More concisely: Given a function `f` with power series expansion `p` on a ball `B(x, r)` in a normed space, the power series `p.changeOrigin y` defines `f` on any subball of `B(x, r)` with center `x + y` and radius `r - ||y||₊`, where `𝕜` is a nontrivially normed field, `E` and `F` are normed add commutative groups and normed spaces over `𝕜` with `F` complete.
|
FormalMultilinearSeries.lt_radius_of_isBigO
theorem FormalMultilinearSeries.lt_radius_of_isBigO :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
r ≠ 0 →
∀ {a : ℝ}, a ∈ Set.Ioo (-1) 1 → ((fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => a ^ x) → ↑r < p.radius
This theorem states that given a formal multilinear series `p` over a non-trivially normed field `𝕜` with normed additive commutative groups `E` and `F` forming normed spaces over `𝕜`, if for a nonnegative real number `r` (which is not zero) the norm of `pₙ` multiplied by `rⁿ` is big O of `aⁿ` (for some real number `a` in the open interval from `-1` to `1`), as `n` goes to infinity, then `r` is strictly less than the radius of `p`. This theorem connects the growth rate of the norm of the terms in the formal multilinear series with the radius of convergence of the series.
More concisely: If the norm of the n-th term of a formal multilinear series over a non-trivially normed field, multiplied by r^n, is big O of a^n as n goes to infinity, then r is strictly less than the radius of convergence of the series.
|
FormalMultilinearSeries.le_radius_of_bound
theorem FormalMultilinearSeries.le_radius_of_bound :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) (C : ℝ) {r : NNReal}, (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C) → ↑r ≤ p.radius
This theorem states that given a formal multilinear series `p` over a nontrivially normed field `𝕜`, a normed additive commutative group `E`, and a normed space `F` with `𝕜` as scalar field (annotated by `[inst : NontriviallyNormedField 𝕜]`, `[inst_1 : NormedAddCommGroup E]`, `[inst_2 : NormedSpace 𝕜 E]`, `[inst_3 : NormedAddCommGroup F]`, and `[inst_4 : NormedSpace 𝕜 F]`), if the series `‖pₙ‖ rⁿ` is bounded by a real number `C` for all natural numbers `n` (written as `∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C`), then the radius of the formal multilinear series `p` is greater than or equal to `r` (written as `↑r ≤ FormalMultilinearSeries.radius p`). Here `r` is a nonnegative real number defined as `NNReal` and the `‖pₙ‖` denotes the norm of `pₙ`.
More concisely: If the norm of the coefficients of a formal multilinear series over a nontrivially normed field is bounded by a constant times the radius raised to the power of the degree for all degrees, then the radius of the series is greater than or equal to the constant.
|
FormalMultilinearSeries.continuousOn
theorem FormalMultilinearSeries.continuousOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F} [inst_5 : CompleteSpace F], ContinuousOn p.sum (EMetric.ball 0 p.radius)
The theorem `FormalMultilinearSeries.continuousOn` states that for any nontrivial normed field `𝕜`, normed additive commutative groups `E` and `F`, which are also normed spaces over `𝕜`, and a formal multilinear series `p` from `E` to `F` where `F` is a complete space, the sum of the series `p` is continuous within its disk of convergence. Specifically, the disk of convergence is described as the set of all points `y` such that the extended metric distance from `y` to zero is less than the radius of `p`.
More concisely: Given a nontrivial normed field `𝕜`, normed additive commutative groups `E` and `F` as normed spaces over `𝕜`, and a formal multilinear series `p` from `E` to `F` with a complete domain `F`, the sum of `p` is continuous on the disk of convergence, defined as the set of `y` in `E` with the extended metric distance from `y` to zero less than the radius of `p`.
|
analyticAt_const
theorem analyticAt_const :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {v : F},
AnalyticAt 𝕜 (fun x => v) x
The theorem `analyticAt_const` states that for any types `𝕜`, `E`, and `F` where `𝕜` is a nontrivially normed field, `E` is a normed additive commutative group that is a normed space over `𝕜`, and `F` is a normed additive commutative group that is a normed space over `𝕜`; for any elements `x` of type `E` and `v` of type `F`, the function which maps `x` to a constant `v` is analytic at `x`. In other words, this function has a convergent power series expansion around `x`.
More concisely: For any normed field `𝕜`, normed additive commutative groups `E` and `F` over `𝕜`, and elements `x in E` and `v in F`, the function `x ↦ v` is analytic at `x` in the sense of having a convergent power series expansion.
|
HasFPowerSeriesOnBall.uniform_geometric_approx'
theorem HasFPowerSeriesOnBall.uniform_geometric_approx' :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
HasFPowerSeriesOnBall f p x r →
↑r' < r →
∃ a ∈ Set.Ioo 0 1,
∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
This theorem states that, given a function `f` from a normed commutative additive group `E` to a normed commutative additive group `F` over a non-trivially normed field `𝕜`, and a formal multilinear series `p` on a ball centered at `x` with extended nonnegative real radius `r`, if `f` has a power series expansion given by `p`, then the approximation of `f` by the partial sums of this power series becomes exponentially better as we move towards the center of the ball and consider more terms in the series. Specifically, if `r'` is any nonnegative real number less than `r`, then there exist real numbers `a` strictly between 0 and 1 and `C` greater than zero such that for all points `y` with a distance less than `r'` from the origin and for all natural numbers `n`, the norm of the difference between `f` at `x + y` and the `n`-th partial sum of `p` at `y` is less than or equal to `C * (a * (‖y‖ / r')) ^ n`. This asserts that the approximation improves geometrically as we increase `n` and decrease `‖y‖` within the stricter subdisk of radius `r'`.
More concisely: Given a function `f` from a normed commutative additive group to another with power series expansion `p` over a non-trivially normed field, and for any ball centered at `x` with radius `r`, there exist `a` and `C` such that for all `y` with distance less than `r'` to `x` and all `n`, the norm of `f(x+y) - p.sum(n)(y)` is bounded by `C * (a * (||y|| / r') ^ n)`.
|
HasFPowerSeriesOnBall.hasFPowerSeriesAt
theorem HasFPowerSeriesOnBall.hasFPowerSeriesAt :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r → HasFPowerSeriesAt f p x
This theorem states that for any nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, normed spaces over `𝕜` for `E` and `F`, a function `f` from `E` to `F`, a formal multilinear series `p`, and a point `x` in `E`, if `f` has a formal power series on a ball centered at `x` with radius `r` (which is an extended nonnegative real number, i.e., a real number in [0, ∞]), then `f` also has a formal power series at the point `x`.
In other words, having a formal power series on a ball implies having a formal power series at the center of that ball. The formal multilinear series `p` serves as the representation of the formal power series in this context.
More concisely: If a function `f` from a normed additive group `E` to another normed additive group `F` over a nontrivially normed field `𝕜`, has a formal power series on a ball centered at a point `x` in `E`, then `f` has a formal power series at point `x`.
|
AnalyticAt.exists_ball_analyticOn
theorem AnalyticAt.exists_ball_analyticOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace F]
{f : E → F} {x : E}, AnalyticAt 𝕜 f x → ∃ r, 0 < r ∧ AnalyticOn 𝕜 f (Metric.ball x r)
The theorem `AnalyticAt.exists_ball_analyticOn` states that if a function `f` from `E` to `F` is analytic at a point `x` in `E`, then there exists a positive radius `r` such that `f` is analytic on the open ball of radius `r` centered at `x`. Here, the field `𝕜` is a nontrivially normed field, `E` and `F` are normed vector spaces over `𝕜`, and `F` is complete. In mathematical terms, if a function has a power series expansion at a point, it also has a power series expansion at every point in some open neighborhood of that point.
More concisely: If a function `f : E → F` is analytic at a point `x ∈ E` in the normed vector spaces `E` and `F` over a nontrivially normed field `𝕜`, then there exists a positive radius `r` such that `f` is analytic on the open ball `B(x, r)` centered at `x`.
|
FormalMultilinearSeries.isLittleO_one_of_lt_radius
theorem FormalMultilinearSeries.isLittleO_one_of_lt_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
↑r < p.radius → (fun n => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun x => 1
The theorem `FormalMultilinearSeries.isLittleO_one_of_lt_radius` states that for any nonnegative real number `r` that is strictly smaller than the radius of a given formal multilinear series `p` (over a non-trivially normed field `𝕜`, with normed vector spaces `E` and `F`), the sequence defined by the norm of the `n`th term of `p` multiplied by `r` to the power of `n` (‖pₙ‖ rⁿ) converges to `0` at infinity. This is indicated by "little o" notation (=o[Filter.atTop] fun x => 1), which represents that the function `fun n => ‖p n‖ * ↑r ^ n` is infinitesimally smaller than `1` as `n` approaches infinity.
More concisely: For any formal multilinear series `p` over a non-trivially normed field with normed vector spaces, if `r` is a strictly positive real number less than the radius of `p`, then the sequence `‖pₙ‖ * r^n` converges to 0 as `n` approaches infinity, which is denoted as `‖pₙ‖ * r^n = o(1)`.
|
FormalMultilinearSeries.le_radius_of_bound_nnreal
theorem FormalMultilinearSeries.le_radius_of_bound_nnreal :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) (C : NNReal) {r : NNReal}, (∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C) → ↑r ≤ p.radius
The theorem `FormalMultilinearSeries.le_radius_of_bound_nnreal` states that given any nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, and normed spaces over `𝕜` for `E` and `F`, for any formal multilinear series `p` from `𝕜` to `E` to `F`, a non-negative real number `C`, and another non-negative real number `r`, if the norm of the nth term of the series `p` multiplied by `r` to the power `n` is bounded by `C` for all natural numbers `n`, then the radius of the series `p` must be at least `r`. In the language of analysis, if the sequence of norms of the terms of the formal multilinear series, scaled by a power `n` of a non-negative real number, is bounded, then the radius of convergence of the series is at least that non-negative real number.
More concisely: If the norms of the terms of a formal multilinear series, scaled by a power of a non-negative real number, are bounded, then the radius of convergence is at least that non-negative real number.
|
HasFPowerSeriesOnBall.comp_sub
theorem HasFPowerSeriesOnBall.comp_sub :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r → ∀ (y : E), HasFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) r
The theorem `HasFPowerSeriesOnBall.comp_sub` states that, given a nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, and a normed space over these fields/groups, if a function `f` from `E` to `F` has a power series `p` around a point `x` within a radius `r` (which is an extended nonnegative real number), then the function `z ↦ f (z - y)` also has the same power series, but around the point `x + y` with the same radius `r`, for any point `y` in `E`. This essentially shows the transferability of a power series to another point in the function space by changing the variable via subtraction.
More concisely: Given a nontrivially normed field `𝕜`, normed additive groups `E` and `F`, and a normed space over these fields/groups, if `f : E → F` has a power series `p` around `x ∈ E` with radius `r > 0`, then `z ↦ f (z - y)` has the same power series `p` around `x + y` with radius `r`, for any `y ∈ E`.
|
HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal},
HasFPowerSeriesOnBall f p x r →
r' < r →
(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[Filter.principal (EMetric.ball (x, x) r')] fun y =>
‖y - (x, x)‖ * ‖y.1 - y.2‖
The theorem states that if a function `f` has a formal power series `∑ n, pₙ` on a ball of radius `r`, then, for any two points `y` and `z` in a smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is asymptotically bounded by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This property is formulated using the Big O notation (`IsBigO`) and the principal filter (`Filter.principal`) on a product space `E × E`. Here, `x` is the center of the ball, `r'` is the radius of the smaller ball, and `C` is some constant. The underlying space is assumed to be a nontrivially normed field `𝕜` and normed additive commutative groups `E` and `F` with normed spaces over `𝕜`.
More concisely: Given a function `f` with a formal power series expansion on a ball of radius `r` in a normed field `𝕜` and normed additive commutative groups `E` and `F`, for any two points `y` and `z` in a smaller ball, the difference `f y - f z - p 1 (fun _ ↦ y - z)` is asymptotically bounded by `C * (max ‖y - x‖, ‖z - x‖) * ‖y - z‖`, where `x` is the center, `r'` is the radius of the smaller ball, `p` is the power series, and `C` is a constant. (Formulated using the Big O notation and the principal filter on `E × E`.)
|
FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius
theorem FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, ↑r < p.radius → ∃ C > 0, ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C
The theorem "FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius" states that for any given nonnegative real number `r` that is strictly smaller than the radius of a formal multilinear series `p`, over a nontrivially normed field `𝕜` and normed space `E` and `F`, there exists a positive constant `C` such that for all natural numbers `n`, the nonnegative norm of the `n`-th term of the series `p` multiplied by `r` to the power of `n` is less than or equal to `C`. Here `‖p n‖₊` represents the nonnegative norm of the `n`-th term of the series `p`. In mathematical terms, if `r` is strictly less than the radius of convergence of the series `p`, then the series `‖pₙ‖ rⁿ` is bounded.
More concisely: For any formal multilinear series `p` over a nontrivially normed field and space, if the non-negative real number `r` strictly less than the radius of convergence, then there exists a constant `C` such that for all natural numbers `n`, the norm of the `n`-th term `‖p n‖` multiplied by `r` raised to the power of `n` is bounded by `C`.
|
HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn'
theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r →
TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (EMetric.ball x r)
The theorem `HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn'` states that if a function `f` has a power series expansion at a point `x`, then the function `f` is the locally uniform limit of the partial sums of that power series within its radius of convergence `r`. In other words, for every point `y` in the open ball with radius `r` centered at `x` (denoted `EMetric.ball x r`), the partial sums of the power series (represented by `p.partialSum n (y - x)`) converge to the function value `f(y)` uniformly as `n` goes to infinity (represented by `Filter.atTop`).
More concisely: If a function `f` has a power series expansion with radius of convergence `r` at `x`, then `f` is the uniform limit of the partial sums of the power series on the open ball `EMetric.ball x r`.
|
AnalyticAt.sub
theorem AnalyticAt.sub :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (f - g) x
The theorem `AnalyticAt.sub` states that for any types `𝕜`, `E`, `F` where `𝕜` is a nontrivially normed field, `E` and `F` are normed additive commutative groups, and `E`, `F` are normed spaces over `𝕜`, if we have two functions `f` and `g` from `E` to `F` and if both `f` and `g` are analytic at a point `x` in `E`, then the function `f - g` is also analytic at `x`. In mathematical terms, this states that the difference of two analytic functions is also analytic.
More concisely: If `𝕜` is a nontrivially normed field and `f`, `g` are analytic functions from the normed additive commutative groups and normed spaces `E` and `F` over `𝕜`, then the difference `f - g` is also analytic at any point `x` in `E`.
|
HasFPowerSeriesOnBall.exchange_radius
theorem HasFPowerSeriesOnBall.exchange_radius :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {r₁ r₂ : ENNReal} {x : 𝕜},
HasFPowerSeriesOnBall f p₁ x r₁ → HasFPowerSeriesOnBall f p₂ x r₂ → HasFPowerSeriesOnBall f p₁ x r₂
The theorem `HasFPowerSeriesOnBall.exchange_radius` states that for any nontrivially normed field `𝕜` and normed add commutative group `E` with `E` being a normed space over `𝕜`, given two formal multilinear series `p₁` and `p₂` and a function `f : 𝕜 → E`, if `f` has power series representations at a point `x` with radii of convergence `r₁` and `r₂` respectively, then we can guarantee that `f` also has a power series representation with the first series `p₁` and the larger radius `r₂`. This theorem can be useful when the formal multilinear series in one representation is simpler, but the other series has a larger radius of convergence.
More concisely: Given a nontrivially normed field `𝕜`, a normed add commutative group `E` over `𝕜`, and a function `f : 𝕜 → E` with power series representations `p₁` and `p₂` at some point `x` with radii of convergence `r₁` and `r₂` respectively, if `r₁ ≤ r₂`, then `f` also has a power series representation with `p₁` and radius `r₂`.
|
HasFPowerSeriesOnBall.r_eq_top_of_exists
theorem HasFPowerSeriesOnBall.r_eq_top_of_exists :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {r : ENNReal} {x : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E},
HasFPowerSeriesOnBall f p x r →
(∀ (r' : NNReal), 0 < r' → ∃ p', HasFPowerSeriesOnBall f p' x ↑r') → HasFPowerSeriesOnBall f p x ⊤
The theorem states that if a function `f` from 𝕜 to E has a power series representation `p` on a ball of some radius, and for each positive radius there exists a power series representation, then `p` converges to `f` on the whole of 𝕜. Here, 𝕜 is a nontrivially normed field, E is a normed additive commutative group and also a normed space over 𝕜. The radius of the ball in the power series representation can be an extended nonnegative real number (including infinity), denoted as `ENNReal` in Lean 4, and for every nonnegative real number radius `r'`, if there exists a power series representation, then the power series `p` converges to function `f` everywhere in 𝕜.
More concisely: If a function `f` from a nontrivially normed field `𝕜` to a normed additive commutative group and normed space `E` over `𝕜` has a convergent power series representation `p` on the whole of `𝕜` for every positive radius, then `p` is the power series representation of `f`.
|
HasFPowerSeriesOnBall.tendstoUniformlyOn'
theorem HasFPowerSeriesOnBall.tendstoUniformlyOn' :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
HasFPowerSeriesOnBall f p x r →
↑r' < r → TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (Metric.ball x ↑r')
This theorem states that if a function has a power series expansion at a point `x`, then it uniformly converges to the partial sums of this power series within any slightly smaller disk contained in the disk of convergence. In more precise terms, given a function `f` with a power series expansion `p` at `x` within a disk of radius `r` (with `r` being an extended nonnegative real number), for any smaller radius `r'` (a nonnegative real number) with `r'` less than `r`, the function `f` is the uniform limit of the partial sums `p.partialSum n (y - x)` at every point `y` within the smaller disk of radius `r'` centered at `x`, as `n` goes to infinity. This is a fundamental result about the convergence of power series.
More concisely: Given a function `f` with power series expansion `p` at `x` with radius of convergence `r`, for any `r' < r`, `f` is the uniform limit of `p.partialSum n (y - x)` as `n` goes to infinity, for all `y` in the disk of radius `r'` centered at `x`.
|
HasFPowerSeriesAt.eq_formalMultilinearSeries
theorem HasFPowerSeriesAt.eq_formalMultilinearSeries :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜},
HasFPowerSeriesAt f p₁ x → HasFPowerSeriesAt f p₂ x → p₁ = p₂
This Lean theorem, `HasFPowerSeriesAt.eq_formalMultilinearSeries`, states that if two one-dimensional formal multilinear series, denoted as `p₁` and `p₂`, represent the same function `f` at a point `x` in a normed space over a non-trivially normed field `𝕜`, then `p₁` and `p₂` must be equal. In the context of mathematics, this theorem asserts the uniqueness of the formal multilinear series representation of a function at a given point.
More concisely: If two one-dimensional formal multilinear series represent the same function at a point in a normed space over a non-trivially normed field, then they are equal.
|
HasFPowerSeriesOnBall.tendstoUniformlyOn
theorem HasFPowerSeriesOnBall.tendstoUniformlyOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
HasFPowerSeriesOnBall f p x r →
↑r' < r →
TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (Metric.ball 0 ↑r')
This theorem states that if a function `f` has a power series expansion at a point `x`, then `f` is the uniform limit of the partial sums of this power series on any strict subdisk within the disk of convergence. In other words, if the power series of `f` converges to `f` in a disk of radius `r`, then in any smaller disk of radius `r'` (where `r'` is a nonnegative real number less than `r`), the function `f(x + y)` is the limit of the sequence of partial sums of the power series when we let the number of terms go to infinity. This convergence is uniform, meaning that the speed of convergence does not depend on `y` in the smaller disk.
More concisely: If a function `f` has a power series expansion that converges uniformly to `f` in a disk of radius `r`, then the partial sums of the power series uniformly converge to `f` in any strict subdisk of radius `r' < r.
|
FormalMultilinearSeries.le_radius_of_isBigO
theorem FormalMultilinearSeries.le_radius_of_isBigO :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
((fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => 1) → ↑r ≤ p.radius
The theorem `FormalMultilinearSeries.le_radius_of_isBigO` states that for any formal multilinear series `p` over a normed field `𝕜`, if the norm of `pₙ` times `rⁿ` is of "big-O" notation equal to 1 as `n` tends to infinity (`‖pₙ‖ rⁿ = O(1)`, as `n → ∞`), then the radius of `p` is at least `r`. Here, `r` is a nonnegative real number (`NNReal`), and the "big-O" notation (`=O[Filter.atTop]`) refers to a bound that holds when `n` becomes sufficiently large (i.e., `n` goes to infinity).
More concisely: If the norm of a formal multilinear series' `n`-th term times `r^n` is big-O(1) as `n` approaches infinity, then the radius of the series is at least `r`.
|
HasFPowerSeriesAt.analyticAt
theorem HasFPowerSeriesAt.analyticAt :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f p x → AnalyticAt 𝕜 f x
The theorem `HasFPowerSeriesAt.analyticAt` states that for any function `f` from `E` to `F` and any point `x` in `E`, if `f` has a convergent power series expansion represented by a formal multilinear series `p` at the point `x`, then `f` is analytic at the point `x`. Here, `𝕜` is a non-trivial normed field, `E` is a normed additive commutative group that is also a normed space over `𝕜`, and `F` is another normed additive commutative group that is also a normed space over `𝕜`.
More concisely: If a function `f` from a normed additive commutative group `E` to another normed additive commutative group `F` over a non-trivial normed field `𝕜` has a convergent power series expansion at a point `x` in `E`, then `f` is analytic at `x`.
|
HasFPowerSeriesAt.eq_zero_of_eventually
theorem HasFPowerSeriesAt.eq_zero_of_eventually :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜},
HasFPowerSeriesAt f p x → (nhds x).EventuallyEq f 0 → p = 0
This theorem states that if you have a one-dimensional formal multilinear series `p` that represents a function `f` around a point `x` in a normed space over a normed and nontrivially normed field, and if the function `f` eventually equals zero in the neighborhood of `x`, then the series `p` must be zero. In other words, a non-zero formal multilinear series cannot represent a function that is eventually zero.
More concisely: A non-zero one-dimensional formal multilinear series does not represent a function that eventually equals zero in a normed space over a normed and nontrivially normed field.
|
HasFPowerSeriesOnBall.uniform_geometric_approx
theorem HasFPowerSeriesOnBall.uniform_geometric_approx :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
HasFPowerSeriesOnBall f p x r →
↑r' < r →
∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
This theorem states that given a function `f` from a normed space `E` to another normed space `F` over a nontrivially normed field `𝕜` that admits a power series expansion `p` centered at a point `x` within a ball of extended nonnegative radius `r`, and given a nonnegative real number `r'` that is less than `r`, there exists a number `a` in the open interval (0, 1) and a positive constant `C` such that for every point `y` in the open ball centered at 0 with radius `r'` and for every natural number `n`, the norm of the difference between `f(x + y)` and the `n`th partial sum of the power series at `y` is less than or equal to `C` times `a` raised to the `n`th power. This essentially means that the function is exponentially close to its power series expansion on strict subballs of the ball of convergence.
More concisely: Given a normed space function `f` with power series expansion `p` at `x` in a ball of radius `r`, and `r' < r`, there exists `a in (0, 1)` and a constant `C` such that for all `y` in the open ball of radius `r'` around 0, the norm of `f(x + y) - p(y)` is bounded by `C * a^n` for all natural numbers `n`.
|
ContinuousLinearMap.comp_analyticOn
theorem ContinuousLinearMap.comp_analyticOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[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} {s : Set E}
(g : F →L[𝕜] G), AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (⇑g ∘ f) s
The theorem `ContinuousLinearMap.comp_analyticOn` states that for any types 𝕜, E, F, and G, where 𝕜 is a non-trivially normed field, E, F, G are normed additive commutative groups and normed spaces over 𝕜. Given a function `f` from E to F which is analytic on a set `s` of type E, and a continuous linear map `g` from F to G, the composition of `g` and `f`, denoted `(⇑g ∘ f)`, is also analytic on the set `s`. In other words, if a function `f` is analytic on a set `s`, and `g` is a continuous linear map, then the composition of `g` and `f` remains analytic on the same set `s`.
More concisely: Given a normed field 𝕜, a set $s$ in a normed additive commutative group and normed space $E$ over 𝕜, a function $f:s\to E'$ analytic on $s$ with $E',F,G$ being normed additive commutative groups and normed spaces over 𝕜, and a continuous linear map $g:F\to G$, the composition $g\circ f:s\to G$ is analytic on $s$.
|
HasFPowerSeriesAt.eq_zero
theorem HasFPowerSeriesAt.eq_zero :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {x : 𝕜}, HasFPowerSeriesAt 0 p x → p = 0
This theorem states that in a non-trivially normed field `𝕜` and a normed additive commutative group `E` which is also a normed space over `𝕜`, if a one-dimensional formal multilinear series `p` represents the zero function at a point `x` in `𝕜`, then `p` must be the zero series. In other words, any formal multilinear series that represents the zero function is itself zero.
More concisely: In a non-trivially normed field and a normed additive commutative group that is also a normed space, if a one-dimensional formal multilinear series represents the zero function at a point, then it is the zero series.
|
HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn
theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
HasFPowerSeriesOnBall f p x r →
TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (EMetric.ball 0 r)
This theorem states that if a function `f` has a power series expansion at a point `x`, then the function is the locally uniform limit of the partial sums of this power series within its disk of convergence. More specifically, for each point `y` in the disk of radius `r` around `0` in the domain, the partial sums of the power series converges to the value of the function at `x + y` as the index of the partial sums tends to infinity. The convergence is uniform in each compact subset of the disk.
More concisely: If a function `f` has a power series expansion `P` around point `x` with radius of convergence `r`, then for each `y` in the disk of radius `r` around `x`, the sequence of partial sums of `P` converges uniformly to `f(x + y)` as the index goes to infinity.
|
AnalyticOn.continuousOn
theorem AnalyticOn.continuousOn :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
AnalyticOn 𝕜 f s → ContinuousOn f s
This theorem states that if a function `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, both of which have a normed space structure over a nontrivially normed field `𝕜`, is analytic on a set `s` of `E`, then `f` is also continuous on `s`. In other words, any function that is analytic on a set (which means it is analytic around every point of the set) is also continuous on that set (which means it is continuous at every point of the set).
More concisely: If a function between two normed additive commutative groups is analytic on a set, then it is continuous on that set.
|
AnalyticAt.continuousAt
theorem AnalyticAt.continuousAt :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
AnalyticAt 𝕜 f x → ContinuousAt f x
The theorem `AnalyticAt.continuousAt` states that, for any non-trivial normed field `𝕜`, any normed additive groups `E` and `F` over `𝕜` which are also normed spaces, any function `f` from `E` to `F`, and any point `x` in `E`, if the function `f` is analytic at the point `x` (meaning `f` admits a convergent power series expansion around `x`), then `f` is also continuous at the point `x`. In other words, the value of `f` at `x` tends to the limit of `f` at `x` as points in `E` approach `x`.
More concisely: If a function between two normed spaces is analytic at a point, then it is continuous at that point.
|