English
Let f: R → ℝ be a nonnegative, multiplicatively bounded function. If x ∈ R satisfies f(xy) = f(x) f(y) for every y ∈ R, then the bounded seminorm associated to f takes the same value at x as f itself; i.e., seminormFromBounded' f (x) = f(x).
Русский
Пусть f: R → ℝ неотрицательная и ограниченная по умножению. Если для некоторого x ∈ R выполняется f(xy) = f(x) f(y) для каждого y ∈ R, то соответствующий ограниченный сепиномер дает на x то же значение, что и f: seminormFromBounded' f (x) = f(x).
LaTeX
$$$0 \le f \quad\land\quad (\forall x,y,\ f(xy) \le c \cdot f(x) f(y)) \land\quad (\forall y,\ f(xy)=f(x)f(y)) \Rightarrow \operatorname{seminormFromBounded'} f x = f x$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function and `x : R` is
multiplicative for `f`, then `seminormFromBounded' f x = f x`. -/
theorem seminormFromBounded_of_mul_apply (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) : seminormFromBounded' f x = f x :=
by
simp_rw [seminormFromBounded', hx, ← mul_div_assoc']
apply le_antisymm
· refine ciSup_le (fun x ↦ ?_)
by_cases hx : f x = 0
· rw [hx, div_zero, mul_zero]; exact f_nonneg _
· rw [div_self hx, mul_one]
· by_cases f_ne_zero : f ≠ 0
· conv_lhs => rw [← mul_one (f x)]
rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
have h_bdd : BddAbove (Set.range fun y ↦ f x * (f y / f y)) :=
by
use f x
rintro r ⟨y, rfl⟩
by_cases hy0 : f y = 0
· simp only [hy0, div_zero, mul_zero]; exact f_nonneg _
· simp only [div_self hy0, mul_one, le_refl]
exact le_ciSup h_bdd (1 : R)
· push_neg at f_ne_zero
simp_rw [f_ne_zero, Pi.zero_apply, zero_div, zero_mul, ciSup_const]; rfl
