mathlib documentation

algebra.order.rearrangement

Rearrangement inequality #

This file proves the rearrangement 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.

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} [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) :

∑ (i : ι) in s, f i • g (⇑σ i) ≤ ∑ (i : ι) in s, f i • g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is maximized when f and g vary 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} [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) :

∑ (i : ι) in s, f (⇑σ i) • g i ≤ ∑ (i : ι) in s, f i • g i

Rearrangement Inequality: Pointwise scalar multiplication of f and g is maximized when f and g vary 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} [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) :

∑ (i : ι) in s, f i • g i ≤ ∑ (i : ι) in s, 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_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) :

∑ (i : ι) in s, f i • g i ≤ ∑ (i : ι) in s, 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 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) :

∑ (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 vary 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} [linear_ordered_ring α] [linear_ordered_add_comm_group β] [module α β] [ordered_smul α β] {σ : 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 vary together. Stated by permuting the entries of f.

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

∑ (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_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) :

∑ (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.

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} [linear_ordered_ring α] {s : finset ι} {σ : equiv.perm ι} {f g : ι → α} (hfg : monovary_on f g ↑s) (hσ : {x : ι | ⇑σ x ≠ x} ⊆ ↑s) :

∑ (i : ι) in s, (f i) * g (⇑σ i) ≤ ∑ (i : ι) in s, (f i) * g i

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

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

∑ (i : ι) in s, (f (⇑σ i)) * g i ≤ ∑ (i : ι) in s, (f i) * g i

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

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

∑ (i : ι) in s, (f i) * g i ≤ ∑ (i : ι) in s, (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_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) :

∑ (i : ι) in s, (f i) * g i ≤ ∑ (i : ι) in s, (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 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) :

∑ (i : ι), (f i) * g (⇑σ i) ≤ ∑ (i : ι), (f i) * g i

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

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

∑ (i : ι), (f (⇑σ i)) * g i ≤ ∑ (i : ι), (f i) * g i

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

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

∑ (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_le_sum_comp_perm_mul {ι : Type u_1} {α : Type u_2} [linear_ordered_ring α] {σ : 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.