antivary_iff_mul_rearrangement — Mathlib

English

Two functions antivary f 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 ∀ 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_mul_rearrangement : Antivary f g ↔ ∀ i j, f i * g i + f j * g j ≤ f i * g j + f j * g i := by
  simp only [smul_eq_mul, antivary_iff_smul_rearrangement]

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