Evaluation of power series #
Power series in one indeterminate are the particular case of multivariate power series,
for the Unit type of indeterminates.
This file provides a simpler syntax.
Let R, S be types, with CommRing R, CommRing S.
One assumes that IsTopologicalRing R and UniformAddGroup R,
and that S is a complete and separated topological R-algebra,
with IsLinearTopology S S, which means there is a basis of neighborhoods of 0
consisting of ideals.
Given φ : R →+* S, a : S, and f : MvPowerSeries σ R,
PowerSeries.eval₂ f φ a is the evaluation of the power series f at a.
It f is (the coercion of) a polynomial, it coincides with the evaluation of that polynomial.
Otherwise, it is defined by density from polynomials;
its values are irrelevant unless φ is continuous and a is topologically
nilpotent (a ^ n tends to 0 when n tends to infinity).
Under Continuous φ and IsTopologicallyNilpotent a,
the following lemmas furnish the properties of evaluation:
PowerSeries.eval₂Hom: the evaluation of multivariate power series, as a ring morphism,PowerSeries.aeval: the evaluation map as an algebra morphismPowerSeries.uniformContinuous_eval₂: uniform continuity of the evaluationPowerSeries.continuous_eval₂: continuity of the evaluationPowerSeries.eval₂_eq_tsum: the evaluation is given by the sum of its monomials, evaluated.
We refer to the documentation of MvPowerSeries.eval₂ for more details.
theorem
PowerSeries.hasEval
{S : Type u_2}
[CommRing S]
[TopologicalSpace S]
{a : S}
(ha : IsTopologicallyNilpotent a)
:
MvPowerSeries.HasEval fun (x : Unit) => a
noncomputable def
PowerSeries.eval₂
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
(φ : R →+* S)
(a : S)
[UniformSpace R]
[UniformSpace S]
:
PowerSeries R → S
Evaluation of a power series f at a point a.
It coincides with the evaluation of f as a polynomial if f is the coercion of a polynomial.
Otherwise, it is only relevant if φ is continuous and a is topologically nilpotent.
Equations
- PowerSeries.eval₂ φ a = MvPowerSeries.eval₂ φ fun (x : Unit) => a
Instances For
@[simp]
theorem
PowerSeries.eval₂_coe
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
(φ : R →+* S)
(a : S)
[UniformSpace R]
[UniformSpace S]
(f : Polynomial R)
:
@[simp]
theorem
PowerSeries.eval₂_C
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
(φ : R →+* S)
(a : S)
[UniformSpace R]
[UniformSpace S]
(r : R)
:
@[simp]
theorem
PowerSeries.eval₂_X
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
(φ : R →+* S)
(a : S)
[UniformSpace R]
[UniformSpace S]
:
noncomputable def
PowerSeries.eval₂Hom
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
:
The evaluation homomorphism at a on PowerSeries, as a RingHom.
Equations
- PowerSeries.eval₂Hom hφ ha = MvPowerSeries.eval₂Hom hφ ⋯
Instances For
theorem
PowerSeries.coe_eval₂Hom
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
:
theorem
PowerSeries.uniformContinuous_eval₂
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
:
UniformContinuous (eval₂ φ a)
theorem
PowerSeries.continuous_eval₂
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
:
Continuous (eval₂ φ a)
theorem
PowerSeries.hasSum_eval₂
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
(f : PowerSeries R)
:
theorem
PowerSeries.eval₂_eq_tsum
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
(f : PowerSeries R)
:
theorem
PowerSeries.eval₂_unique
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
{ε : PowerSeries R → S}
(hε : Continuous ε)
(h : ∀ (p : Polynomial R), ε ↑p = Polynomial.eval₂ φ a p)
:
theorem
PowerSeries.comp_eval₂
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{φ : R →+* S}
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
(hφ : Continuous ⇑φ)
(ha : IsTopologicallyNilpotent a)
{T : Type u_3}
[UniformSpace T]
[CompleteSpace T]
[T2Space T]
[CommRing T]
[IsTopologicalRing T]
[IsLinearTopology T T]
[UniformAddGroup T]
{ε : S →+* T}
(hε : Continuous ⇑ε)
:
noncomputable def
PowerSeries.aeval
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
:
For IsTopologicallyNilpotent a,
the evaluation homomorphism at a on PowerSeries, as an AlgHom.
Equations
Instances For
theorem
PowerSeries.coe_aeval
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
:
theorem
PowerSeries.continuous_aeval
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
:
Continuous ⇑(aeval ha)
@[simp]
theorem
PowerSeries.aeval_coe
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
(p : Polynomial R)
:
theorem
PowerSeries.aeval_unique
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
{ε : PowerSeries R →ₐ[R] S}
(hε : Continuous ⇑ε)
:
theorem
PowerSeries.hasSum_aeval
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
(f : PowerSeries R)
:
theorem
PowerSeries.aeval_eq_sum
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
(f : PowerSeries R)
:
theorem
PowerSeries.comp_aeval
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{a : S}
[UniformSpace R]
[UniformSpace S]
[UniformAddGroup R]
[IsTopologicalSemiring R]
[UniformAddGroup S]
[T2Space S]
[CompleteSpace S]
[IsTopologicalRing S]
[IsLinearTopology S S]
[Algebra R S]
[ContinuousSMul R S]
(ha : IsTopologicallyNilpotent a)
{T : Type u_3}
[CommRing T]
[UniformSpace T]
[UniformAddGroup T]
[IsTopologicalRing T]
[IsLinearTopology T T]
[T2Space T]
[Algebra R T]
[ContinuousSMul R T]
[CompleteSpace T]
{ε : S →ₐ[R] T}
(hε : Continuous ⇑ε)
: