English
If there exists c with ||c|| > 1, then for any nonzero x there exists n ∈ ℤ with c^n ≠ 0 such that ||c^n x|| < ε, ε/||c|| ≤ ||c^n x||, and ||c^n||^{-1} ≤ ε^{-1} ||c|| ||x||.
Русский
Если существует c с ||c|| > 1, то для любого ненулевого x существует n ∈ ℤ такое, что c^n ≠ 0 и выполняются неравенства: ||c^n x|| < ε, ε/||c|| ≤ ||c^n x||, и ||c^n||^{-1} ≤ ε^{-1} ||c|| ||x||.
LaTeX
$$$\exists n \in \mathbb{Z},\ c^n \neq 0 \wedge \|c^n \cdot x\| < \varepsilon \wedge (\varepsilon / \|c\| \le \|c^n \cdot x\|) \wedge (\|c^n\|^{-1} \le \varepsilon^{-1} \cdot \|c\| \cdot \|x\|).$$$
Lean4
/-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
the rescaling element that shows up in applications. -/
theorem rescale_to_shell_semi_normed_zpow {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : ‖x‖ ≠ 0) :
∃ n : ℤ, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ (ε / ‖c‖ ≤ ‖c ^ n • x‖) ∧ (‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖) :=
(normSeminorm 𝕜 E).rescale_to_shell_zpow hc εpos hx
