English
For fixed x, the range of y ↦ f(x y)/f y is bounded above, by c f x.
Русский
Для фиксированного x множество значений y ↦ f(xy)/f(y) ограничено сверху величиной c f x.
LaTeX
$$$\operatorname{Range}\;\bigl( y \mapsto \frac{f(xy)}{f(y)}\bigr) \text{ is bounded above by } c f x$$$
Lean4
theorem seminormFromBounded_aux (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
0 ≤ c * f x := by
rcases (f_nonneg x).eq_or_lt' with hx | hx
· simp [hx]
· change 0 < f x at hx
have hc : 0 ≤ c := by
specialize f_mul x 1
rw [mul_one, show c * f x * f 1 = c * f 1 * f x by ring, le_mul_iff_one_le_left hx] at f_mul
replace f_nonneg : 0 ≤ f 1 := f_nonneg 1
rcases f_nonneg.eq_or_lt' with h1 | h1
· linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]
· rw [← div_le_iff₀ h1] at f_mul
linarith [one_div_pos.mpr h1]
positivity
