English
Let f1 ≤ f2 be finitely supported functions ι →₀ α, and h : ι → α → β monotone in the second argument on the union of their supports, with h i 0 = 0 on that union. Then f1.sum h ≤ f2.sum h.
Русский
Пусть f1 ≤ f2 для функций с конечной опорой ι →₀ α, и h:ι→α→β монотонна по второму аргументу на объединении опор, а также выполнено h i 0 = 0 на этом объединении. Тогда f1.sum h ≤ f2.sum h.
LaTeX
$$$f_1 \le f_2 \Rightarrow f_1.\mathrm{sum}(h) \le f_2.\mathrm{sum}(h)$, при предположениях "Monotone" и h i 0 = 0$$
Lean4
theorem sum_le_sum_index [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β} (hf : f₁ ≤ f₂)
(hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)) (hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) :
f₁.sum h ≤ f₂.sum h := by
classical
rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀, sum_of_support_subset _ Finset.subset_union_right _ hh₀]
exact Finset.sum_le_sum fun i hi ↦ hh _ hi <| hf _
