Documentation

Mathlib.RingTheory.PowerSeries.Restricted

Univariate restricted power series #

IsRestricted : We say a univariate power series over a normed ring R is restricted for a real number c if ‖coeff t f‖ * c ^ t → 0 under the cofinite filter.

source
@[reducible, inline]
abbrev PowerSeries.IsRestricted {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) :
Prop

Predicate for when f is a restricted power series.

Equations
Instances For
    source
    theorem PowerSeries.isRestricted_iff {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) :
    IsRestricted c f ↔ Filter.Tendsto (fun (t : ℕ) => ‖(coeff t) f‖ * c ^ t) Filter.cofinite (nhds 0)
    source
    theorem PowerSeries.isRestricted_iff' {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) :
    IsRestricted c f ↔ Filter.Tendsto (fun (t : ℕ) => ‖(coeff t) f‖ * c ^ t) Filter.atTop (nhds 0)
    source
    @[simp]
    theorem PowerSeries.isRestricted_abs_iff {R : Type u_1} [NormedRing R] (c : ℝ) (f : PowerSeries R) :
    IsRestricted |c| f ↔ IsRestricted c f
    source
    theorem PowerSeries.isRestricted_zero {R : Type u_1} [NormedRing R] (c : ℝ) :
    IsRestricted c 0
    source
    theorem PowerSeries.isRestricted_monomial {R : Type u_1} [NormedRing R] (c : ℝ) (n : ℕ) (a : R) :
    IsRestricted c ((monomial n) a)
    source
    theorem PowerSeries.isRestricted_one {R : Type u_1} [NormedRing R] (c : ℝ) :
    IsRestricted c 1
    source
    theorem PowerSeries.isRestricted_C {R : Type u_1} [NormedRing R] (c : ℝ) (a : R) :
    IsRestricted c (C a)
    source
    @[deprecated MvPowerSeries.IsRestricted.add (since := "2026-09-28")]
    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)
    source
    @[deprecated MvPowerSeries.IsRestricted.neg (since := "2026-09-28")]
    theorem PowerSeries.isRestricted.neg {R : Type u_1} [NormedRing R] (c : ℝ) {f : PowerSeries R} (hf : IsRestricted c f) :
    IsRestricted c (-f)
    source
    @[deprecated MvPowerSeries.IsRestricted.mul (since := "2026-09-28")]
    theorem PowerSeries.isRestricted.mul {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) :
    IsRestricted c (f * g)
    source
    def PowerSeries.IsRestricted.addSubgroup {R : Type u_1} [NormedRing R] (c : ℝ) :
    AddSubgroup (PowerSeries R)

    Restricted power series as an additive subgroup of PowerSeries R.

    Equations
    Instances For
      source
      def PowerSeries.IsRestricted.subring {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) :
      Subring (PowerSeries R)

      Restricted power series as an subring of PowerSeries R.

      Equations
      Instances For