English
If f is nonnegative, multiplicatively bounded, and nonarchimedean, then seminormFromBounded' f is nonarchimedean.
Русский
Если f неотрицательна, ограничена умножением и неархимедова, то seminormFromBounded' f неархимедова.
LaTeX
$$$\text{IsNonarchimedean} f \Rightarrow \text{IsNonarchimedean}(\operatorname{seminormFromBounded}' f)$$$
Lean4
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded, nonarchimedean function, then
`seminormFromBounded' f` is nonarchimedean. -/
theorem seminormFromBounded_isNonarchimedean (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y)
(hna : IsNonarchimedean f) : IsNonarchimedean (seminormFromBounded' f) :=
by
refine fun x y ↦ ciSup_le (fun z ↦ ?_)
rw [le_max_iff]
suffices hf : f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z
by
rcases hf with hfx | hfy
· exact Or.inl <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z hfx
· exact Or.inr <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z hfy
by_cases hz : f z = 0
· simp only [hz, div_zero, le_refl, or_self_iff]
· rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz),
div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul, ← le_max_iff]
exact hna _ _
