English
Let f be a function from an additive ordered structure to a linear-order, with base case bound at 0 and a subadditivity condition f(x+y) ≤ max(f(x), f(y)). Then for any list l, f(l.sum) ≤ foldr max 0 (map f l).
Русский
Пусть f распределяет значения по элементам и удовлетворяет f(0) ≤ 0 и f(x+y) ≤ max(f(x), f(y)). Тогда для любого списка l выполняется f суммирования элементов ≤ накопление максимума по элементам списка.
LaTeX
$$$\\forall M,N,\\ [AddZeroClass M],\\ [Zero N],\\ [LinearOrder N],\\ f:M\\to N,\\ f(0)\\le 0,\\ (\\forall x,y,\\ f(x+y) \\le \\max(f(x),f(y))) \\Rightarrow\\forall l:\\,\\text{List } M,\\ f(l.sum) \\le \\text{foldr max } 0 (\\text{map } f\, l).$$
Lean4
theorem sum_le_foldr_max [AddZeroClass M] [Zero N] [LinearOrder N] (f : M → N) (h0 : f 0 ≤ 0)
(hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : List M) : f l.sum ≤ (l.map f).foldr max 0 := by
induction l with
| nil => simpa using h0
| cons hd tl IH =>
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
exact (hadd _ _).trans (max_le_max le_rfl IH)
