Documentation

TauCeti.RingTheory.PowerSeries.Entire.Eval

Evaluation of entire power series #

For a power series f = ∑ aₙ Xⁿ over a commutative ring R and an element b of an R-algebra A, PowerSeries.evalAt f b is the infinite sum ∑ₙ aₙ • bⁿ, with the junk value 0 when the sum does not converge. When R is normed, A is a complete seminormed ring with ‖r • x‖ ≤ ‖r‖ ‖x‖, and f is entire, the sum converges absolutely at every b: since f is restricted at the radius 2 ‖b‖, its terms are bounded by a constant times 2⁻ⁿ. No ultrametric hypothesis is needed for convergence, so this evaluates entire series both at operators on p-adic Banach spaces and in complex Banach algebras. When A is normed, evaluation at b is a ring homomorphism on the subring of entire series (PowerSeries.IsEntire.evalAtHom). Evaluation commutes with continuous algebra homomorphisms into Hausdorff algebras.

The same bound shows that an entire series F = ∑ Fₙ Xⁿ with coefficients in a complete normed ring, such as a series of operators, can be evaluated at every scalar: the sum PowerSeries.evalScalar F a = ∑ₙ aⁿ • Fₙ converges absolutely.

A consequence used for Fredholm determinants: if f(0) = 1 and f(a) = 0, then a is a unit with inverse -∑ₙ aₙ₊₁ • aⁿ, since f(a) = 1 + a ∑ₙ aₙ₊₁ • aⁿ.

The same identity f(x) = a₀ + x ∑ₙ aₙ₊₁ • xⁿ, together with continuity of f at 0, gives an identity principle over coefficient rings: an entire series over a complete normed commutative ring vanishing at non-zero-divisors accumulating at 0 is zero. Over Tate scalars, where the powers of a pseudo-uniformiser are such points, an entire series is therefore determined by its values.

Main definitions #

Main results #

References #

source
theorem PowerSeries.IsEntire.summable_norm_smul_pow {R : Type u_1} {A : Type u_2} [NormedRing R] [SeminormedRing A] [SMulZeroClass R A] [IsBoundedSMul R A] {f : PowerSeries R} (hf : f.IsEntire) (b : A) :
Summable fun (n : ℕ) => ‖(coeff n) f • b ^ n‖

For an entire series f = ∑ aₙ Xⁿ, the terms aₙ • bⁿ are absolutely summable.

source
theorem PowerSeries.IsEntire.summable_smul_pow {R : Type u_1} {A : Type u_2} [NormedRing R] [SeminormedRing A] [SMulZeroClass R A] [IsBoundedSMul R A] {f : PowerSeries R} [CompleteSpace A] (hf : f.IsEntire) (b : A) :
Summable fun (n : ℕ) => (coeff n) f • b ^ n

For an entire series f = ∑ aₙ Xⁿ, the terms aₙ • bⁿ are summable in a complete seminormed ring with a bounded scalar action.

source
theorem PowerSeries.IsEntire.norm_evalAt_le {R : Type u_1} {A : Type u_2} [NormedCommRing R] [SeminormedRing A] [Algebra R A] [IsBoundedSMul R A] {f : PowerSeries R} [NormOneClass A] (hf : f.IsEntire) (b : A) :
‖f.evalAt b‖ ≤ ∑' (n : ℕ), ‖(coeff n) f‖ * ‖b‖ ^ n

In a seminormed algebra with ‖1‖ = 1, ‖f(b)‖ ≤ ∑ ‖aₙ‖ ‖b‖ⁿ.

source
theorem PowerSeries.IsEntire.hasSum_evalAt {R : Type u_1} {A : Type u_2} [NormedCommRing R] [SeminormedRing A] [Algebra R A] [IsBoundedSMul R A] {f : PowerSeries R} [CompleteSpace A] (hf : f.IsEntire) (b : A) :
HasSum (fun (n : ℕ) => (coeff n) f • b ^ n) (f.evalAt b)

Evaluation of entire series. For an entire series f = ∑ aₙ Xⁿ and any b in a complete seminormed algebra, the series ∑ aₙ • bⁿ converges to f(b).

source
theorem PowerSeries.IsEntire.tendsto_aeval_trunc {R : Type u_1} {A : Type u_2} [NormedCommRing R] [SeminormedRing A] [Algebra R A] [IsBoundedSMul R A] {f : PowerSeries R} [CompleteSpace A] (hf : f.IsEntire) (b : A) :
Filter.Tendsto (fun (n : ℕ) => (Polynomial.aeval b) ((trunc n) f)) Filter.atTop (nhds (f.evalAt b))

The truncations of an entire series f, evaluated at any b in a complete seminormed algebra, converge to f(b).

source
theorem PowerSeries.IsEntire.map_evalAt {R : Type u_1} {A : Type u_2} [NormedCommRing R] [SeminormedRing A] [Algebra R A] [IsBoundedSMul R A] {f : PowerSeries R} [CompleteSpace A] {B : Type u_3} {F : Type u_4} [Semiring B] [Algebra R B] [TopologicalSpace B] [T2Space B] [FunLike F A B] [AlgHomClass F R A B] (hf : f.IsEntire) (ψ : F) (hψ : Continuous ⇑ψ) (b : A) :
ψ (f.evalAt b) = f.evalAt (ψ b)

Evaluation of entire series commutes with continuous algebra homomorphisms: ψ (f(b)) = f(ψ b).

source
theorem PowerSeries.IsEntire.evalAt_add {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (b : A) :
(f + g).evalAt b = f.evalAt b + g.evalAt b

Evaluation is additive on entire series.

source
theorem PowerSeries.IsEntire.evalAt_sub {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (b : A) :
(f - g).evalAt b = f.evalAt b - g.evalAt b

Evaluation commutes with subtraction of entire series.

source
theorem PowerSeries.IsEntire.evalAt_smul {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f : PowerSeries R} (hf : f.IsEntire) (a : R) (b : A) :
(a • f).evalAt b = a • f.evalAt b

Evaluation commutes with scalar multiplication of entire series.

source
theorem PowerSeries.IsEntire.evalAt_sum {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {ι : Type u_3} (s : Finset ι) {f : ι → PowerSeries R} (hf : ∀ i ∈ s, (f i).IsEntire) (b : A) :
(∑ i ∈ s, f i).evalAt b = ∑ i ∈ s, (f i).evalAt b

Evaluation commutes with finite sums of entire series.

source
theorem PowerSeries.IsEntire.evalAt_mul {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f g : PowerSeries R} (hf : f.IsEntire) (hg : g.IsEntire) (b : A) :
(f * g).evalAt b = f.evalAt b * g.evalAt b

Evaluation is multiplicative on entire series: this is the Cauchy product formula for the absolutely convergent series ∑ aₙ • bⁿ and ∑ cₙ • bⁿ.

source
noncomputable def PowerSeries.IsEntire.evalAtHom (R : Type u_1) {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] (b : A) :
↥(IsEntire.subring R) →+* A

Evaluation of entire series at b as a ring homomorphism from the subring of entire series to a complete normed algebra.

Instances For
    source
    @[simp]
    theorem PowerSeries.IsEntire.evalAtHom_apply {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] (b : A) (f : ↥(IsEntire.subring R)) :
    (evalAtHom R b) f = (↑f).evalAt b

    The evaluation homomorphism at b sends an entire series f to f(b).

    source
    theorem PowerSeries.IsEntire.evalAt_pow {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f : PowerSeries R} (hf : f.IsEntire) (n : ℕ) (b : A) :
    (f ^ n).evalAt b = f.evalAt b ^ n

    Evaluation commutes with powers of entire series.

    source
    theorem PowerSeries.IsEntire.evalAt_map {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} {S : Type u_3} [CommSemiring S] [TopologicalSpace S] [T2Space S] [CompleteSpace R] (hf : f.IsEntire) (φ : R →+* S) (hφ : Continuous ⇑φ) (a : R) :
    ((PowerSeries.map φ) f).evalAt (φ a) = φ (f.evalAt a)

    Evaluation of entire series commutes with continuous coefficient homomorphisms: (φ f)(φ a) = φ (f(a)).

    source
    @[simp]
    theorem PowerSeries.IsEntire.evalAt_hasseDeriv_X_sub_C_pow_mul {R : Type u_1} [NormedCommRing R] {g : PowerSeries R} [CompleteSpace R] (hg : g.IsEntire) (a : R) (m j : ℕ) :
    ((PowerSeries.hasseDeriv j) ((X - C a) ^ m * g)).evalAt a = if m ≤ j then ((PowerSeries.hasseDeriv (j - m)) g).evalAt a else 0

    Evaluated Leibniz rule at a for (X - a)ᵐ g. For entire g, the Hasse derivative of order j of (X - a)ᵐ g at a is the Hasse derivative of order j - m of g at a when m ≤ j, and 0 otherwise.

    source
    theorem PowerSeries.IsEntire.evalAt_eq_algebraMap_add_mul {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f : PowerSeries R} (hf : f.IsEntire) (b : A) :
    f.evalAt b = (algebraMap R A) (constantCoeff f) + b * (mk fun (n : ℕ) => (coeff (n + 1)) f).evalAt b

    The value of an entire series at b is a₀ + b ∑ₙ aₙ₊₁ • bⁿ.

    source
    theorem PowerSeries.IsEntire.isUnit_of_evalAt_eq_zero {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f : PowerSeries R} (hf : f.IsEntire) (h0 : constantCoeff f = 1) {a : A} (ha : f.evalAt a = 0) :
    IsUnit a

    Zeros of entire series with constant coefficient 1 are units. If an entire series f with f(0) = 1 vanishes at a, then a is invertible.

    source
    theorem PowerSeries.IsEntire.inverse_eq_of_evalAt_eq_zero {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f : PowerSeries R} (hf : f.IsEntire) (h0 : constantCoeff f = 1) {a : A} (ha : f.evalAt a = 0) :
    Ring.inverse a = -(mk fun (n : ℕ) => (coeff (n + 1)) f).evalAt a

    If an entire series f = ∑ aₙ Xⁿ with a₀ = 1 vanishes at a, then the inverse of a is -∑ₙ aₙ₊₁ • aⁿ.

    source
    theorem PowerSeries.IsEntire.tendsto_evalAt_nhds_zero_nhds_constantCoeff {R : Type u_1} {A : Type u_2} [NormedCommRing R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [CompleteSpace A] {f : PowerSeries R} (hf : f.IsEntire) :
    Filter.Tendsto (fun (b : A) => f.evalAt b) (nhds 0) (nhds ((algebraMap R A) (constantCoeff f)))

    Continuity at 0. For an entire series f = ∑ aₙ Xⁿ, the value f(b) tends to f(0) = a₀ as b tends to 0.

    source
    theorem PowerSeries.IsEntire.eq_zero_of_frequently_evalAt_eq_zero {R : Type u_1} [NormedCommRing R] {f : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (h : ∃ᶠ (x : R) in nhds 0, x ∈ nonZeroDivisors R ∧ f.evalAt x = 0) :
    f = 0

    Identity principle for entire series over a ring. An entire series over a complete normed commutative ring that vanishes at non-zero-divisors accumulating at 0 is zero. Over a normed field the non-zero-divisors are the nonzero elements; over Tate scalars the powers of a pseudo-uniformiser are non-zero-divisors tending to 0.

    source
    theorem PowerSeries.IsEntire.eq_of_forall_evalAt_eq {R : Type u_1} [NormedCommRing R] {f g : PowerSeries R} [CompleteSpace R] (hf : f.IsEntire) (hg : g.IsEntire) (hR : ∃ᶠ (x : R) in nhds 0, x ∈ nonZeroDivisors R) (h : ∀ (x : R), f.evalAt x = g.evalAt x) :
    f = g

    Entire series are determined by their values over a complete normed commutative ring in which non-zero-divisors accumulate at 0, such as a nontrivially normed field or a ring with Tate scalars.

    source
    theorem PowerSeries.IsEntire.summable_norm_pow_smul_coeff {R : Type u_1} {A : Type u_2} [SeminormedRing R] [NormedRing A] {F : PowerSeries A} [SMulZeroClass R A] [IsBoundedSMul R A] (hF : F.IsEntire) (a : R) :
    Summable fun (n : ℕ) => ‖a ^ n • (coeff n) F‖

    For an entire series F = ∑ Fₙ Xⁿ over a normed ring, the terms aⁿ • Fₙ of its value at a scalar a are absolutely summable.

    source
    theorem PowerSeries.IsEntire.hasSum_evalScalar {R : Type u_1} {A : Type u_2} [SeminormedRing R] [NormedRing A] {F : PowerSeries A} [SMulZeroClass R A] [IsBoundedSMul R A] [CompleteSpace A] (hF : F.IsEntire) (a : R) :
    HasSum (fun (n : ℕ) => a ^ n • (coeff n) F) (F.evalScalar a)

    Evaluation of entire series at scalars. For an entire series F = ∑ Fₙ Xⁿ over a complete normed ring and any scalar a, the series ∑ aⁿ • Fₙ converges to F(a).

    source
    theorem PowerSeries.IsEntire.evalScalar_add {R : Type u_1} {A : Type u_2} [SeminormedRing R] [NormedRing A] {F : PowerSeries A} [DistribMulAction R A] [IsBoundedSMul R A] [CompleteSpace A] {G : PowerSeries A} (hF : F.IsEntire) (hG : G.IsEntire) (a : R) :
    (F + G).evalScalar a = F.evalScalar a + G.evalScalar a

    Evaluation at a scalar is additive on entire series over a complete normed ring.