Substitutions in power series #
A (possibly multivariate) power series can be substituted into a (univariate) power series if and only if its constant coefficient is nilpotent.
This is a particularization of the substitution of multivariate power series to the case of univariate power series.
Because of the special API for PowerSeries, some results for MvPowerSeries
do not immediately apply and a “primed” version is provided here.
@[reducible, inline]
(Possibly multivariate) power series which can be substituted in a PowerSeries.
Equations
- PowerSeries.HasSubst a = IsNilpotent ((MvPowerSeries.constantCoeff τ S) a)
Instances For
theorem
PowerSeries.hasSubst_iff
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
{a : MvPowerSeries τ S}
:
theorem
PowerSeries.HasSubst.const
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
:
MvPowerSeries.HasSubst fun (x : Unit) => a
theorem
PowerSeries.hasSubst_iff_hasEval_of_discreteTopology
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[TopologicalSpace S]
[DiscreteTopology S]
{a : MvPowerSeries τ S}
:
theorem
PowerSeries.HasSubst.hasEval
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[TopologicalSpace S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
:
HasEval a
theorem
PowerSeries.HasSubst.of_constantCoeff_zero
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
{a : MvPowerSeries τ S}
(ha : (MvPowerSeries.constantCoeff τ S) a = 0)
:
HasSubst a
theorem
PowerSeries.HasSubst.of_constantCoeff_zero'
{S : Type u_4}
[CommRing S]
{a : PowerSeries S}
(ha : (constantCoeff S) a = 0)
:
HasSubst a
A variant of HasSubst.of_constantCoeff_zero for PowerSeries
to avoid the expansion of Unit.
The univariate X : R⟦X⟧ can be substituted in power series
This lemma is added because simp doesn't find it from HasSubst.X.
theorem
PowerSeries.HasSubst.monomial
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
{n : τ →₀ ℕ}
(hn : n ≠ 0)
(s : S)
:
HasSubst ((MvPowerSeries.monomial S n) s)
A variant of HasSubst.monomial to avoid the expansion of Unit.
A variant of HasSubst.zero to avoid the expansion of Unit.
theorem
PowerSeries.HasSubst.add
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{f g : MvPowerSeries τ R}
(hf : HasSubst f)
(hg : HasSubst g)
:
theorem
PowerSeries.HasSubst.mul_left
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{f g : MvPowerSeries τ R}
(hf : HasSubst f)
:
theorem
PowerSeries.HasSubst.mul_right
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{f g : MvPowerSeries τ R}
(hf : HasSubst f)
:
theorem
PowerSeries.HasSubst.smul
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
(r : MvPowerSeries τ S)
{a : MvPowerSeries τ S}
(ha : HasSubst a)
:
noncomputable def
PowerSeries.HasSubst.ideal
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
:
Ideal (MvPowerSeries τ S)
Families of PowerSeries that can be substituted, as an Ideal.
Equations
- PowerSeries.HasSubst.ideal = { carrier := setOf PowerSeries.HasSubst, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
theorem
PowerSeries.HasSubst.smul'
{A : Type u_1}
[CommRing A]
{R : Type u_2}
[CommRing R]
[Algebra A R]
{τ : Type u_3}
{f : MvPowerSeries τ R}
(a : A)
(hf : HasSubst f)
:
A more general version of HasSubst.smul.
noncomputable def
PowerSeries.subst
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
(a : MvPowerSeries τ S)
(f : PowerSeries R)
:
MvPowerSeries τ S
Substitution of power series into a power series.
Equations
- PowerSeries.subst a f = MvPowerSeries.subst (fun (x : Unit) => a) f
Instances For
noncomputable def
PowerSeries.substAlgHom
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
:
Substitution of power series into a power series, as an AlgHom.
Equations
Instances For
theorem
PowerSeries.coe_substAlgHom
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
:
theorem
PowerSeries.substAlgHom_eq_aeval
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
[UniformSpace R]
[DiscreteUniformity R]
[UniformSpace S]
[DiscreteUniformity S]
(ha : HasSubst a)
:
Rewrite PowerSeries.substAlgHom as PowerSeries.aeval.
Its use is discouraged because it introduces a topology and might lead into awkward comparisons.
theorem
PowerSeries.subst_smul
{A : Type u_1}
[CommRing A]
{R : Type u_2}
[CommRing R]
[Algebra A R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
[Algebra A S]
[IsScalarTower A R S]
(ha : HasSubst a)
(r : A)
(f : PowerSeries R)
:
theorem
PowerSeries.coeff_subst_finite
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
(f : PowerSeries R)
(e : τ →₀ ℕ)
:
(Function.support fun (d : ℕ) => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)).Finite
theorem
PowerSeries.coeff_subst_finite'
{R : Type u_2}
[CommRing R]
{S : Type u_4}
[CommRing S]
[Algebra R S]
{b : PowerSeries S}
(hb : HasSubst b)
(f : PowerSeries R)
(e : ℕ)
:
theorem
PowerSeries.coeff_subst
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
(f : PowerSeries R)
(e : τ →₀ ℕ)
:
(MvPowerSeries.coeff S e) (subst a f) = ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)
theorem
PowerSeries.constantCoeff_subst
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
(f : PowerSeries R)
:
(MvPowerSeries.constantCoeff τ S) (subst a f) = ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.constantCoeff τ S) (a ^ d)
theorem
PowerSeries.map_algebraMap_eq_subst_X
{R : Type u_2}
[CommRing R]
{S : Type u_4}
[CommRing S]
[Algebra R S]
(f : PowerSeries R)
:
theorem
PowerSeries.substAlgHom_coe
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
(p : Polynomial R)
:
theorem
PowerSeries.substAlgHom_X
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
:
theorem
PowerSeries.subst_coe
{R : Type u_2}
[CommRing R]
{τ : Type u_3}
{S : Type u_4}
[CommRing S]
[Algebra R S]
{a : MvPowerSeries τ S}
(ha : HasSubst a)
(p : Polynomial R)
:
theorem
PowerSeries.HasSubst.comp
{S : Type u_4}
[CommRing S]
{υ : Type u_5}
{T : Type u_6}
[CommRing T]
[Algebra S T]
{a : PowerSeries S}
(ha : HasSubst a)
{b : MvPowerSeries υ T}
(hb : HasSubst b)
:
HasSubst ((substAlgHom hb) a)
theorem
PowerSeries.substAlgHom_comp_substAlgHom
{R : Type u_2}
[CommRing R]
{S : Type u_4}
[CommRing S]
{υ : Type u_5}
{T : Type u_6}
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
{a : PowerSeries S}
{b : MvPowerSeries υ T}
[IsScalarTower R S T]
(ha : HasSubst a)
(hb : HasSubst b)
:
theorem
PowerSeries.substAlgHom_comp_substAlgHom_apply
{R : Type u_2}
[CommRing R]
{S : Type u_4}
[CommRing S]
{υ : Type u_5}
{T : Type u_6}
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
{a : PowerSeries S}
{b : MvPowerSeries υ T}
[IsScalarTower R S T]
(ha : HasSubst a)
(hb : HasSubst b)
(f : PowerSeries R)
:
theorem
PowerSeries.subst_comp_subst
{R : Type u_2}
[CommRing R]
{S : Type u_4}
[CommRing S]
{υ : Type u_5}
{T : Type u_6}
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
{a : PowerSeries S}
{b : MvPowerSeries υ T}
[IsScalarTower R S T]
(ha : HasSubst a)
(hb : HasSubst b)
:
theorem
PowerSeries.subst_comp_subst_apply
{R : Type u_2}
[CommRing R]
{S : Type u_4}
[CommRing S]
{υ : Type u_5}
{T : Type u_6}
[CommRing T]
[Algebra R S]
[Algebra R T]
[Algebra S T]
{a : PowerSeries S}
{b : MvPowerSeries υ T}
[IsScalarTower R S T]
(ha : HasSubst a)
(hb : HasSubst b)
(f : PowerSeries R)
: