English
seminormFromBounded' is submultiplicative: seminormFromBounded'(f)(xy) ≤ seminormFromBounded'(f)(x) seminormFromBounded'(f)(y).
Русский
seminormFromBounded' является субумножаемой: seminormFromBounded'(f)(xy) ≤ seminormFromBounded'(f)(x) seminormFromBounded'(f)(y).
LaTeX
$$$\operatorname{seminormFromBounded}' f (x y) \le \operatorname{seminormFromBounded}' f x \cdot \operatorname{seminormFromBounded}' f y$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then for every `x : R`,
`f x ≤ f 1 * seminormFromBounded' f x`. -/
theorem seminormFromBounded_ge (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
f x ≤ f 1 * seminormFromBounded' f x := by
by_cases h1 : f 1 = 0
· specialize f_mul x 1
rw [mul_one, h1, mul_zero] at f_mul
have hx0 : f x = 0 := f_mul.antisymm (f_nonneg _)
rw [hx0, h1, zero_mul]
· rw [mul_comm, ← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) h1)]
conv_lhs => rw [← mul_one x]
exact le_ciSup (seminormFromBounded_bddAbove_range f_nonneg f_mul x) (1 : R)
