Theorems · Theorem · functional analysis

Seminorm.rescale_to_shell_zpow

∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ {x : E}, p x ≠ 0 → ∃ n, c ^ n ≠ 0 ∧ p (c ^ n • x) < ε ∧ ε / ‖c‖ ≤ p (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x

Let p be a seminorm on a vector space over a NormedField. If there is a scalar c with ‖c‖>1, then any x such that p x ≠ 0 can be moved by scalar multiplication to any p-shell of width ‖c‖. Also recap information on the value of p on the rescaling element that shows up in applications.

Defined in

Mathlib.Analysis.Seminorm

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldAddCommGroupModule