English
A variant of rescaling to shell with a prime marker.
Русский
Вариант переноса в оболочку с пометой prime.
LaTeX
$$$ p.rescale_to_shell' (hc) (ε) (x) (hx) : \\exists d, d \\,\\neq \\,0 \\land p(d x) < \\epsilon \\land \\epsilon / \\|d\\| \\le p(x). $$$
Lean4
/-- 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. -/
theorem rescale_to_shell (p : Seminorm 𝕜 E) {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : p x ≠ 0) :
∃ d : 𝕜, d ≠ 0 ∧ p (d • x) < ε ∧ (ε / ‖c‖ ≤ p (d • x)) ∧ (‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x) :=
let ⟨_, hn⟩ := p.rescale_to_shell_zpow hc εpos hx;
⟨_, hn⟩
