English
If f ≠ 0, then seminormFromBounded' f 1 = 1.
Русский
Если f ≠ 0, то seminormFromBounded' f 1 = 1.
LaTeX
$$$\operatorname{seminormFromBounded}' f 1 = 1$$$
Lean4
/-- If `f : R → ℝ` is a nonzero, nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f 1 = 1`. -/
theorem seminormFromBounded_one (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
seminormFromBounded' f 1 = 1 := by
simp_rw [seminormFromBounded', one_mul]
apply le_antisymm
· refine ciSup_le (fun x ↦ ?_)
by_cases hx : f x = 0
· rw [hx, div_zero]; exact zero_le_one
· rw [div_self hx]
· rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
have h_bdd : BddAbove (Set.range fun y ↦ f y / f y) :=
by
use (1 : ℝ)
rintro r ⟨y, rfl⟩
by_cases hy : f y = 0
· simp only [hy, div_zero, zero_le_one]
· simp only [div_self hy, le_refl]
exact le_ciSup h_bdd (1 : R)
