Restricted power series

IsRestricted : We say a power series over a normed ring R is restricted for a parameter c if ‖coeff R i f‖ * c ^ i → 0.

def PowerSeries.IsRestricted {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) : Prop

A power series over R is restricted of parameter c if we have ‖coeff R i f‖ * c ^ i → 0.

Equations

• PowerSeries.IsRestricted c f = Filter.Tendsto (fun (i : ℕ) => ‖(PowerSeries.coeff i) f‖ * c ^ i) Filter.atTop (nhds 0)

theorem PowerSeries.IsRestricted.isRestricted_iff {R : Type u_1} [NormedRing R] (c : ℝ) {f : PowerSeries R} : IsRestricted c f ↔ ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖‖(coeff n) f‖ * c ^ n‖ < ε

theorem PowerSeries.IsRestricted.isRestricted_iff_abs {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) : IsRestricted c f ↔ IsRestricted |c| f

theorem PowerSeries.IsRestricted.zero {R : Type u_1} [NormedRing R] (c : ℝ) : IsRestricted c 0

theorem PowerSeries.IsRestricted.one {R : Type u_1} [NormedRing R] (c : ℝ) : IsRestricted c 1

theorem PowerSeries.IsRestricted.monomial {R : Type u_1} [NormedRing R] (c : ℝ) (n : ℕ) (a : R) : IsRestricted c ((PowerSeries.monomial n) a)

theorem PowerSeries.IsRestricted.C {R : Type u_1} [NormedRing R] (c : ℝ) (a : R) : IsRestricted c (PowerSeries.C a)

theorem PowerSeries.IsRestricted.add {R : Type u_1} [NormedRing R] (c : ℝ) {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f + g)

theorem PowerSeries.IsRestricted.neg {R : Type u_1} [NormedRing R] (c : ℝ) {f : PowerSeries R} (hf : IsRestricted c f) : IsRestricted c (-f)

theorem PowerSeries.IsRestricted.smul {R : Type u_1} [NormedRing R] (c : ℝ) {f : PowerSeries R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f)

def PowerSeries.IsRestricted.convergenceSet {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) : Set ℝ

The set of ‖coeff R i f‖ * c ^ i for a given power series f and parameter c.

Equations

• PowerSeries.IsRestricted.convergenceSet c f = {x : ℝ | ∃ (i : ℕ), ‖(PowerSeries.coeff i) f‖ * c ^ i = x}

theorem PowerSeries.IsRestricted.convergenceSet_BddAbove {R : Type u_1} [NormedRing R] (c : ℝ) {f : PowerSeries R} (hf : IsRestricted c f) : BddAbove (convergenceSet c f)

theorem PowerSeries.IsRestricted.mul {R : Type u_1} [NormedRing R] (c : ℝ) [IsUltrametricDist R] {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f * g)