# Documentation

Mathlib.Algebra.Order.Rearrangement

# Rearrangement inequality #

This file proves the rearrangement inequality and deduces the conditions for equality and strict inequality.

The rearrangement inequality tells you that for two functions f g : ι → α, the sum ∑ i, f i * g (σ i) is maximized over all σ : Perm ι when g ∘ σ monovaries with f and minimized when g ∘ σ antivaries with f.

The inequality also tells you that ∑ i, f i * g (σ i) = ∑ i, f i * g i if and only if g ∘ σ monovaries with f when g monovaries with f. The above equality also holds if and only if g ∘ σ antivaries with f when g antivaries with f.

From the above two statements, we deduce that the inequality is strict if and only if g ∘ σ does not monovary with f when g monovaries with f. Analogously, the inequality is strict if and only if g ∘ σ does not antivary with f when g antivaries with f.

## Implementation notes #

In fact, we don't need much compatibility between the addition and multiplication of α, so we can actually decouple them by replacing multiplication with scalar multiplication and making f and g land in different types. As a bonus, this makes the dual statement trivial. The multiplication versions are provided for convenience.

The case for Monotone/Antitone pairs of functions over a LinearOrder is not deduced in this file because it is easily deducible from the Monovary API.

### Scalar multiplication versions #

theorem MonovaryOn.sum_smul_comp_perm_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f i g (σ i)) Finset.sum s fun i => f i g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of g.

theorem MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i g (σ i)) = Finset.sum s fun i => f i g i) MonovaryOn f (g σ) s

Equality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f and g ∘ σ monovary together. Stated by permuting the entries of g.

theorem MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i g (σ i)) < Finset.sum s fun i => f i g i) ¬MonovaryOn f (g σ) s

Strict inequality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together. Stated by permuting the entries of g.

theorem MonovaryOn.sum_comp_perm_smul_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f (σ i) g i) Finset.sum s fun i => f i g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of f.

theorem MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f (σ i) g i) = Finset.sum s fun i => f i g i) MonovaryOn (f σ) g s

Equality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f ∘ σ and g monovary together. Stated by permuting the entries of f.

theorem MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f (σ i) g i) < Finset.sum s fun i => f i g i) ¬MonovaryOn (f σ) g s

Strict inequality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f ∘ σ and g do not monovary together. Stated by permuting the entries of f.

theorem AntivaryOn.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f i g i) Finset.sum s fun i => f i g (σ i)

Rearrangement Inequality: Pointwise scalar multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of g.

theorem AntivaryOn.sum_smul_eq_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i g (σ i)) = Finset.sum s fun i => f i g i) AntivaryOn f (g σ) s

Equality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f and g ∘ σ antivary together. Stated by permuting the entries of g.

theorem AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i g i) < Finset.sum s fun i => f i g (σ i)) ¬AntivaryOn f (g σ) s

Strict inequality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not antivary together. Stated by permuting the entries of g.

theorem AntivaryOn.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f i g i) Finset.sum s fun i => f (σ i) g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of f.

theorem AntivaryOn.sum_smul_eq_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f (σ i) g i) = Finset.sum s fun i => f i g i) AntivaryOn (f σ) g s

Equality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f ∘ σ and g antivary together. Stated by permuting the entries of f.

theorem AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {s : } {σ : } {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i g i) < Finset.sum s fun i => f (σ i) g i) ¬AntivaryOn (f σ) g s

Strict inequality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f ∘ σ and g do not antivary together. Stated by permuting the entries of f.

theorem Monovary.sum_smul_comp_perm_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
(Finset.sum Finset.univ fun i => f i g (σ i)) Finset.sum Finset.univ fun i => f i g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f i g (σ i)) = Finset.sum Finset.univ fun i => f i g i) Monovary f (g σ)

Equality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f and g ∘ σ monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f i g (σ i)) < Finset.sum Finset.univ fun i => f i g i) ¬Monovary f (g σ)

Strict inequality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_comp_perm_smul_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
(Finset.sum Finset.univ fun i => f (σ i) g i) Finset.sum Finset.univ fun i => f i g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of f.

theorem Monovary.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f (σ i) g i) = Finset.sum Finset.univ fun i => f i g i) Monovary (f σ) g

Equality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f ∘ σ and g monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_comp_perm_smul_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f (σ i) g i) < Finset.sum Finset.univ fun i => f i g i) ¬Monovary (f σ) g

Strict inequality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together. Stated by permuting the entries of g.

theorem Antivary.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
(Finset.sum Finset.univ fun i => f i g i) Finset.sum Finset.univ fun i => f i g (σ i)

Rearrangement Inequality: Pointwise scalar multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of g.

theorem Antivary.sum_smul_eq_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f i g (σ i)) = Finset.sum Finset.univ fun i => f i g i) Antivary f (g σ)

Equality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f and g ∘ σ antivary together. Stated by permuting the entries of g.

theorem Antivary.sum_smul_lt_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f i g i) < Finset.sum Finset.univ fun i => f i g (σ i)) ¬Antivary f (g σ)

Strict inequality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not antivary together. Stated by permuting the entries of g.

theorem Antivary.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
(Finset.sum Finset.univ fun i => f i g i) Finset.sum Finset.univ fun i => f (σ i) g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of f.

theorem Antivary.sum_smul_eq_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f (σ i) g i) = Finset.sum Finset.univ fun i => f i g i) Antivary (f σ) g

Equality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f ∘ σ and g antivary together. Stated by permuting the entries of f.

theorem Antivary.sum_smul_lt_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f i g i) < Finset.sum Finset.univ fun i => f (σ i) g i) ¬Antivary (f σ) g

Strict inequality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f ∘ σ and g do not antivary together. Stated by permuting the entries of f.

### Multiplication versions #

Special cases of the above when scalar multiplication is actually multiplication.

theorem MonovaryOn.sum_mul_comp_perm_le_sum_mul {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f i * g (σ i)) Finset.sum s fun i => f i * g i

Rearrangement Inequality: Pointwise multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of g.

theorem MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i * g (σ i)) = Finset.sum s fun i => f i * g i) MonovaryOn f (g σ) s

Equality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f and g ∘ σ monovary together. Stated by permuting the entries of g.

theorem MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i g (σ i)) < Finset.sum s fun i => f i g i) ¬MonovaryOn f (g σ) s

Strict inequality case of Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together. Stated by permuting the entries of g.

theorem MonovaryOn.sum_comp_perm_mul_le_sum_mul {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f (σ i) * g i) Finset.sum s fun i => f i * g i

Rearrangement Inequality: Pointwise multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of f.

theorem MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f (σ i) * g i) = Finset.sum s fun i => f i * g i) MonovaryOn (f σ) g s

Equality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f ∘ σ and g monovary together. Stated by permuting the entries of f.

theorem MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f (σ i) * g i) < Finset.sum s fun i => f i * g i) ¬MonovaryOn (f σ) g s

Strict inequality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f ∘ σ and g do not monovary together. Stated by permuting the entries of f.

theorem AntivaryOn.sum_mul_le_sum_mul_comp_perm {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f i * g i) Finset.sum s fun i => f i * g (σ i)

Rearrangement Inequality: Pointwise multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of g.

theorem AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i * g (σ i)) = Finset.sum s fun i => f i * g i) AntivaryOn f (g σ) s

Equality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f and g ∘ σ antivary together. Stated by permuting the entries of g.

theorem AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i * g i) < Finset.sum s fun i => f i * g (σ i)) ¬AntivaryOn f (g σ) s

Strict inequality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not antivary together. Stated by permuting the entries of g.

theorem AntivaryOn.sum_mul_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
(Finset.sum s fun i => f i * g i) Finset.sum s fun i => f (σ i) * g i

Rearrangement Inequality: Pointwise multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of f.

theorem AntivaryOn.sum_mul_eq_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f (σ i) * g i) = Finset.sum s fun i => f i * g i) AntivaryOn (f σ) g s

Equality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f ∘ σ and g antivary together. Stated by permuting the entries of f.

theorem AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x | σ x x} s) :
((Finset.sum s fun i => f i * g i) < Finset.sum s fun i => f (σ i) * g i) ¬AntivaryOn (f σ) g s

Strict inequality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f ∘ σ and g do not antivary together. Stated by permuting the entries of f.

theorem Monovary.sum_mul_comp_perm_le_sum_mul {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Monovary f g) :
(Finset.sum Finset.univ fun i => f i * g (σ i)) Finset.sum Finset.univ fun i => f i * g i

Rearrangement Inequality: Pointwise multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_mul_comp_perm_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f i * g (σ i)) = Finset.sum Finset.univ fun i => f i * g i) Monovary f (g σ)

Equality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f and g ∘ σ monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_mul_comp_perm_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f i * g (σ i)) < Finset.sum Finset.univ fun i => f i * g i) ¬Monovary f (g σ)

Strict inequality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_comp_perm_mul_le_sum_mul {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Monovary f g) :
(Finset.sum Finset.univ fun i => f (σ i) * g i) Finset.sum Finset.univ fun i => f i * g i

Rearrangement Inequality: Pointwise multiplication of f and g is maximized when f and g monovary together. Stated by permuting the entries of f.

theorem Monovary.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f (σ i) * g i) = Finset.sum Finset.univ fun i => f i * g i) Monovary (f σ) g

Equality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is unchanged by a permutation if and only if f ∘ σ and g monovary together. Stated by permuting the entries of g.

theorem Monovary.sum_comp_perm_mul_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Monovary f g) :
((Finset.sum Finset.univ fun i => f (σ i) * g i) < Finset.sum Finset.univ fun i => f i * g i) ¬Monovary (f σ) g

Strict inequality case of Rearrangement Inequality: Pointwise multiplication of f and g, which monovary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together. Stated by permuting the entries of g.

theorem Antivary.sum_mul_le_sum_mul_comp_perm {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
(Finset.sum Finset.univ fun i => f i * g i) Finset.sum Finset.univ fun i => f i * g (σ i)

Rearrangement Inequality: Pointwise multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of g.

theorem Antivary.sum_mul_eq_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f i * g (σ i)) = Finset.sum Finset.univ fun i => f i * g i) Antivary f (g σ)

Equality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f and g ∘ σ antivary together. Stated by permuting the entries of g.

theorem Antivary.sum_mul_lt_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f i g i) < Finset.sum Finset.univ fun i => f i g (σ i)) ¬Antivary f (g σ)

Strict inequality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f and g ∘ σ do not antivary together. Stated by permuting the entries of g.

theorem Antivary.sum_mul_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
(Finset.sum Finset.univ fun i => f i * g i) Finset.sum Finset.univ fun i => f (σ i) * g i

Rearrangement Inequality: Pointwise multiplication of f and g is minimized when f and g antivary together. Stated by permuting the entries of f.

theorem Antivary.sum_mul_eq_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f (σ i) * g i) = Finset.sum Finset.univ fun i => f i * g i) Antivary (f σ) g

Equality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is unchanged by a permutation if and only if f ∘ σ and g antivary together. Stated by permuting the entries of f.

theorem Antivary.sum_mul_lt_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
((Finset.sum Finset.univ fun i => f i * g i) < Finset.sum Finset.univ fun i => f (σ i) * g i) ¬Antivary (f σ) g

Strict inequality case of the Rearrangement Inequality: Pointwise multiplication of f and g, which antivary together, is strictly decreased by a permutation if and only if f ∘ σ and g do not antivary together. Stated by permuting the entries of f.