# mathlib3documentation

algebra.order.rearrangement

# Rearrangement inequality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 linear_order is not deduced in this file because it is easily deducible from the monovary API.

### Scalar multiplication versions #

theorem monovary_on.sum_smul_comp_perm_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g (σ i)) s.sum (λ (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_on.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g (σ i)) = s.sum (λ (i : ι), f i g i) (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 monovary_on.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g (σ i)) < s.sum (λ (i : ι), f i g i) ¬ (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 monovary_on.sum_comp_perm_smul_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) g i) s.sum (λ (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_on.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) g i) = s.sum (λ (i : ι), f i g i) monovary_on (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 monovary_on.sum_comp_perm_smul_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) g i) < s.sum (λ (i : ι), f i g i) ¬monovary_on (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 antivary_on.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g i) s.sum (λ (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_on.sum_smul_eq_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g (σ i)) = s.sum (λ (i : ι), f i g i) (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 antivary_on.sum_smul_lt_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g i) < s.sum (λ (i : ι), f i g (σ i)) ¬ (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 antivary_on.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g i) s.sum (λ (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_on.sum_smul_eq_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) g i) = s.sum (λ (i : ι), f i g i) antivary_on (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 antivary_on.sum_smul_lt_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [ β] [ β] {s : finset ι} {σ : equiv.perm ι} {f : ι α} {g : ι β} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g i) < s.sum (λ (i : ι), f (σ i) g i) ¬antivary_on (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g (σ i)) finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g (σ i)) = finset.univ.sum (λ (i : ι), f i g i) (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g (σ i)) < finset.univ.sum (λ (i : ι), f i g i) ¬ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) g i) finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) g i) = finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) g i) < finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g i) finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g (σ i)) = finset.univ.sum (λ (i : ι), f i g i) (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g i) < finset.univ.sum (λ (i : ι), f i g (σ i)) ¬ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g i) finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) g i) = finset.univ.sum (λ (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} [ β] [ β] {σ : equiv.perm ι} {f : ι α} {g : ι β} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g i) < finset.univ.sum (λ (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 monovary_on.sum_mul_comp_perm_le_sum_mul {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g (σ i)) s.sum (λ (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_on.sum_mul_comp_perm_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g (σ i)) = s.sum (λ (i : ι), f i * g i) (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 monovary_on.sum_mul_comp_perm_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i g (σ i)) < s.sum (λ (i : ι), f i g i) ¬ (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 monovary_on.sum_comp_perm_mul_le_sum_mul {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) * g i) s.sum (λ (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_on.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) * g i) = s.sum (λ (i : ι), f i * g i) monovary_on (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 monovary_on.sum_comp_perm_mul_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) * g i) < s.sum (λ (i : ι), f i * g i) ¬monovary_on (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 antivary_on.sum_mul_le_sum_mul_comp_perm {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g i) s.sum (λ (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_on.sum_mul_eq_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g (σ i)) = s.sum (λ (i : ι), f i * g i) (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 antivary_on.sum_mul_lt_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g i) < s.sum (λ (i : ι), f i * g (σ i)) ¬ (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 antivary_on.sum_mul_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g i) s.sum (λ (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_on.sum_mul_eq_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f (σ i) * g i) = s.sum (λ (i : ι), f i * g i) antivary_on (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 antivary_on.sum_mul_lt_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {s : finset ι} {σ : equiv.perm ι} {f g : ι α} (hfg : g s) (hσ : {x : ι | σ x x} s) :
s.sum (λ (i : ι), f i * g i) < s.sum (λ (i : ι), f (σ i) * g i) ¬antivary_on (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g (σ i)) finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g (σ i)) = finset.univ.sum (λ (i : ι), f i * g i) (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g (σ i)) < finset.univ.sum (λ (i : ι), f i * g i) ¬ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) * g i) finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) * g i) = finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) * g i) < finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g i) finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g (σ i)) = finset.univ.sum (λ (i : ι), f i * g i) (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i g i) < finset.univ.sum (λ (i : ι), f i g (σ i)) ¬ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g i) finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f (σ i) * g i) = finset.univ.sum (λ (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} {σ : equiv.perm ι} {f g : ι α} [fintype ι] (hfg : g) :
finset.univ.sum (λ (i : ι), f i * g i) < finset.univ.sum (λ (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.