Iterating module-valued restricted series

Splitting the variables into two arbitrary sets identifies restricted coefficient families with iterated restricted families, isometrically for their Gauss norms at positive polyradii. The outer restrictedness condition concerns the Gauss norms of the slices, not just their individual coefficients. This distinction is essential for iterating analytic operations on module-valued series.

These lemmas generalise the scalar iteration argument, without ring or ultrametric assumptions on the coefficient group. The scalar equivalence TauCeti.MvPowerSeries.restrictedSumEquiv in TateAlgebra/Sum.lean is derived from them. The linear isometry works over any seminormed coefficient ring acting boundedly on the group. Neither completeness nor finitely many variables is required.

References

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

def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumSlice {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] (a : Gauss (Sum.elim c d) E) (s : σ →₀ ℕ) : Gauss d E

A slice of a jointly restricted family, with the exponents in σ fixed.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumSlice_apply {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] (a : Gauss (Sum.elim c d) E) (s : σ →₀ ℕ) (t : τ →₀ ℕ) : ↑(a.sumSlice s).toAddSubgroup t = ↑a.toAddSubgroup (s.sumElim t)

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.isRestrictedFamily_sumSlice {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] (a : Gauss (Sum.elim c d) E) : IsRestrictedFamily c a.sumSlice

The Gauss norms of the slices of a jointly restricted family themselves decay with the outer weights. Merely knowing that every slice is restricted would not suffice.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.isRestrictedFamily_flatten {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] (a : Gauss c (Gauss d E)) : IsRestrictedFamily (Sum.elim c d) fun (k : σ ⊕ τ →₀ ℕ) => ↑(↑a.toAddSubgroup (Finsupp.comapDomain Sum.inl k ⋯)).toAddSubgroup (Finsupp.comapDomain Sum.inr k ⋯)

Flattening restricted families of restricted families preserves joint restrictedness.

noncomputable def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumAddEquiv {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] : Gauss (Sum.elim c d) E ≃+ Gauss c (Gauss d E)

Splitting and flattening jointly restricted families are inverse additive maps.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumAddEquiv_apply {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] (a : Gauss (Sum.elim c d) E) (s : σ →₀ ℕ) (t : τ →₀ ℕ) : ↑(↑(sumAddEquiv a).toAddSubgroup s).toAddSubgroup t = ↑a.toAddSubgroup (s.sumElim t)

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumAddEquiv_symm_apply {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] (a : Gauss c (Gauss d E)) (s : σ →₀ ℕ) (t : τ →₀ ℕ) : ↑(sumAddEquiv.symm a).toAddSubgroup (s.sumElim t) = ↑(↑a.toAddSubgroup s).toAddSubgroup t

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_sumAddEquiv {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] (a : Gauss (Sum.elim c d) E) : ‖sumAddEquiv a‖ = ‖a‖

Iteration preserves the weighted Gauss norm, including at radii not realised by scalars.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.isometry_sumAddEquiv {σ : Type u_1} {τ : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] : Isometry ⇑sumAddEquiv

Splitting jointly restricted coefficient families is an isometry.

noncomputable def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumLinearIsometryEquiv {σ : Type u_1} {τ : Type u_2} {E : Type u_3} (R : Type u_4) [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] : Gauss (Sum.elim c d) E ≃ₗᵢ[R] Gauss c (Gauss d E)

Restricted module-valued series in disjoint sets of variables are isometrically the restricted series in the first variables with restricted-series coefficients in the second.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumLinearIsometryEquiv_apply {σ : Type u_1} {τ : Type u_2} {E : Type u_3} (R : Type u_4) [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : Gauss (Sum.elim c d) E) (s : σ →₀ ℕ) (t : τ →₀ ℕ) : ↑(↑((sumLinearIsometryEquiv R) a).toAddSubgroup s).toAddSubgroup t = ↑a.toAddSubgroup (s.sumElim t)

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumLinearIsometryEquiv_symm_apply {σ : Type u_1} {τ : Type u_2} {E : Type u_3} (R : Type u_4) [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : Gauss c (Gauss d E)) (s : σ →₀ ℕ) (t : τ →₀ ℕ) : ↑((sumLinearIsometryEquiv R).symm a).toAddSubgroup (s.sumElim t) = ↑(↑a.toAddSubgroup s).toAddSubgroup t

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumLinearIsometryEquiv_ofFinsupp_single {σ : Type u_1} {τ : Type u_2} {E : Type u_3} (R : Type u_4) [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (s : σ →₀ ℕ) (t : τ →₀ ℕ) (e : E) : (sumLinearIsometryEquiv R) ((ofFinsupp R (Sum.elim c d)) (Finsupp.single (s.sumElim t) e)) = (ofFinsupp R c) (Finsupp.single s ((ofFinsupp R d) (Finsupp.single t e)))

A single coefficient becomes a single outer coefficient with a single inner coefficient.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.sumLinearIsometryEquiv_mapLinearMap {σ : Type u_1} {τ : Type u_2} {E : Type u_3} {R : Type u_4} [SeminormedAddCommGroup E] {c : σ → ℝ} {d : τ → ℝ} [∀ (i : σ), Fact (0 < c i)] [∀ (j : τ), Fact (0 < d j)] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] {F : Type u_5} [SeminormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] (φ : E →ₗ[R] F) {C : ℝ} (hφ : ∀ (e : E), ‖φ e‖ ≤ C * ‖e‖) (a : Gauss (Sum.elim c d) E) : (sumLinearIsometryEquiv R) ((mapLinearMap φ hφ) a) = (mapLinearMap (mapLinearMap φ hφ) ⋯) ((sumLinearIsometryEquiv R) a)

Iteration commutes with bounded coefficient linear maps, acting on both levels of the iterated family.