English
There exists a rescaling factor d with d ≠ 0 such that p(d x) lies in a prescribed shell while staying within bounds in terms of x.
Русский
Существует коэффициент масштабирования d ≠ 0, при котором p(d x) попадает в заданную оболочку и управляет пределами в зависимости от x.
LaTeX
$$$ \\exists d \\neq 0:\\; p(d x) \\text{ satisfies shell inequalities with respect to } 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_zpow (p : Seminorm 𝕜 E) {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : p x ≠ 0) :
∃ n : ℤ, c ^ n ≠ 0 ∧ p (c ^ n • x) < ε ∧ (ε / ‖c‖ ≤ p (c ^ n • x)) ∧ (‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x) :=
by
have xεpos : 0 < (p x) / ε := by positivity
rcases exists_mem_Ico_zpow xεpos hc with ⟨n, hn⟩
have cpos : 0 < ‖c‖ := by positivity
have cnpos : 0 < ‖c ^ (n + 1)‖ := by rw [norm_zpow]; exact xεpos.trans hn.2
refine ⟨-(n + 1), ?_, ?_, ?_, ?_⟩
· show c ^ (-(n + 1)) ≠ 0; exact zpow_ne_zero _ (norm_pos_iff.1 cpos)
· show p ((c ^ (-(n + 1))) • x) < ε
rw [map_smul_eq_mul, zpow_neg, norm_inv, ← div_eq_inv_mul, div_lt_iff₀ cnpos, mul_comm, norm_zpow]
exact (div_lt_iff₀ εpos).1 (hn.2)
· show ε / ‖c‖ ≤ p (c ^ (-(n + 1)) • x)
rw [zpow_neg, div_le_iff₀ cpos, map_smul_eq_mul, norm_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos), zpow_one,
mul_inv_rev, mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel₀ (ne_of_gt cpos), one_mul, ← div_eq_inv_mul,
le_div_iff₀ (zpow_pos cpos _), mul_comm]
exact (le_div_iff₀ εpos).1 hn.1
· show ‖(c ^ (-(n + 1)))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x
have : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖ := by ring
rw [zpow_neg, norm_inv, inv_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos), zpow_one, this, ← div_eq_inv_mul]
exact mul_le_mul_of_nonneg_right hn.1 (norm_nonneg _)
