antivary_iff_smul_rearrangement — Mathlib

English

Two functions antivary f and g satisfy: for all i, j, f i • g i + f j • g j ≤ f i • g j + f j • g i.

Русский

Две функции antivary удовлетворяют глобально: для любых индексов i, j выполняется f(i) • g(i) + f(j) • g(j) ≤ f(i) • g(j) + f(j) • g(i).

LaTeX

$$$Antivary f g \\iff \\forall i j, f i \\bullet g i + f j \\bullet g j ≤ f i \\bullet g j + f j \\bullet g i$$$

Lean4

/-- Two functions antivary iff the rearrangement inequality holds. -/
theorem antivary_iff_smul_rearrangement : Antivary f g ↔ ∀ i j, f i • g i + f j • g j ≤ f i • g j + f j • g i :=
  monovary_toDual_right.symm.trans <| by rw [monovary_iff_smul_rearrangement]; rfl

Похожие утверждения