# 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) :
is, f i g (σ i) is, 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) :
is, f i g (σ i) = is, f i g i MonovaryOn f (g σ) s

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 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) :
is, f i g (σ i) < is, 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, 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) :
is, f (σ i) g i is, 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) :
is, f (σ i) g i = is, f i g i MonovaryOn (f σ) g s

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 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) :
is, f (σ i) g i < is, 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, 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) :
is, f i g i is, 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_comp_perm_eq_sum_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) :
is, f i g (σ i) = is, 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.

@[deprecated AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff]
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) :
is, f i g (σ i) = is, f i g i AntivaryOn f (g σ) s

Alias of AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff.

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) :
is, f i g i < is, 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) :
is, f i g i is, 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_comp_perm_smul_eq_sum_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) :
is, f (σ i) g i = is, 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.

@[deprecated AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff]
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) :
is, f (σ i) g i = is, f i g i AntivaryOn (f σ) g s

Alias of AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff.

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) :
is, f i g i < is, 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) :
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 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) :
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_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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 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) :
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_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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 Antivary.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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.

@[deprecated Antivary.sum_smul_comp_perm_eq_sum_smul_iff]
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) :
i : ι, f i g (σ i) = i : ι, f i g i Antivary f (g σ)

Alias of Antivary.sum_smul_comp_perm_eq_sum_smul_iff.

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) :
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_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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.

theorem Antivary.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {σ : } {f : ια} {g : ιβ} [] (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.

@[deprecated Antivary.sum_comp_perm_smul_eq_sum_smul_iff]
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) :
i : ι, f (σ i) g i = i : ι, f i g i Antivary (f σ) g

Alias of Antivary.sum_comp_perm_smul_eq_sum_smul_iff.

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) :
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} {s : } {σ : } {f : ια} {g : ια} (hfg : MonovaryOn f g s) (hσ : {x : ι | σ x x} s) :
is, f i * g (σ i) is, 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) :
is, f i * g (σ i) = is, f i * g i MonovaryOn f (g σ) s

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 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) :
is, f i g (σ i) < is, 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, 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) :
is, f (σ i) * g i is, 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) :
is, f (σ i) * g i = is, f i * g i MonovaryOn (f σ) g s

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 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) :
is, f (σ i) * g i < is, f i * g i ¬MonovaryOn (f σ) g s

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 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) :
is, f i * g i is, 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) :
is, f i * g (σ i) = is, 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) :
is, f i * g i < is, 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) :
is, f i * g i is, 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_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} {s : } {σ : } {f : ια} {g : ια} (hfg : AntivaryOn f g s) (hσ : {x : ι | σ x x} s) :
is, f (σ i) * g i = is, 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.

@[deprecated AntivaryOn.sum_comp_perm_mul_eq_sum_mul_iff]
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) :
is, f (σ i) * g i = is, f i * g i AntivaryOn (f σ) g s

Alias of AntivaryOn.sum_comp_perm_mul_eq_sum_mul_iff.

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) :
is, f i * g i < is, 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) :
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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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} {σ : } {f : ια} {g : ια} [] (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.

@[deprecated Antivary.sum_comp_perm_mul_eq_sum_mul_iff]
theorem Antivary.sum_mul_eq_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} {σ : } {f : ια} {g : ια} [] (hfg : Antivary f g) :
i : ι, f (σ i) * g i = i : ι, f i * g i Antivary (f σ) g

Alias of Antivary.sum_comp_perm_mul_eq_sum_mul_iff.

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) :
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.