Evaluation of multivariate power series

Let σ, R, S be types, with CommRing R, CommRing S. One assumes that IsTopologicalRing R and IsUniformAddGroup 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, MvPowerSeries.eval₂ f φ a is the evaluation of the multivariate 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 satisfies two conditions bundled in MvPowerSeries.HasEval a :

• for all s : σ, a s is topologically nilpotent, meaning that (a s) ^ n tends to 0 when n tends to infinity
• when a s tends to zero for the filter of cofinite subsets of σ.

Under Continuous φ and HasEval a, the following lemmas furnish the properties of evaluation:

• MvPowerSeries.eval₂Hom: the evaluation of multivariate power series, as a ring morphism,
• MvPowerSeries.aeval: the evaluation map as an algebra morphism
• MvPowerSeries.uniformContinuous_eval₂: uniform continuity of the evaluation
• MvPowerSeries.continuous_eval₂: continuity of the evaluation
• MvPowerSeries.eval₂_eq_tsum: the evaluation is given by the sum of its monomials, evaluated.

structure MvPowerSeries.HasEval {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] (a : σ → S) : Prop

Families at which power series can be consistently evaluated

• hpow (s : σ) : IsTopologicallyNilpotent (a s)
• tendsto_zero : Filter.Tendsto a Filter.cofinite (nhds 0)

theorem MvPowerSeries.hasEval_def {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] (a : σ → S) : HasEval a ↔ (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧ Filter.Tendsto a Filter.cofinite (nhds 0)

theorem MvPowerSeries.HasEval.mono {σ : Type u_1} {S : Type u_4} [CommRing S] {a : σ → S} {t u : TopologicalSpace S} (h : t ≤ u) (ha : HasEval a) : HasEval a

theorem MvPowerSeries.HasEval.zero {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] : HasEval 0

theorem MvPowerSeries.HasEval.add {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [ContinuousAdd S] [IsLinearTopology S S] {a b : σ → S} (ha : HasEval a) (hb : HasEval b) : HasEval (a + b)

theorem MvPowerSeries.HasEval.mul_left {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] (c : σ → S) {x : σ → S} (hx : HasEval x) : HasEval (c * x)

theorem MvPowerSeries.HasEval.mul_right {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] (c : σ → S) {x : σ → S} (hx : HasEval x) : HasEval (x * c)

theorem MvPowerSeries.HasEval.map {σ : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] {S : Type u_3} [CommRing S] [TopologicalSpace S] {φ : R →+* S} (hφ : Continuous ⇑φ) {a : σ → R} (ha : HasEval a) : HasEval fun (s : σ) => φ (a s)

[Bourbaki, Algebra, chap. 4, §4, n°3, Prop. 4 (i) (a & b)][bourbaki1981].

theorem MvPowerSeries.HasEval.X {σ : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] : HasEval fun (s : σ) => X s

def MvPowerSeries.hasEvalIdeal {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] : Ideal (σ → S)

The domain of evaluation of MvPowerSeries, as an ideal

Equations

• MvPowerSeries.hasEvalIdeal = { carrier := {a : σ → S | MvPowerSeries.HasEval a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem MvPowerSeries.coe_hasEvalIdeal {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] : ↑hasEvalIdeal = {a : σ → S | HasEval a}

theorem MvPowerSeries.mem_hasEvalIdeal_iff {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] {a : σ → S} : a ∈ hasEvalIdeal ↔ HasEval a

theorem MvPolynomial.toMvPowerSeries_isUniformInducing {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] : IsUniformInducing toMvPowerSeries

theorem MvPolynomial.toMvPowerSeries_isDenseInducing {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] : IsDenseInducing toMvPowerSeries

theorem MvPolynomial.toMvPowerSeries_uniformContinuous {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsUniformAddGroup R] [IsUniformAddGroup S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : MvPowerSeries.HasEval a) : UniformContinuous ⇑(eval₂Hom φ a)

noncomputable def MvPowerSeries.eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (f : MvPowerSeries σ R) : S

Evaluation of a multivariate power series at f at a point a : σ → S.

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 HasEval a.

Equations

• MvPowerSeries.eval₂ φ a f = if H : ∃ (p : MvPolynomial σ R), ↑p = f then MvPolynomial.eval₂ φ a H.choose else ⋯.extend (MvPolynomial.eval₂ φ a) f

@[simp]

theorem MvPowerSeries.eval₂_coe {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (f : MvPolynomial σ R) : eval₂ φ a ↑f = MvPolynomial.eval₂ φ a f

@[simp]

theorem MvPowerSeries.eval₂_C {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (r : R) : eval₂ φ a ((C σ R) r) = φ r

@[simp]

theorem MvPowerSeries.eval₂_X {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (s : σ) : eval₂ φ a (X s) = a s

noncomputable def MvPowerSeries.eval₂Hom {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) : MvPowerSeries σ R →+* S

Evaluation of power series at adequate elements, as a RingHom

Equations

• MvPowerSeries.eval₂Hom hφ ha = IsDenseInducing.extendRingHom ⋯ ⋯ ⋯

theorem MvPowerSeries.eval₂Hom_eq_extend {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) (f : MvPowerSeries σ R) : (eval₂Hom hφ ha) f = ⋯.extend (MvPolynomial.eval₂ φ a) f

theorem MvPowerSeries.coe_eval₂Hom {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) : ⇑(eval₂Hom hφ ha) = eval₂ φ a

theorem MvPowerSeries.uniformContinuous_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) : UniformContinuous (eval₂ φ a)

theorem MvPowerSeries.continuous_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) : Continuous (eval₂ φ a)

theorem MvPowerSeries.hasSum_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) (f : MvPowerSeries σ R) : HasSum (fun (d : σ →₀ ℕ) => φ ((coeff R d) f) * d.prod fun (s : σ) (e : ℕ) => a s ^ e) (eval₂ φ a f)

theorem MvPowerSeries.eval₂_eq_tsum {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) (f : MvPowerSeries σ R) : eval₂ φ a f = ∑' (d : σ →₀ ℕ), φ ((coeff R d) f) * d.prod fun (s : σ) (e : ℕ) => a s ^ e

theorem MvPowerSeries.eval₂_unique {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) {ε : MvPowerSeries σ R → S} (hε : Continuous ε) (h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p) : ε = eval₂ φ a

theorem MvPowerSeries.comp_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) {T : Type u_4} [UniformSpace T] [CompleteSpace T] [T2Space T] [CommRing T] [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T] {ε : S →+* T} (hε : Continuous ⇑ε) : ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)

noncomputable def MvPowerSeries.aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) : MvPowerSeries σ R →ₐ[R] S

Evaluation of power series at adequate elements, as an AlgHom

Equations

• MvPowerSeries.aeval ha = { toRingHom := MvPowerSeries.eval₂Hom ⋯ ha, commutes' := ⋯ }

theorem MvPowerSeries.coe_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) : ⇑(aeval ha) = eval₂ (algebraMap R S) a

theorem MvPowerSeries.continuous_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) : Continuous ⇑(aeval ha)

@[simp]

theorem MvPowerSeries.aeval_coe {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) (p : MvPolynomial σ R) : (aeval ha) ↑p = (MvPolynomial.aeval a) p

theorem MvPowerSeries.aeval_unique {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] {ε : MvPowerSeries σ R →ₐ[R] S} (hε : Continuous ⇑ε) : aeval ⋯ = ε

theorem MvPowerSeries.hasSum_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) (f : MvPowerSeries σ R) : HasSum (fun (d : σ →₀ ℕ) => (coeff R d) f • d.prod fun (s : σ) (e : ℕ) => a s ^ e) ((aeval ha) f)

theorem MvPowerSeries.aeval_eq_sum {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) (f : MvPowerSeries σ R) : (aeval ha) f = ∑' (d : σ →₀ ℕ), (coeff R d) f • d.prod fun (s : σ) (e : ℕ) => a s ^ e

theorem MvPowerSeries.comp_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) {T : Type u_4} [CommRing T] [UniformSpace T] [IsUniformAddGroup T] [IsTopologicalRing T] [IsLinearTopology T T] [T2Space T] [Algebra R T] [ContinuousSMul R T] [CompleteSpace T] {ε : S →ₐ[R] T} (hε : Continuous ⇑ε) : ε.comp (aeval ha) = aeval ⋯