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
theorem rescale_to_shell_zpow [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε)
{x : F} (hx : x ≠ 0) :
∃ n : ℤ, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ (ε / ‖c‖ ≤ ‖c ^ n • x‖) ∧ (‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖) :=
rescale_to_shell_semi_normed_zpow hc εpos (norm_ne_zero_iff.mpr hx)
