Gauss norms on module-valued restricted series

The wrapper IsRestrictedFamily.Gauss c E equips the existing restricted families with the weighted supremum seminorm at every positive real polyradius. Coefficient projections are bounded, bounded maps of coefficient modules induce bounded maps of restricted families, and convolution by a scalar restricted series satisfies the Gauss norm inequality. These estimates equip module-valued series with the norm needed for bounded analytic operations and presentations of coefficient modules. Bounded coefficient lifts give Gauss lifts with the same norm bound, so the induced map is open and is a quotient map. This extends the coefficient-lifting argument of TauCeti.MvPowerSeries.exists_restrictedMap_eq_and_norm_coeff_le to module coefficients.

Complete coefficient groups give complete restricted families. The construction allows arbitrary variable sets and seminormed additive coefficient groups. It is a norm for normed coefficients. Neither completeness nor an ultrametric norm is needed for the additive norm; the latter is required for the convolution estimate. For ring-valued coefficients, the existing comparison with scalar restricted series preserves the Gauss norm.

References

• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §5.1.1.

structure TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss {σ : Type u_1} (c : σ → ℝ) (E : Type u_5) [SeminormedAddCommGroup E] : Type (max u_1 u_5)

Restricted coefficient families with their Gauss topology at polyradius c. The wrapper keeps this topology separate from the pointwise topology inherited by the algebraic subgroup.

• ofAddSubgroup :: (
• toAddSubgroup : ↥(IsRestrictedFamily.addSubgroup E c)

  The underlying algebraic restricted family.

• )

@[instance_reducible]

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instCoeFunForallFinsuppNat {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} : CoeFun (Gauss c E) fun (x : Gauss c E) => (σ →₀ ℕ) → E

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.ext {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} {a b : Gauss c E} (h : ∀ (t : σ →₀ ℕ), ↑a.toAddSubgroup t = ↑b.toAddSubgroup t) : a = b

Gauss families are determined by their coefficients.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.ext_iff {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} {a b : Gauss c E} : a = b ↔ ∀ (t : σ →₀ ℕ), ↑a.toAddSubgroup t = ↑b.toAddSubgroup t

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroup_ofAddSubgroup {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a : ↥(IsRestrictedFamily.addSubgroup E c)) : { toAddSubgroup := a }.toAddSubgroup = a

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.ofAddSubgroup_toAddSubgroup {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a : Gauss c E) : { toAddSubgroup := a.toAddSubgroup } = a

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.ofAddSubgroup_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a : ↥(IsRestrictedFamily.addSubgroup E c)) (t : σ →₀ ℕ) : ↑{ toAddSubgroup := a }.toAddSubgroup t = ↑a t

@[instance_reducible]

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instAddCommGroup {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} : AddCommGroup (Gauss c E)

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroup_add {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a b : Gauss c E) : (a + b).toAddSubgroup = a.toAddSubgroup + b.toAddSubgroup

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.zero_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (t : σ →₀ ℕ) : ↑(toAddSubgroup 0) t = 0

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.neg_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a : Gauss c E) (t : σ →₀ ℕ) : ↑(-a).toAddSubgroup t = -↑a.toAddSubgroup t

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sub_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a b : Gauss c E) (t : σ →₀ ℕ) : ↑(a - b).toAddSubgroup t = ↑a.toAddSubgroup t - ↑b.toAddSubgroup t

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.add_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a b : Gauss c E) (t : σ →₀ ℕ) : ↑(a + b).toAddSubgroup t = ↑a.toAddSubgroup t + ↑b.toAddSubgroup t

def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroupAddEquiv {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} : Gauss c E ≃+ ↥(IsRestrictedFamily.addSubgroup E c)

The Gauss-topological family and the existing algebraic subgroup have the same addition.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroupAddEquiv_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a : Gauss c E) : toAddSubgroupAddEquiv a = a.toAddSubgroup

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroupAddEquiv_symm_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (a : ↥(IsRestrictedFamily.addSubgroup E c)) : toAddSubgroupAddEquiv.symm a = { toAddSubgroup := a }

@[instance_reducible]

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instModule {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] : Module R (Gauss c E)

def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroupLinearEquiv {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] : Gauss c E ≃ₗ[R] ↥(IsRestrictedFamily.addSubgroup E c)

Forgetting the Gauss topology preserves the coefficient-module action.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroupLinearEquiv_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : Gauss c E) : (toAddSubgroupLinearEquiv R) a = a.toAddSubgroup

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroupLinearEquiv_symm_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : ↥(IsRestrictedFamily.addSubgroup E c)) : (toAddSubgroupLinearEquiv R).symm a = { toAddSubgroup := a }

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.smul_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (r : R) (a : Gauss c E) (t : σ →₀ ℕ) : ↑(r • a).toAddSubgroup t = r • ↑a.toAddSubgroup t

noncomputable def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.ofFinsupp {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (c : σ → ℝ) : ((σ →₀ ℕ) →₀ E) →ₗ[R] Gauss c E

Include finite-support coefficient families in the Gauss-topological carrier.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.ofFinsupp_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} (R : Type u_5) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : (σ →₀ ℕ) →₀ E) (t : σ →₀ ℕ) : ↑((ofFinsupp R c) a).toAddSubgroup t = a t

def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.mapLinearMap {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} {R : Type u_5} [SeminormedRing R] [Module R E] [IsBoundedSMul R E] {F : Type u_6} [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) : Gauss c E →ₗ[R] Gauss c F

A bounded coefficient map induces a linear map of Gauss families.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.mapLinearMap_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} {R : Type u_5} [SeminormedRing R] [Module R E] [IsBoundedSMul R E] {F : Type u_6} [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) (a : Gauss c E) (t : σ →₀ ℕ) : ↑((mapLinearMap φ hφ) a).toAddSubgroup t = φ (↑a.toAddSubgroup t)

theorem LinearMap.toAddSubgroup_mapGaussFamily {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} {R : Type u_5} [SeminormedRing R] [Module R E] [IsBoundedSMul R E] {F : Type u_6} [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) (a : TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss c E) : ((TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.mapLinearMap φ hφ) a).toAddSubgroup = (TauCeti.MvPowerSeries.IsRestrictedFamily.mapLinearMap φ hφ) a.toAddSubgroup

Forgetting the Gauss topology commutes with a bounded coefficient map.

@[instance_reducible]

noncomputable instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instSeminormedAddCommGroup {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] : SeminormedAddCommGroup (Gauss c E)

Restricted families carry the weighted Gauss seminorm.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_eq_iSup {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] (a : Gauss c E) : ‖a‖ = ⨆ (t : σ →₀ ℕ), ‖↑a.toAddSubgroup t‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2

The norm is the supremum of the weighted coefficient norms. Restrictedness ensures that this supremum is bounded.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_coeff_mul_prod_le {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] (a : Gauss c E) (t : σ →₀ ℕ) : (‖↑a.toAddSubgroup t‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) ≤ ‖a‖

A weighted coefficient norm is bounded by the Gauss norm of the family.

@[instance_reducible]

noncomputable instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instNormedAddCommGroup {σ : Type u_1} {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] {F : Type u_5} [NormedAddCommGroup F] : NormedAddCommGroup (Gauss c F)

The Gauss seminorm is a norm when the coefficient seminorm is a norm.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_le_iff {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] {a : Gauss c E} {B : ℝ} : ‖a‖ ≤ B ↔ ∀ (t : σ →₀ ℕ), (‖↑a.toAddSubgroup t‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) ≤ B

A bound on the Gauss norm is equivalent to the same bound on every weighted coefficient.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_le_mul_of_norm_coeff_le {σ : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedAddCommGroup F] {a : Gauss c E} {b : Gauss c F} {L : ℝ} (h : ∀ (t : σ →₀ ℕ), ‖↑a.toAddSubgroup t‖ ≤ L * ‖↑b.toAddSubgroup t‖) : ‖a‖ ≤ L * ‖b‖

A uniform coefficient norm bound gives the same bound for the Gauss seminorm. The constant L may be any real number: if it is negative, all coefficients vanish.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_coeff_le {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] (a : Gauss c E) (t : σ →₀ ℕ) : ‖↑a.toAddSubgroup t‖ ≤ (t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2)⁻¹ * ‖a‖

Coefficient projections have bound the inverse of the monomial weight.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.uniformContinuous_coeff {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] (t : σ →₀ ℕ) : UniformContinuous fun (a : Gauss c E) => ↑a.toAddSubgroup t

Coefficients are uniformly continuous for the Gauss norm.

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instCompleteSpace {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [CompleteSpace E] : CompleteSpace (Gauss c E)

Complete coefficient groups give complete restricted families for the Gauss norm.

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instIsUltrametricDist {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [IsUltrametricDist E] : IsUltrametricDist (Gauss c E)

The Gauss norm is ultrametric whenever the coefficient norm is.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_ofFinsupp_single {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (t : σ →₀ ℕ) (e : E) : ‖(ofFinsupp R c) (Finsupp.single t e)‖ = ‖e‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2

A single-coefficient family has its weighted coefficient norm.

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instIsBoundedSMul {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] : IsBoundedSMul R (Gauss c E)

Coefficientwise scalar multiplication is bounded for the Gauss norm.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_mapLinearMap_le {σ : Type u_1} {E : Type u_2} {F : Type u_3} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) (a : Gauss c E) : ‖(mapLinearMap φ hφ) a‖ ≤ C * ‖a‖

A coefficient map bounded by C induces a map of restricted families with the same bound.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.uniformContinuous_mapLinearMap {σ : Type u_1} {E : Type u_2} {F : Type u_3} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) : UniformContinuous ⇑(mapLinearMap φ hφ)

The map induced by a bounded coefficient linear map is uniformly continuous.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.exists_mapLinearMap_eq_and_norm_le {σ : Type u_1} {E : Type u_2} {F : Type u_3} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) {L : ℝ} (hlift : ∀ (y : F), ∃ (x : E), φ x = y ∧ ‖x‖ ≤ L * ‖y‖) (b : Gauss c F) : ∃ (a : Gauss c E), (mapLinearMap φ hφ) a = b ∧ ‖a‖ ≤ L * ‖b‖

Bounded coefficient lifts give Gauss lifts with the same bound.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.isOpenMap_mapLinearMap {σ : Type u_1} {E : Type u_2} {F : Type u_3} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) {L : ℝ} (hlift : ∀ (y : F), ∃ (x : E), φ x = y ∧ ‖x‖ ≤ L * ‖y‖) : IsOpenMap ⇑(mapLinearMap φ hφ)

A bounded coefficient map with uniformly bounded lifts induces an open map of Gauss families, without completeness assumptions.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.isQuotientMap_mapLinearMap {σ : Type u_1} {E : Type u_2} {F : Type u_3} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) {L : ℝ} (hlift : ∀ (y : F), ∃ (x : E), φ x = y ∧ ‖x‖ ≤ L * ‖y‖) : Topology.IsQuotientMap ⇑(mapLinearMap φ hφ)

Bounded coefficient maps with uniformly bounded lifts induce quotient maps for the Gauss topologies at positive real polyradii.

@[instance_reducible]

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instNormedSpace {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] {K : Type u_5} [NormedField K] [NormedSpace K E] : NormedSpace K (Gauss c E)

Over a normed field, restricted families with normed-space coefficients form a normed space for the coefficientwise scalar action.

@[instance_reducible]

noncomputable instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instModuleSubtypeMvPowerSeriesMemSubringSubring {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [NormedRing R] [IsUltrametricDist R] [IsUltrametricDist E] [Module R E] [IsBoundedSMul R E] : Module (↥(MvPowerSeries.IsRestricted.subring c)) (Gauss c E)

The scalar restricted series act on Gauss families by convolution.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.toAddSubgroup_isRestrictedSubring_smul {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [NormedRing R] [IsUltrametricDist R] [IsUltrametricDist E] [Module R E] [IsBoundedSMul R E] (f : ↥(MvPowerSeries.IsRestricted.subring c)) (a : Gauss c E) : (f • a).toAddSubgroup = f • a.toAddSubgroup

Forgetting the Gauss topology preserves convolution by a restricted scalar series.

@[simp]

theorem LinearMap.mapGaussFamily_isRestrictedSubring_smul {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [NormedRing R] [IsUltrametricDist R] [IsUltrametricDist E] [Module R E] [IsBoundedSMul R E] {F : Type u_5} [SeminormedAddCommGroup F] [IsUltrametricDist F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) (f : ↥(MvPowerSeries.IsRestricted.subring c)) (a : TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss c E) : (TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.mapLinearMap φ hφ) (f • a) = f • (TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.mapLinearMap φ hφ) a

Bounded coefficient maps commute with convolution by scalar restricted series.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_isRestrictedSubring_smul_le {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [NormedRing R] [IsUltrametricDist R] [IsUltrametricDist E] [Module R E] [IsBoundedSMul R E] (f : ↥(MvPowerSeries.IsRestricted.subring c)) (a : Gauss c E) : ‖f • a‖ ≤ ‖f‖ * ‖a‖

Convolution by a scalar restricted series satisfies the Gauss norm inequality.

instance TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.instIsBoundedSMulSubtypeMvPowerSeriesMemSubringSubring {σ : Type u_1} {E : Type u_2} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [NormedRing R] [IsUltrametricDist R] [IsUltrametricDist E] [Module R E] [IsBoundedSMul R E] : IsBoundedSMul (↥(MvPowerSeries.IsRestricted.subring c)) (Gauss c E)

Restricted scalar series act by bounded scalar multiplication on restricted families.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_subringLinearEquiv {σ : Type u_1} {R : Type u_4} {c : σ → ℝ} [hc : ∀ (i : σ), Fact (0 < c i)] [NormedRing R] [IsUltrametricDist R] (f : ↥(MvPowerSeries.IsRestricted.subring c)) : ‖{ toAddSubgroup := subringLinearEquiv f }‖ = ‖f‖

The existing ring-valued coefficient comparison preserves the Gauss norm.