Multivariate restricted power series

IsRestricted : We say a multivariate power series over a normed ring R is restricted for a tuple c if ‖coeff t f‖ * ∏ i ∈ t.support, c i ^ t i → 0 under the cofinite filter.

def MvPowerSeries.IsRestricted {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (f : MvPowerSeries σ R) : Prop

A multivariate powe0r series over a normed ring R is restricted for a tuple c if ‖coeff t f‖ * ∏ i ∈ t.support, c i ^ t i → 0 under the cofinite filter.

Equations

• MvPowerSeries.IsRestricted c f = Filter.Tendsto (fun (t : σ →₀ ℕ) => ‖(MvPowerSeries.coeff t) f‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) Filter.cofinite (nhds 0)

@[simp]

theorem MvPowerSeries.isRestricted_abs_iff {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (f : MvPowerSeries σ R) : IsRestricted |c| f ↔ IsRestricted c f

theorem MvPowerSeries.isRestricted_zero {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) : IsRestricted c 0

theorem MvPowerSeries.isRestricted_monomial {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (n : σ →₀ ℕ) (a : R) : IsRestricted c ((monomial n) a)

theorem MvPowerSeries.isRestricted_one {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) : IsRestricted c 1

theorem MvPowerSeries.isRestricted_C {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (a : R) : IsRestricted c (C a)

theorem MvPowerSeries.isRestricted.add {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f + g)

theorem MvPowerSeries.isRestricted.neg {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f : MvPowerSeries σ R} (hf : IsRestricted c f) : IsRestricted c (-f)

theorem MvPowerSeries.tendsto_antidiagonal {M : Type u_3} {S : Type u_4} [AddMonoid M] [Finset.HasAntidiagonal M] [NormedRing S] [IsUltrametricDist S] {C : M → ℝ} (hC : ∀ (a b : M), C (a + b) = C a * C b) {f g : M → S} (hf : Filter.Tendsto (fun (i : M) => ‖f i‖ * C i) Filter.cofinite (nhds 0)) (hg : Filter.Tendsto (fun (i : M) => ‖g i‖ * C i) Filter.cofinite (nhds 0)) : Filter.Tendsto (fun (a : M) => ‖∑ p ∈ Finset.antidiagonal a, f p.1 * g p.2‖ * C a) Filter.cofinite (nhds 0)

theorem MvPowerSeries.isRestricted.mul {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f * g)

def MvPowerSeries.IsRestricted.addSubgroup {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) : AddSubgroup (MvPowerSeries σ R)

Restricted power series as an additive subgroup of MvPowerSeries σ R.

Equations

• MvPowerSeries.IsRestricted.addSubgroup c = { carrier := MvPowerSeries.IsRestricted c, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def MvPowerSeries.IsRestricted.subring {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) : Subring (MvPowerSeries σ R)

Restricted power series as a subring of MvPowerSeries σ R.

Equations

• MvPowerSeries.IsRestricted.subring c = { carrier := (MvPowerSeries.IsRestricted.addSubgroup c).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }