FormalMultilinearSeries.changeOriginSeriesTerm_bound
theorem FormalMultilinearSeries.changeOriginSeriesTerm_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) {n : โ},
(โ (m : โ), n โค m โ p m = 0) โ
โ (k l : โ) {s : Finset (Fin (k + l))} (hs : s.card = l), n โค k + l โ p.changeOriginSeriesTerm k l s hs = 0
This theorem states that if `p` is a formal multilinear series such that its `m`th term is zero for all `m` that are greater than or equal to `n`, then the term of the series obtained by changing the origin of `p` at combined indices `k` and `l` (with `s` a finite set of size `l` from the set of all `k+l` indices) will also be zero for all `k` and `l` where the sum `k + l` is greater than or equal to `n`. This is valid in the context of a nontrivially normed field `๐` and normed add commutative groups `E` and `F` where `E` and `F` are normed spaces over `๐`.
More concisely: If `p` is a multilinear series over a nontrivially normed field `๐` with `m`th term zero for all `m โฅ n`, then the term of the series obtained by shifting indices `k` and `l` (sum `โฅ n`) is zero.
|
HasFiniteFPowerSeriesOnBall.eq_partialSum
theorem HasFiniteFPowerSeriesOnBall.eq_partialSum :
โ {๐ : 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} {n : โ},
HasFiniteFPowerSeriesOnBall f p x n r โ โ y โ EMetric.ball 0 r, โ (m : โ), n โค m โ f (x + y) = p.partialSum m y
This theorem states that if a function `f` has a finite power series expansion bounded by `n`, then for any point `y` in the open disk of radius `r` centered at the origin and for any natural number `m` satisfying `n โค m`, the value of the function `f` at `x + y` is equal to the `m`-th partial sum of the power series at `y`. Here, `๐` is a nontrivial normed field, `E` and `F` are normed additive commutative groups over `๐`, and `p` is a formal multilinear series linking `E` and `F`.
More concisely: If `f` is a function with a finite `n`th power series expansion bounded by `๐` in `x` around `0`, then for any `y` in the open disk of radius `r` in `๐-E` centered at `0`, and any `m (โฅ 0)` with `n โค m`, `f(x + y) = โโโโฑ=โโฑ=โ p(xโฑ, yโฑ) + Rโ(x, y)`, where `Rโ` is the remainder term of the power series.
|
ContinuousLinearMap.comp_cPolynomialOn
theorem ContinuousLinearMap.comp_cPolynomialOn :
โ {๐ : 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), CPolynomialOn ๐ f s โ CPolynomialOn ๐ (โg โ f) s
The theorem `ContinuousLinearMap.comp_cPolynomialOn` states that, given a non-trivially normed field `๐` and normed add-commutative groups E, F, and G with associated normed vector spaces, if a function `f` from E to F is continuously polynomial on a set `s` in E, and `g` is a continuous linear map from F to G, then the composition of `g` and `f` (i.e., `g โ f`) is also continuously polynomial on the set `s`. This implies that the property of being continuously polynomial is preserved under the composition with a continuous linear map.
More concisely: Given a non-trivially normed field ๐ and normed vector spaces E, F, and G with continuous linear map g : F โ G, if f : E โ F is continuously polynomial on a set s โ E, then the composition g โ f is also continuously polynomial on s.
|
HasFiniteFPowerSeriesOnBall.eq_partialSum'
theorem HasFiniteFPowerSeriesOnBall.eq_partialSum' :
โ {๐ : 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} {n : โ},
HasFiniteFPowerSeriesOnBall f p x n r โ โ y โ EMetric.ball x r, โ (m : โ), n โค m โ f y = p.partialSum m (y - x)
This theorem states that for any types ๐, E, and F where ๐ is a nontrivially normed field, E is a normed addition commutative group and a normed space over ๐, and F is also a normed addition commutative group and a normed space over ๐, given a function `f` from E to F, a formal multilinear series `p` from ๐, E, and F, an element `x` of E, a nonnegative extended real number `r`, and a natural number `n`, if `f` has a finite power series on the ball centered at `x` with radius `r` truncated at `n`, then for any `y` in the ball centered at `x` with radius `r` and for any natural number `m` greater than or equal to `n`, `f` at `y` is equal to the `m`th partial sum of `p` at `y - x`.
In short, if a function has a finite power series representation within a given ball in a normed space, then the function's value at any point within the ball can be approximated by the partial sums of the power series.
More concisely: Given a nontrivially normed field ๐, normed commutative groups and spaces E and F over ๐, a function `f` from E to F with a finite power series representation around `x` in E with radius `r`, and a natural number `m` greater than or equal to the truncation point `n`, for all `y` in the ball centered at `x` with radius `r`, `f(y) = โโโ (p(x, ..., x, x - y, ..., x) / k!), where the sum runs over all multi-indices k of length m.`
|
FormalMultilinearSeries.hasSum_of_finite
theorem FormalMultilinearSeries.hasSum_of_finite :
โ {๐ : 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 : โ), n โค m โ p m = 0) โ โ (x : E), HasSum (fun n => (p n) fun x_1 => x) (p.sum x)
This theorem states that for a finite formal multilinear series 'p' over a nontrivially normed field '๐', normed add commutative group 'E', and normed space 'F', if the series 'p' is zero for all terms greater than or equal to a certain natural number 'n', then the sum of the series at any point 'x' in 'E' is equal to the sum of the series 'p' at 'x'. In other words, this theorem assures us that we can compute the sum of a finite formal multilinear series by summing the series term by term without worrying about the terms beyond 'n'.
More concisely: If 'p' is a finite formal multilinear series over a nontrivially normed field with normed additive group 'E' and normed space 'F' such that all terms of 'p' greater than or equal to a certain natural number 'n' are zero, then the sum of 'p' at any point 'x' in 'E' equals the sum of the first 'n' terms of 'p' at 'x'.
|
isOpen_cPolynomialAt
theorem isOpen_cPolynomialAt :
โ (๐ : 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),
IsOpen {x | CPolynomialAt ๐ f x}
The theorem `isOpen_cPolynomialAt` states that for any function `f` mapping from one normed vector space to another over a non-trivially normed field `๐`, the set of points `x` at which `f` admits a finite power series expansion (or in other words, `f` is continuously polynomial at `x`) forms an open set in the topological space of the domain. This essentially means that around every point where the function is continuously polynomial, there exists an open neighbourhood entirely comprised of points where the function is also continuously polynomial.
More concisely: The set of points in a normed vector space where a function admits a finite power series expansion forms an open subset.
|
CPolynomialAt.analyticAt
theorem CPolynomialAt.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} {x : E},
CPolynomialAt ๐ f x โ AnalyticAt ๐ f x
The theorem `CPolynomialAt.analyticAt` states that for any non-trivially normed field `๐`, normed add-commutative groups `E` and `F`, a normed space `E` over `๐`, a normed space `F` over `๐`, and a function `f` from `E` to `F`, if `f` is continuously polynomial at a point `x` in `E` (i.e., it admits a finite power series expansion around `x`), then `f` is also analytic at `x` (i.e., it admits a convergent power series expansion around `x`).
More concisely: If a function `f` from a normed space `E` to another normed space `F` over a non-trivially normed field `๐` has a finite power series expansion around a point `x` in `E`, then `f` is analytic at `x`, meaning it has a convergent power series expansion around `x`.
|
FormalMultilinearSeries.cPolynomialAt_changeOrigin_of_finite
theorem FormalMultilinearSeries.cPolynomialAt_changeOrigin_of_finite :
โ {๐ : 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 : โ), n โค m โ p m = 0) โ โ (k : โ), CPolynomialAt ๐ (fun x => p.changeOrigin x k) 0
For any field ๐ endowed with a norm, types E and F which are both normed additive commutative groups and normed spaces over ๐, and a formal multilinear series p, the theorem asserts that if every term of the series p from a certain index n onward is zero, then for every positive integer k, the terms of the series p.changeOrigin are continuously polynomial at the origin. In other words, each term in the series "p.changeOrigin" admits a finite power series expansion around the origin.
More concisely: If a multilinear series p over a field with a norm has all terms from a certain index onward equal to zero, then each term in the series p.changeOrigin admits a finite power series expansion around the origin.
|
HasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt_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] {f : E โ F}
{p : FormalMultilinearSeries ๐ E F} {r : ENNReal} {n : โ} {x y : E},
HasFiniteFPowerSeriesOnBall f p x n r โ y โ EMetric.ball x r โ CPolynomialAt ๐ f y
This theorem states that if a function `f` from type `E` to `F` admits a finite power series expansion `p` on an open ball centered at `x` with radius `r` in a non-trivially normed field `๐`, then the function `f` is continuously polynomial at every point `y` within this ball. In other words, if a function can be represented by a finite power series within a certain region in the domain, it behaves as a polynomial function at each point in this region.
More concisely: If a function `f` from type `E` to `F` admits a finite power series expansion on an open ball centered at `x` in a non-trivially normed field `๐`, then `f` is continuously polynomial on this ball.
|
CPolynomialOn.continuous
theorem CPolynomialOn.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},
CPolynomialOn ๐ f Set.univ โ Continuous f
This theorem states that, for any function `f` mapping from a normed additive commutative group `E` to another normed additive commutative group `F`, over a non-trivially normed field `๐`, if the function `f` is continuously polynomial on the universal set (i.e., it is continuously polynomial at every point in the domain), then `f` is continuous. Here, "continuously polynomial" means that the function behaves like a polynomial near every point in its domain, and it does so in a way that is continuous with respect to changes in the input.
More concisely: If `f` is a function from a normed additive commutative group `E` to another normed additive commutative group `F` over a non-trivially normed field, and `f` is continuously polynomial on `E`, then `f` is continuous.
|
HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero
theorem HasFiniteFPowerSeriesAt.eventually_zero_of_bound_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] {f : E โ F}
{pf : FormalMultilinearSeries ๐ E F} {x : E}, HasFiniteFPowerSeriesAt f pf x 0 โ (nhds x).EventuallyEq f 0
The theorem states that if a function `f` has a formal power series expansion at a point `x` that is bounded by `0`, then the function `f` equals `0` in a neighborhood of `x`. Here, a neighborhood of `x` is a set that contains an open set around `x`. The function `f` is from a normed vector space `E` over a non-trivial normed field `๐` to another normed vector space `F` over the same field `๐`. The formal power series of `f` at `x` is represented by `pf`, and `HasFiniteFPowerSeriesAt f pf x 0` asserts that the power series has a finite radius of convergence and is bounded by `0`. Moreover, `(nhds x).EventuallyEq f 0` indicates that `f` is eventually equal to `0` at points closer and closer to `x`.
More concisely: If a function `f` from a normed vector space to another normed vector space, with a formal power series expansion at `x` that is bounded and has finite radius of convergence, then `f(x) = 0` and `f` equals `0` in a neighborhood of `x`.
|
HasFiniteFPowerSeriesAt.toHasFPowerSeriesAt
theorem HasFiniteFPowerSeriesAt.toHasFPowerSeriesAt :
โ {๐ : 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} {n : โ}, HasFiniteFPowerSeriesAt f p x n โ HasFPowerSeriesAt f p x
This theorem states that for any nontrivial normed field `๐`, normed additive commutative group `E` and `F`, normed space `E` over `๐`, normed space `F` over `๐`, any function `f` from `E` to `F`, any formal multilinear series `p`, any element `x` of `E`, and any natural number `n`, if the function `f` has a finite formal power series at `x` of order `n`, then `f` also has a formal power series at `x`. Essentially, this theorem connects the concept of a finite formal power series to a formal power series for a function in the context of normed spaces and fields.
More concisely: If a function from a normed space to another normed space over a nontrivial normed field has a finite formal power series at some point, then it has a formal power series at that point.
|
HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one
theorem HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one :
โ {๐ : 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}
{pf : FormalMultilinearSeries ๐ E F} {x : E} {r : ENNReal},
HasFiniteFPowerSeriesOnBall f pf x 1 r โ โ y โ EMetric.ball x r, f y = f x
This theorem states that if a function `f` from a normed space `E` to another normed space `F` over a nontrivially normed field `๐` has a finite formal power series within a ball of radius `1`, then `f` is constant and equal to the value `f x` within that ball. In other words, if any point `y` is within the `EMetric.ball` with center `x` and nonnegative extended real radius `r`, then the value of the function `f` at `y` is the same as the value of the function `f` at `x`.
More concisely: If a continuous function `f` from a normed space `E` to another normed space `F` over a nontrivially normed field `๐` has a convergent power series representation within the ball of radius `1` centered at `x` in `E`, then `f` is constant and equal to `f x` within that ball.
|
HasFiniteFPowerSeriesAt.cPolynomialAt
theorem HasFiniteFPowerSeriesAt.cPolynomialAt :
โ {๐ : 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} {n : โ}, HasFiniteFPowerSeriesAt f p x n โ CPolynomialAt ๐ f x
The theorem `HasFiniteFPowerSeriesAt.cPolynomialAt` states that for any field `๐` equipped with a norm, any normed additive commutative group `E` over `๐`, another normed additive commutative group `F` over `๐`, any function `f` from `E` to `F`, any formal multilinear series `p`, any element `x` from `E`, and any natural number `n`, if the function `f` has a finite power series expansion represented by `p` of order `n` at `x` (`HasFiniteFPowerSeriesAt f p x n`), then `f` is continuously polynomial at `x` (`CPolynomialAt ๐ f x`). In simpler terms, if a function has a finite power series expansion at a point, then it is continuously polynomial at that point.
More concisely: If a function has a finite power series expansion at a point in a normed additive commutative group over a field with a norm, then the function is continuously polynomial at that point.
|
FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite
theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite :
โ {๐ : 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 : โ), n โค m โ p m = 0) โ HasFiniteFPowerSeriesOnBall p.sum p 0 n โค
This theorem states that for any finite power series `p`, if `p m` is equal to zero for all `m` greater than or equal to a certain natural number `n`, then the sum of the series `p` can be represented as a formal power series on an open ball centered at `0` with radius `โ` and `n` terms. Here, `๐` is the field of scalars, `E` and `F` are normed spaces over `๐`, which are also normed additive commutative groups.
More concisely: If a finite power series `p` over a field `๐` has zero coefficient for all terms of degree greater than or equal to some natural number `n`, then `p` can be represented as a formal power series with `n` terms on the open ball centered at `0` with radius `โ` in the normed spaces `E` and `F` over `๐`.
|
ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall
theorem ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall :
โ {๐ : 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} {n : โ} (g : F โL[๐] G),
HasFiniteFPowerSeriesOnBall f p x n r โ
HasFiniteFPowerSeriesOnBall (โg โ f) (g.compFormalMultilinearSeries p) x n r
The theorem `ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall` states that if a function `f` has a finite power series `p` defined on a certain ball in a normed vector space, and `g` is a continuous linear map, then the composition `g โ f` also has a finite power series `g โ p` defined on the same ball. This is valid in the context where `๐` is a non-trivial normed field, `E`, `F` and `G` are normed additive commutative groups over `๐` forming normed spaces, `f` is a function from `E` to `F`, `p` is a formal multilinear series from `E` to `F`, `x` is an element of `E`, `r` is a non-negative extended real number, `n` is a natural number, and `g` is a continuous linear map from `F` to `G`.
More concisely: If `f` is a function from a normed space `E` to another normed space `F` with a finite power series `p` on the ball of radius `r` centered at `x` in `E`, and `g` is a continuous linear map from `F` to a normed space `G`, then `g โ f` has a finite power series `g โ p` on the same ball.
|
FormalMultilinearSeries.continuousOn_of_finite
theorem FormalMultilinearSeries.continuousOn_of_finite :
โ {๐ : 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 : โ), n โค m โ p m = 0) โ Continuous p.sum
This theorem states that the sum of a finite power series is continuous. More specifically, given a type `๐` which is a nontrivially normed field, types `E` and `F` that are normed additive commutative groups, and where `๐`, `E`, and `F` form normed spaces, it states that for any formal multilinear series `p` from `๐` to `E` and `F`, if for a certain natural number `n`, `p` equals zero for all numbers `m` greater than or equal to `n`, then the sum of `p` is a continuous function.
More concisely: Given a normed field `๐`, normed additive commutative groups `E` and `F`, and a formal multilinear series `p` from `๐` to `E` and `F` such that `p` is zero for all `m` greater than a certain natural number `n`, the sum of `p` is a continuous function.
|
FormalMultilinearSeries.changeOriginSeries_finite_of_finite
theorem FormalMultilinearSeries.changeOriginSeries_finite_of_finite :
โ {๐ : 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 : โ), n โค m โ p m = 0) โ โ (k : โ) {m : โ}, n โค k + m โ p.changeOriginSeries k m = 0
This theorem states that if `p` is a finite formal multilinear series, then the series `p.changeOriginSeries k` is also finite for every natural number `k`. Specifically, if the series `p` vanishes for indices `m` greater than or equal to `n` (i.e., `p m = 0` for `n โค m`), then the series `p.changeOriginSeries k` also vanishes for indices `m` such that `n โค k + m`. Here, `๐` is a nontrivially normed field, `E` and `F` are normed additive commutative groups over `๐`, and `p` is a formal multilinear series from `E` to `F`.
More concisely: If `p` is a finite multilinear series from a normed additive commutative group `E` to another `F` over a nontrivially normed field `๐`, with `p` vanishing for indices greater than or equal to `n`, then `p.changeOriginSeries k` also vanishes for indices `m` satisfying `n โค k + m`.
|
HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero
theorem HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_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] {f : E โ F}
{pf : FormalMultilinearSeries ๐ E F} {x : E} {r : ENNReal},
HasFiniteFPowerSeriesOnBall f pf x 0 r โ โ y โ EMetric.ball x r, f y = 0
This theorem states that if a function `f` has a finite formal power series bounded by `0` on a ball in an extended metric space, then the function `f` is identically zero on that ball. Here, `๐` represents a nontrivially normed field, `E` and `F` are normed additively commutative groups that are normed spaces over `๐`, and `f` is a function from `E` to `F`. The ball in the extended metric space is centered at `x` with radius `r`, and `pf` is the formal multilinear series for `f`. If `y` is any point in the ball, `f` evaluated at `y` equals zero.
More concisely: If a function `f` from a normed space `E` to another normed space `F` over a nontrivially normed field `๐` has a formal power series bounded by 0 on the ball `B(x,r)` in the extended metric space, then `f(y) = 0` for all `y โ B(x,r)`.
|
HasFiniteFPowerSeriesOnBall.comp_sub
theorem HasFiniteFPowerSeriesOnBall.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} {n : โ},
HasFiniteFPowerSeriesOnBall f p x n r โ
โ (y : E), HasFiniteFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) n r
The theorem `HasFiniteFPowerSeriesOnBall.comp_sub` states that given a function `f` that has a finite power series `p` around a point `x` in a normed space, then the function obtained by shifting the input of `f` by a vector `y` also has the same finite power series, but now around the point `x + y`. This result is valid over any non-trivially normed field and is true for all vectors `y`.
More concisely: If `f` has a finite power series expansion `p` around `x` in a normed space, then `f` shifted by `y` has the same finite power series expansion around `x + y`.
|
CPolynomialAt.exists_ball_cPolynomialOn
theorem CPolynomialAt.exists_ball_cPolynomialOn :
โ {๐ : 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},
CPolynomialAt ๐ f x โ โ r, 0 < r โง CPolynomialOn ๐ f (Metric.ball x r)
The theorem states that if a function `f` is continuously polynomial at a certain point, then there exists a nonempty ball around that point where the function is continuously polynomial on the entire set of points within the ball. In other words, if the function `f` has a finite power series expansion around a certain point, then there is a non-empty neighborhood of that point where the function has a finite power series expansion at every point.
More concisely: If a function `f` is continuously polynomial around a point, then there exists a neighborhood of that point where `f` is represented by its finite power series expansion.
|
HasFiniteFPowerSeriesOnBall.continuousOn
theorem HasFiniteFPowerSeriesOnBall.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} {n : โ},
HasFiniteFPowerSeriesOnBall f p x n r โ ContinuousOn f (EMetric.ball x r)
This theorem states that if a function `f` from a normed space `E` over a non-trivially normed field `๐` to another normed space `F` over the same field has a finite power series expansion `p` of degree `n` on a ball of radius `r` centered at `x` in `E`, then the function `f` is continuous on this ball. Here, the "ball" is defined in the sense of an extended metric space (`EMetric.ball`), meaning it includes all points whose extended distance (which can be infinite) to `x` is less than `r`.
More concisely: If a function `f` from a normed space `E` to another normed space `F` over the same field has a finite power series expansion of degree `n` on the ball of radius `r` centered at `x` in `E`, then `f` is continuous on this ball.
|
HasFiniteFPowerSeriesAt.eventually_const_of_bound_one
theorem HasFiniteFPowerSeriesAt.eventually_const_of_bound_one :
โ {๐ : 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}
{pf : FormalMultilinearSeries ๐ E F} {x : E},
HasFiniteFPowerSeriesAt f pf x 1 โ (nhds x).EventuallyEq f fun x_1 => f x
The theorem states that if a function `f` has a formal power series at a point `x` that is bounded by `1`, then `f` is constant and equal to `f(x)` within a neighborhood of `x`. Here, `๐` is a nontrivially normed field, `E` is a normed add commutative group over `๐`, `F` is also a normed add commutative group over `๐`, and `f` is a function from `E` to `F`. The formal power series of `f` at `x` is denoted by `pf`. The concept of a neighborhood used in the theorem is related to the topology of the space, where a set is considered a neighborhood of `x` if it contains an open set around `x`.
More concisely: If `f` is a function from a normed add commutative group `E` to another normed add commutative group `F` over a nontrivially normed field `๐`, and `pf` is the formal power series of `f` at `x` with `|pf(z)| โค 1` for all `z` in some neighborhood of `x`, then `f` is constant and equal to `f(x)` in that neighborhood.
|
FormalMultilinearSeries.changeOrigin_finite_of_finite
theorem FormalMultilinearSeries.changeOrigin_finite_of_finite :
โ {๐ : 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}
(p : FormalMultilinearSeries ๐ E F) {n : โ},
(โ (m : โ), n โค m โ p m = 0) โ โ {k : โ}, n โค k โ p.changeOrigin x k = 0
This theorem states that if `p` is a formal multilinear series and all terms `p m` are zero for `m` greater than or equal to `n`, then the terms of the series after changing the origin to `x`, denoted by `p.changeOrigin x k`, also become zero for `k` greater than or equal to `n`. This holds for any normed space over a non-trivially normed field.
More concisely: If a multilinear series `p` has zero terms for all indices greater than or equal to `n`, then changing the origin of `p` to `x` results in a series with zero terms for indices greater than or equal to `n`, for any normed space over a non-trivially normed field.
|