English
Under mild hypotheses (nonnegativity, submultiplicativity, subadditivity, and preservation of zero and negation) the seminorm from boundedness is a norm if and only if its kernel is trivial.
Русский
При слабых гипотезах (неотрицательность, субумножение, субаддитивность и сохранение нуля и отрицания) семинормFromBounded является нормой тогда и только тогда, когда его ядро тривиально.
LaTeX
$$$\big( f(0)=0,\ 0\le f,\ f(xy) \le c f(x) f(y),\ f(a+b) \le f(a)+f(b),\ f(-x)=f(x) \big) \Rightarrow\Big( \big( \forall x, (\operatorname{seminormFromBounded} f) x =0 \Rightarrow x=0\ big) \; \Leftrightarrow\; f^{-1}({0})={0} \Big)$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded, subadditive function that preserves
zero and negation, then `seminormFromBounded' f` is a norm if and only if `f⁻¹' {0} = {0}`. -/
theorem seminormFromBounded_is_norm_iff (f_zero : f 0 = 0) (f_nonneg : 0 ≤ f)
(f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (f_add : ∀ a b, f (a + b) ≤ f a + f b)
(f_neg : ∀ x : R, f (-x) = f x) :
(∀ x : R, (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0} :=
by
refine ⟨fun h0 ↦ ?_, fun h_ker x hx ↦ ?_⟩
· rw [← seminormFromBounded_ker f_nonneg f_mul]
ext x
simp only [Set.mem_preimage, Set.mem_singleton_iff]
exact ⟨fun h ↦ h0 x h, fun h ↦ by rw [h]; exact seminormFromBounded_zero f_zero⟩
· rw [← Set.mem_singleton_iff, ← h_ker, Set.mem_preimage, Set.mem_singleton_iff, ←
seminormFromBounded_eq_zero_iff f_nonneg f_mul x]
exact hx
