English
If q ≤ C p on a shell, then q ≤ C p on all x with p(x) ≠ 0.
Русский
Если q ≤ C p на оболочке, то q ≤ C p для всех x, у которых p(x) ≠ 0.
LaTeX
$$$ q(x) \\le C \\cdot p(x) \\;\\text{whenever } p(x) \\neq 0. $$$
Lean4
/-- Let `p` and `q` be two seminorms on a vector space over a `NontriviallyNormedField`.
If we have `q x ≤ C * p x` on some shell of the form `{x | ε/‖c‖ ≤ p x < ε}` (where `ε > 0`
and `‖c‖ > 1`), then we also have `q x ≤ C * p x` for all `x` such that `p x ≠ 0`. -/
theorem bound_of_shell (p q : Seminorm 𝕜 E) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖)
(hf : ∀ x, ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x) {x : E} (hx : p x ≠ 0) : q x ≤ C * p x :=
by
rcases p.rescale_to_shell hc ε_pos hx with ⟨δ, hδ, δxle, leδx, -⟩
simpa only [map_smul_eq_mul, mul_left_comm C, mul_le_mul_iff_right₀ (norm_pos_iff.2 hδ)] using hf (δ • x) leδx δxle
