English
For a subset s of the index set and functions f: I → α, g: I → β, the monotone-on subset condition MonovaryOn f g s is equivalent to the rearrangement inequality: for all i ∈ s and j ∈ s, f(i) • g(j) + f(j) • g(i) ≤ f(i) • g(i) + f(j) • g(j).
Русский
Для подмножества s индексов и функций f: I → α, g: I → β условие моно-варьированности на подмножестве MonovaryOn f g s эквивалентно перестановочному неравенству: для всех i, j ∈ s выполняется f(i) • g(j) + f(j) • g(i) ≤ f(i) • g(i) + f(j) • g(j).
LaTeX
$$$MonovaryOn f g s \\iff \\forall i \\in s, \\forall j \\in s, f i \\bullet g j + f j \\bullet g i \\le f i \\bullet g i + f j \\bullet g j$$$
Lean4
/-- Two functions monovary iff the rearrangement inequality holds. -/
theorem monovaryOn_iff_smul_rearrangement :
MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j :=
monovaryOn_iff_forall_smul_nonneg.trans <|
forall₄_congr fun i _ j _ ↦ by
simp [smul_sub, sub_smul, ← add_sub_right_comm, le_sub_iff_add_le, add_comm (f i • g i), add_comm (f i • g j)]
