Power Series
Results named in Tau Ceti's TauCeti.RingTheory.PowerSeries modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe Bézout identity for the entire resultant#
For monic P and entire F there are an
entire series G and a polynomial H of degree less than deg P with
Res(P, F) = P * G + H * F.
Polynomial.exists_C_entireResultant_eq.{u_1} {R : Type u_1} [NormedCommRing R] [CompleteSpace R]
{P : Polynomial R} {F : PowerSeries R} (hP : P.Monic) (hF : F.IsEntire) :
∃ G,
G.IsEntire ∧
∃ H, H.degree < ↑P.natDegree ∧ PowerSeries.C (P.entireResultant F) = ↑P * G + ↑H * F
TheoremCauchy–Hadamard for entire series#
The n-th roots ‖aₙ‖ ^ (1 / n) of the coefficient
norms of an entire series tend to zero.
PowerSeries.IsEntire.tendsto_norm_coeff_rpow_inv_natCast.{u_1} {R : Type u_1} [NormedRing R]
{F : PowerSeries R} (hF : F.IsEntire) :
Filter.Tendsto (fun n => ‖(PowerSeries.coeff n) F‖ ^ (↑n)⁻¹) Filter.atTop (nhds 0)
Lean
Formalized in Tau Ceti as PowerSeries.IsEntire.tendsto_norm_coeff_rpow_inv_natCast.
Sources
TheoremCauchy–Hadamard formula#
the inverse of the radius of ∑ aₙ Xⁿ is
limsup ‖aₙ‖ ^ (1 / n).
PowerSeries.radius_inv_eq_limsup.{u_1} {R : Type u_1} [NormedRing R] {f : PowerSeries R} :
f.radius⁻¹ = Filter.limsup (fun n => ↑(‖(PowerSeries.coeff n) f‖₊ ^ (1 / ↑n))) Filter.atTop
Lean
Formalized in Tau Ceti as PowerSeries.radius_inv_eq_limsup.
Other forms
Cauchy–Hadamard formula, liminf form. Formalized in Tau Ceti as PowerSeries.radius_eq_liminf.
PowerSeries.radius_eq_liminf.{u_1} {R : Type u_1} [NormedRing R] {f : PowerSeries R} :
f.radius = Filter.liminf (fun n => 1 / ↑(‖(PowerSeries.coeff n) f‖₊ ^ (1 / ↑n))) Filter.atTop
Sources
TheoremFactor theorem for entire series#
An entire series vanishes at a exactly when it is
X - a times an entire series.
PowerSeries.IsEntire.evalAt_eq_zero_iff.{u_1} {R : Type u_1} [NormedCommRing R] {f : PowerSeries R}
[CompleteSpace R] (hf : f.IsEntire) {a : R} :
f.evalAt a = 0 ↔ ∃ q, q.IsEntire ∧ f = (PowerSeries.X - PowerSeries.C a) * q
TheoremHensel's lemma for K⟦t⟧#
Over a field K, the power series ring K⟦t⟧ is a Henselian
local ring. If a₀ is a root modulo t of a monic polynomial f with f' (a₀) a unit, its
constant coefficient c is a simple root of the reduction of f, which therefore factors as
(X - c) * h with X - c coprime to h; lifting this factorization
(Polynomial.Monic.exists_monic_mul_eq_of_isCoprime) gives a linear factor X - a of f with
a ≡ a₀ mod t.
PowerSeries.henselianLocalRing.{u_1} {K : Type u_1} [Field K] : HenselianLocalRing (PowerSeries K)
TheoremThe Taylor identity#
For an entire series f, the Taylor translate at a evaluated at
b is f(b + a).
PowerSeries.IsEntire.evalAt_taylor.{u_1} {R : Type u_1} [NormedCommRing R] {f : PowerSeries R}
[CompleteSpace R] (hf : f.IsEntire) (a b : R) :
(PowerSeries.taylor a f).evalAt b = f.evalAt (b + a)
Lean
Formalized in Tau Ceti as PowerSeries.IsEntire.evalAt_taylor.
Other forms
The Taylor identity for restricted series. Formalized in Tau Ceti as PowerSeries.IsRestricted.evalAt_taylor.
PowerSeries.IsRestricted.evalAt_taylor.{u_1} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R]
{c : ℝ} {f : PowerSeries R} {a b : R} [CompleteSpace R] (hf : PowerSeries.IsRestricted c f)
(ha : ‖a‖ ≤ c) (hb : ‖b‖ ≤ c) : (PowerSeries.taylor a f).evalAt b = f.evalAt (b + a)
The Taylor identity from the double series. Formalized in Tau Ceti as PowerSeries.evalAt_taylor_of_summable.
PowerSeries.evalAt_taylor_of_summable.{u_1} {R : Type u_1} [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [T2Space R] {f : PowerSeries R} {a b : R}
(hF :
Summable fun p => (PowerSeries.coeff p.2) ((PowerSeries.hasseDeriv p.1) f) * a ^ p.2 * b ^ p.1)
(hrow :
∀ (n : ℕ),
HasSum (fun m => (PowerSeries.coeff m) ((PowerSeries.hasseDeriv n) f) • a ^ m)
(((PowerSeries.hasseDeriv n) f).evalAt a)) :
(PowerSeries.taylor a f).evalAt b = f.evalAt (b + a)
Sources
Used by 1
TheoremThe Taylor remainder estimate#
Over a complete ultrametric normed ring, let f be
restricted at a radius c > 0 and let ‖a‖ ≤ c, ‖y‖ ≤ c. If ε bounds the first T terms
‖(Δᵗ f)(a)‖ ‖y‖ᵗ, t < T, of the expansion of f at a, then
‖f(y + a)‖ ≤ max ε (‖f‖_c * (‖y‖ / c) ^ T).
For ε = 0 this is the Schwarz lemma at a single zero of order T.
PowerSeries.IsRestricted.norm_evalAt_add_le_max.{u_1} {R : Type u_1} [NormedCommRing R]
[IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} {a : R} [CompleteSpace R]
(hf : PowerSeries.IsRestricted c f) (hc : 0 < c) (ha : ‖a‖ ≤ c) {y : R} (hy : ‖y‖ ≤ c) {T : ℕ}
{ε : ℝ} (h : ∀ t < T, ‖((PowerSeries.hasseDeriv t) f).evalAt a‖ * ‖y‖ ^ t ≤ ε) :
‖f.evalAt (y + a)‖ ≤ max ε (PowerSeries.gaussNorm norm c f * (‖y‖ / c) ^ T)
Lean
Formalized in Tau Ceti as PowerSeries.IsRestricted.norm_evalAt_add_le_max.
Sources
Uses 1
TheoremThe Whitney formula for roots#
on the union of a family s of n roots and a family t
of m roots, Kₖ is the convolution of the values of the multiplicative sequence on s and
on t.
PowerSeries.aeval_multiset_esymm_add_multiplicativeSequence.{u_1, u_2} {R : Type u_1} [CommRing R]
(Q : PowerSeries R) (n k : ℕ) {S : Type u_2} [CommSemiring S] [Algebra R S] {m : ℕ}
(s t : Multiset S) (hs : s.card = n) (ht : t.card = m) :
(MvPolynomial.aeval fun j => (s + t).esymm (↑j + 1)) (Q.multiplicativeSequence (n + m) k) =
∑ p ∈ Finset.HasAntidiagonal.antidiagonal k,
(MvPolynomial.aeval fun j => s.esymm (↑j + 1)) (Q.multiplicativeSequence n p.1) *
(MvPolynomial.aeval fun j => t.esymm (↑j + 1)) (Q.multiplicativeSequence m p.2)
Lean
Formalized in Tau Ceti as PowerSeries.aeval_multiset_esymm_add_multiplicativeSequence.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.