antivaryOn_iff_smul_rearrangement

English

Two functions antivary on a set s in the sense that for all i, j in s one has f i • g i + f j • g j ≤ f i • g j + f j • g i.

Русский

Две функции antivary на множестве индексов s означают, что для любых i, j ∈ s выполняется f(i) • g(i) + f(j) • g(j) ≤ f(i) • g(j) + f(j) • g(i).

LaTeX

$$$AntivaryOn f g s \\iff \\forall i \\in s, \\forall j \\in s, f i \\bullet g i + f j \\bullet g j \\le f i \\bullet g j + f j \\bullet g i$$$

Lean4

/-- Two functions antivary iff the rearrangement inequality holds. -/
theorem antivaryOn_iff_smul_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 :=
  monovaryOn_toDual_right.symm.trans <| by rw [monovaryOn_iff_smul_rearrangement]; rfl

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