Theorems · Theorem · commutative algebra

RingSeminorm.isBoundedUnder

∀ {R : Type u_1} [inst : Ring R] (p : RingSeminorm R),
  p 1 ≤ 1 →
    ∀ {s : ℕ → ℕ},
      (∀ (n : ℕ), s n ≤ n) →
        ∀ {x : R} (ψ : ℕ → ℕ), Filter.IsBoundedUnder LE.le Filter.atTop fun n => p (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

If f is a ring seminorm on R with f 1 ≤ 1 and s : ℕ → ℕ is bounded by n, then f (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) is eventually bounded.

Defined in

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Cited by

1 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring