English
If f: R → ℝ is nonnegative and submultiplicative in the sense f(xy) ≤ f(x) f(y) with f(1) ≤ 1, then the value of seminormFromBounded' f at x equals f(x).
Русский
Пусть f: R → ℝ неотрицательная и субумножаемая по отношению к умножению (f(xy) ≤ f(x) f(y)) вместе с f(1) ≤ 1; тогда seminormFromBounded' f (x) = f(x).
LaTeX
$$$0 \le f \land (\forall y,\ f(xy) \le f(x) f(y)) \land (f(1) \le 1) \Rightarrow \operatorname{seminormFromBounded'} f x = f x$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative function and `x : R` is submultiplicative for `f`, then
`seminormFromBounded' f x = f x`. -/
theorem seminormFromBounded_of_mul_le (f_nonneg : 0 ≤ f) {x : R} (hx : ∀ y : R, f (x * y) ≤ f x * f y)
(h_one : f 1 ≤ 1) : seminormFromBounded' f x = f x :=
by
simp_rw [seminormFromBounded']
apply le_antisymm
· refine ciSup_le (fun y ↦ ?_)
by_cases hy : f y = 0
· rw [hy, div_zero]; exact f_nonneg _
· rw [div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy)]; exact hx _
· have h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y) :=
by
use f x
rintro r ⟨y, rfl⟩
by_cases hy0 : f y = 0
· simp only [hy0, div_zero]
exact f_nonneg _
· rw [← mul_one (f x), ← div_self hy0, ← mul_div_assoc, div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy0),
mul_div_assoc, div_self hy0, mul_one]
exact hx y
convert le_ciSup h_bdd (1 : R)
by_cases h0 : f x = 0
· rw [mul_one, h0, zero_div]
· have heq : f 1 = 1 := by
apply h_one.antisymm
specialize hx 1
rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx
exact hx
rw [heq, mul_one, div_one]
