English
seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y.
Русский
seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y.
LaTeX
$$$\operatorname{seminormFromBounded}' f (x + y) \le \operatorname{seminormFromBounded}' f x + \operatorname{seminormFromBounded}' f y$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded, subadditive function, then
`seminormFromBounded' f` is subadditive. -/
theorem seminormFromBounded_add (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y)
(f_add : ∀ a b, f (a + b) ≤ f a + f b) (x y : R) :
seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y :=
by
refine ciSup_le (fun z ↦ ?_)
suffices hf : f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z by
exact
le_trans hf
(add_le_add (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z (le_refl _))
(le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z (le_refl _)))
by_cases hz : f z = 0
· simp only [hz, div_zero, zero_add, le_refl]
· rw [← add_div, div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul]
exact f_add _ _
