mathlib3 documentation

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 #

source
theorem monovary_on.sum_smul_comp_perm_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f 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.

source
theorem monovary_on.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f 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 g.

source
theorem monovary_on.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f 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 g.

source
theorem monovary_on.sum_comp_perm_smul_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f 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.

source
theorem monovary_on.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f 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.

source
theorem monovary_on.sum_comp_perm_smul_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : monovary_on f 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.

source
theorem antivary_on.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f 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.

source
theorem antivary_on.sum_smul_eq_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f 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 g.

source
theorem antivary_on.sum_smul_lt_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f 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 g.

source
theorem antivary_on.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f 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.

source
theorem antivary_on.sum_smul_eq_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f 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.

source
theorem antivary_on.sum_smul_lt_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {s : finset ι} {σ : equiv.perm ι} {f : ι → α} {g : ι → β} (hfg : antivary_on f 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.

source
theorem monovary.sum_smul_comp_perm_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_smul_comp_perm_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_smul_comp_perm_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_comp_perm_smul_le_sum_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_comp_perm_smul_eq_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_comp_perm_smul_lt_sum_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : monovary f 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.

source
theorem antivary.sum_smul_le_sum_smul_comp_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f 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.

source
theorem antivary.sum_smul_eq_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f 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 g.

source
theorem antivary.sum_smul_lt_sum_smul_comp_perm_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f 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 g.

source
theorem antivary.sum_smul_le_sum_comp_perm_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f 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.

source
theorem antivary.sum_smul_eq_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f 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.

source
theorem antivary.sum_smul_lt_sum_comp_perm_smul_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : equiv.perm ι} {f : ι → α} {g : ι → β} [fintype ι] (hfg : antivary f 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.

source
theorem monovary_on.sum_mul_comp_perm_le_sum_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f 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.

source
theorem monovary_on.sum_mul_comp_perm_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f 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 g.

source
theorem monovary_on.sum_mul_comp_perm_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f 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 g.

source
theorem monovary_on.sum_comp_perm_mul_le_sum_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f 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.

source
theorem monovary_on.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f 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.

source
theorem monovary_on.sum_comp_perm_mul_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f 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.

source
theorem antivary_on.sum_mul_le_sum_mul_comp_perm {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : antivary_on f 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.

source
theorem antivary_on.sum_mul_eq_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : antivary_on f 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 g.

source
theorem antivary_on.sum_mul_lt_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : antivary_on f 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 g.

source
theorem antivary_on.sum_mul_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : antivary_on f 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.

source
theorem antivary_on.sum_mul_eq_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : antivary_on f 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.

source
theorem antivary_on.sum_mul_lt_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : antivary_on f 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.

source
theorem monovary.sum_mul_comp_perm_le_sum_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_mul_comp_perm_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_mul_comp_perm_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_comp_perm_mul_le_sum_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_comp_perm_mul_eq_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : monovary f 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.

source
theorem monovary.sum_comp_perm_mul_lt_sum_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : monovary f 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.

source
theorem antivary.sum_mul_le_sum_mul_comp_perm {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : antivary f 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.

source
theorem antivary.sum_mul_eq_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : antivary f 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 g.

source
theorem antivary.sum_mul_lt_sum_mul_comp_perm_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : antivary f 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 g.

source
theorem antivary.sum_mul_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : antivary f 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.

source
theorem antivary.sum_mul_eq_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : antivary f 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.

source
theorem antivary.sum_mul_lt_sum_comp_perm_mul_iff {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : equiv.perm ι} {f g : ι → α} [fintype ι] (hfg : antivary f 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.