antivaryOn_iff_mul_rearrangement — Mathlib

English

Antivary f g implies that for all i, j one has f i • g i + f j • g j ≤ f i • g j + f j • g i.

Русский

Антивариация f и g означает, что для любых 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 antivaryOn_iff_mul_rearrangement :
    AntivaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i := by
  simp only [smul_eq_mul, antivaryOn_iff_smul_rearrangement]

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