English
If f is nonnegative and x is multiplicative for f, then x is multiplicative for seminormFromBounded' f; i.e., seminormFromBounded' f (xy) = seminormFromBounded' f x · seminormFromBounded' f y for all y.
Русский
Если f неотрицательная и x мультипликативна для f, то x мультипликативна и для seminormFromBounded' f; то есть для всех y выполняется равенство
seminormFromBounded' f (xy) = seminormFromBounded' f x · seminormFromBounded' f y.
LaTeX
$$$(\forall y,\ f(xy)=f(x)f(y)) \Rightarrow \forall y,\; \operatorname{seminormFromBounded'} f (xy) = \operatorname{seminormFromBounded'} f x \cdot \operatorname{seminormFromBounded'} f y$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function and `x : R` is
multiplicative for `f`, then `x` is multiplicative for `seminormFromBounded' f`. -/
theorem seminormFromBounded_of_mul_is_mul (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) {x : R}
(hx : ∀ y : R, f (x * y) = f x * f y) (y : R) :
seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y :=
by
rw [seminormFromBounded_of_mul_apply f_nonneg f_mul hx]
simp only [seminormFromBounded', mul_assoc, hx, mul_div_assoc, Real.mul_iSup_of_nonneg (f_nonneg _)]
