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.

TODO

Add equality cases for when the permute function is injective. This comes from the following fact: If Monovary f g, Injective g and σ is a permutation, then Monovary f (g ∘ σ) ↔ σ = 1.

Scalar multiplication versions

Weak rearrangement inequality

theorem MonovaryOn.sum_smul_comp_perm_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i

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

theorem AntivaryOn.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f i • g (σ i)

Rearrangement Inequality: Pointwise scalar multiplication of f and g is minimized when f and g antivary together on s. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i

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

theorem AntivaryOn.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f (σ i) • g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is minimized when f and g antivary together on s. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f i • g (σ i) ≤ ∑ 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 Antivary.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i • g i ≤ ∑ 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 Monovary.sum_comp_perm_smul_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f (σ i) • g i ≤ ∑ 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 Antivary.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i • g i ≤ ∑ 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.

Equality case of the rearrangement inequality

theorem MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s

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

theorem AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ AntivaryOn f (g ∘ ⇑σ) ↑s

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

theorem MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s

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

theorem AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ AntivaryOn (f ∘ ⇑σ) g ↑s

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

theorem Monovary.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f i • g (σ i) = ∑ i : ι, f i • g i ↔ Monovary f (g ∘ ⇑σ)

Equality case of the 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_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Monovary (f ∘ ⇑σ) g

Equality case of the 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 Antivary.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i • g (σ i) = ∑ 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_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f (σ i) • g i = ∑ 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.

Strict rearrangement inequality

theorem MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s

Strict inequality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together on s, is strictly decreased by a permutation if and only if f and g ∘ σ do not monovary together on s. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g i < ∑ i ∈ s, 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 on s, is strictly decreased by a permutation if and only if f and g ∘ σ do not antivary together on s. Stated by permuting the entries of g.

theorem MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s

Strict inequality case of the Rearrangement Inequality: Pointwise scalar multiplication of f and g, which monovary together on s, is strictly decreased by a permutation if and only if f ∘ σ and g do not monovary together on s. 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g i < ∑ i ∈ s, 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 on s, is strictly decreased by a permutation if and only if f ∘ σ and g do not antivary together on s. Stated by permuting the entries of f.

theorem Monovary.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f i • g (σ i) < ∑ i : ι, f i • g i ↔ ¬Monovary f (g ∘ ⇑σ)

Strict inequality case of the 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_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f (σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ⇑σ) g

Strict inequality case of the 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_lt_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i • g i < ∑ 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_lt_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i • g i < ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g (σ i) ≤ ∑ i ∈ s, f i * g i

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

theorem MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g (σ i) = ∑ i ∈ s, f i * g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s

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

theorem MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s

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

theorem MonovaryOn.sum_comp_perm_mul_le_sum_mul {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) * g i ≤ ∑ i ∈ s, f i * g i

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

theorem MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s

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

theorem MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : MonovaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) * g i < ∑ i ∈ s, f i * g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s

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

theorem AntivaryOn.sum_mul_le_sum_mul_comp_perm {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f i * g (σ i)

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

theorem AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g (σ i) = ∑ i ∈ s, f i * g i ↔ AntivaryOn f (g ∘ ⇑σ) ↑s

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

theorem AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g i < ∑ i ∈ s, f i * g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s

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

theorem AntivaryOn.sum_mul_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f (σ i) * g i

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

theorem AntivaryOn.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ AntivaryOn (f ∘ ⇑σ) g ↑s

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

theorem AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) (hσ : {x : ι | σ x ≠ x} ⊆ ↑s) : ∑ i ∈ s, f i * g i < ∑ i ∈ s, f (σ i) * g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s

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

theorem Monovary.sum_mul_comp_perm_le_sum_mul {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f i * g (σ i) ≤ ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f i * g (σ i) = ∑ i : ι, f i * g i ↔ Monovary f (g ∘ ⇑σ)

Equality case of the 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f i * g (σ i) < ∑ i : ι, f i * g i ↔ ¬Monovary f (g ∘ ⇑σ)

Strict inequality case of the 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f (σ i) * g i ≤ ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f (σ i) * g i = ∑ i : ι, f i * g i ↔ Monovary (f ∘ ⇑σ) g

Equality case of the 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Monovary f g) : ∑ i : ι, f (σ i) * g i < ∑ i : ι, f i * g i ↔ ¬Monovary (f ∘ ⇑σ) g

Strict inequality case of the 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i * g i ≤ ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i * g (σ i) = ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i • g i < ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i * g i ≤ ∑ 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_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f (σ i) * g i = ∑ 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} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {σ : Equiv.Perm ι} {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ∑ i : ι, f i * g i < ∑ 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.