Antivary.sum_smul_le_sum_smul_comp_perm
theorem Antivary.sum_smul_le_sum_smul_comp_perm :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g → (Finset.univ.sum fun i => f i • g i) ≤ Finset.univ.sum fun i => f i • g (σ i)
**Rearrangement Inequality**: This theorem states that for a given pointwise scalar multiplication of two functions `f` and `g`, its sum (over a universal finite set) is minimized when `f` and `g` are antivarying, i.e., when `f` decreases as `g` increases, and vice versa. This is expressed by rearranging (or permuting) the entries of `g` using a bijection `σ` from the set to itself. Specifically, the sum of `f i • g i` over the universal finite set is less than or equal to the sum of `f i • g (σ i)` over the same set, given that `f` and `g` antivary.
More concisely: Given functions `f` and `g` with pointwise product `h = f * g`, and a bijection `σ`, if `f` and `g` are antivariable (i.e., `f(x)` decreases as `g(x)` increases, and vice versa) for all x, then the sum `Σ i in I (h i)` is less than or equal to `Σ i in I (h (σ i))`.
|
AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff
theorem AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f i * g i) < s.sum fun i => f (σ i) * g i) ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s)
This theorem is known as the "Strict inequality case of the Rearrangement Inequality." It states that for any type `ι`, any linearly ordered ring `α`, any finite set `s` of type `ι`, any permutation `σ` of `ι`, and any two functions `f` and `g` from `ι` to `α`, if `f` and `g` antivary on the set `s` and the set of elements for which `σ` is not the identity is a subset of `s`, then the sum of pointwise multiplication of `f` and `g` over `s` is less than the sum of pointwise multiplication of `f` composed with `σ` and `g` over `s` if and only if `f` composed with `σ` and `g` do not antivary on the set `s`. Here, two functions antivary on a set if increasing one function decreases the other function for all elements in the set.
More concisely: For any linearly ordered ring `α`, finite set `s` of type `ι`, permutation `σ` of `ι`, and functions `f` and `g` from `ι` to `α`, if `f` and `g` antivary on `s` and the set of elements where `σ` is not the identity is a subset of `s`, then the sum of `f i * g i` over `s` is strictly less than the sum of `(f ∘ σ) i * g i` over `s` if and only if `f ∘ σ` and `g` do not antivary on `s`.
|
Antivary.sum_smul_eq_sum_smul_comp_perm_iff
theorem Antivary.sum_smul_eq_sum_smul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f i • g (σ i)) = Finset.univ.sum fun i => f i • g i) ↔ Antivary f (g ∘ ⇑σ))
This theorem, known as the "Equality case of the Rearrangement Inequality", asserts that for any types `ι`, `α` and `β` with `α` being a linear ordered ring and `β` being a linear ordered additive commutative group with a module structure over `α` and an ordering on its scalar multiplication, a function `f` from `ι` to `α`, a function `g` from `ι` to `β`, and a permutation `σ` of `ι`, if `f` and `g` behave in an antivarying manner (meaning the value of `g` decreases when the corresponding value of `f` increases), then the sum of each entry of `f` scaled by the corresponding permuted entry of `g` equals the sum of each entry of `f` scaled by the corresponding entry of `g` if and only if `f` and `g` composed with the permutation `σ` behave in an antivarying manner. The sum is taken over the whole `Finset.univ` which represents all elements of the finite type `ι`.
More concisely: Given functions `f: ι → α` and `g: ι → β` from a finite type `ι` to a linear ordered ring `α` and a linear ordered additive commutative group `β` with a module structure over `α`, if `f` and `g` are antivarying and `σ` is a permutation of `ι`, then the following are equal:
∑ i in ι, f i * g i = ∑ i in ι, f i * g (σ i) if and only if `f` and `g` ∘ `σ` are antivarying.
|
AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff
theorem AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f i * g (σ i)) = s.sum fun i => f i * g i) ↔ AntivaryOn f (g ∘ ⇑σ) ↑s)
The theorem, known as the Equality case of the Rearrangement Inequality, states that for any given types `ι` and `α` where `α` is a linearly ordered ring, a finite set `s` of type `ι`, a permutation `σ` of `ι`, and two functions `f` and `g` from `ι` to `α`, if `f` and `g` are antivarying on the set `s` and the set of elements where `σ` doesn't fix its input is a subset of `s`, then the sum of the product of `f` and `g` after permutation is equal to the sum of the product of `f` and `g` if and only if `f` and the function composed of `g` and `σ` are antivarying on `s`.
Here, "antivarying" means that if the value of `g` at `i` is less than the value of `g` at `j`, then the value of `f` at `j` is less than or equal to the value of `f` at `i`. The theorem essentially relates the conditions under which rearranging the terms in a summation doesn't change the sum, by linking it to the properties of the functions involved in the multiplication.
More concisely: Given types `ι` and `α` where `α` is a linearly ordered ring, a finite set `s` of type `ι`, a permutation `σ` of `ι`, and functions `f` and `g` from `ι` to `α` that are antivarying on `s` with `σ(I) ∉ s` for all `I ∈ ι`, the sum of the product of `f` and `g` after permutation equals the sum of the product of `f` and the composition of `g` and `σ` if and only if `f` and the composition of `g` and `σ` are antivarying on `s`.
|
MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff
theorem MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f (σ i) * g i) = s.sum fun i => f i * g i) ↔ MonovaryOn (f ∘ ⇑σ) g ↑s)
This theorem, referred to as the "Equality case of Rearrangement Inequality", states the following: Given two functions `f` and `g` that monovary together (meaning that if `g(i)` is less than `g(j)` then `f(i)` is less than or equal to `f(j)` for all `i, j` in a given set `s`), the pointwise multiplication of `f` and `g` remains the same if you permute the entries of `f` if and only if the composition of `f` with a permutation `σ` and `g` also monovary together. The set of all `x` where `σ(x)` is not equal to `x` should be a subset of `s`. This theorem is stated by permuting the entries of `f`.
More concisely: Given functions `f` and `g` that monovary on a set `s`, the pointwise product `f ⊤ g` is permutation invariant if and only if the composition `f ∘ σ` monovaries with `g` for some permutation `σ` on `s`, where the domain of `σ` is a subset of `s` and `σ(x) ≠ x` for all `x` in its domain.
|
Monovary.sum_comp_perm_mul_eq_sum_mul_iff
theorem Monovary.sum_comp_perm_mul_eq_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f (σ i) * g i) = Finset.univ.sum fun i => f i * g i) ↔ Monovary (f ∘ ⇑σ) g)
**Equality case of the Rearrangement Inequality**: This theorem states that for any given types ι and α, where α is a LinearOrderedRing, a permutation σ on ι, and two functions `f` and `g` from ι to α; if `f` and `g` monovary together (meaning that if `g i < g j`, then `f i ≤ f j`), then the sum of the pointwise product of `f (σ i)` and `g i` over all elements in ι is equal to the sum of the pointwise product of `f i` and `g i` over all elements in ι if and only if the function `f` composed with σ and `g` monovary together. This is essentially a way of stating that the pointwise multiplication of `f` and `g`, which monovary together, is invariant under a permutation.
More concisely: Given types ι, a LinearOrderedRing α, a permutation σ on ι, and functions `f` and `g` from ι to α that monovary together, the sum of the pointwise products `f (σ i) * g i` equals the sum of `f i * g i` if and only if `f` composed with σ and `g` also monovary together.
|
AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff
theorem AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f i * g i) < s.sum fun i => f i * g (σ i)) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s)
This theorem is known as the strict inequality case of the Rearrangement Inequality. Given a linear ordered ring $\alpha$ and two functions $f, g : \iota \to \alpha$ defined over a finite set $s$, and a permutation $\sigma$ of $\iota$, the theorem states that if $f$ and $g$ antivary on $s$ (i.e., the order of values of $f$ is exactly opposite to the order of values of $g$), then the sum of pointwise multiplication of $f$ and $g$ is strictly less than the sum of pointwise multiplication of $f$ and $g$ permuted by $\sigma$, if and only if $f$ and the composition of $g$ and $\sigma$ do not antivary on $s$. The theorem is stated with the restriction that $\sigma$ only permutes elements within $s$.
More concisely: Given a finite set $s$ in a linear ordered ring, functions $f, g : s \to \alpha$ that antivary, and a permutation $\sigma$ of $s$ preserving its elements, the theorem states that $f \cdot g <_\alpha (f \circ \sigma) \cdot g$ if and only if $f$ and $g \circ \sigma$ do not antivary on $s$.
|
Monovary.sum_comp_perm_smul_eq_sum_smul_iff
theorem Monovary.sum_comp_perm_smul_eq_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f (σ i) • g i) = Finset.univ.sum fun i => f i • g i) ↔ Monovary (f ∘ ⇑σ) g)
The "Equality case of Rearrangement Inequality" theorem states that for a given scalar multiplication of two functions, `f` and `g`, which monovary together (meaning that if `g(i) < g(j)` it implies `f(i) ≤ f(j)`), the pointwise scalar multiplication result remains the same even after a permutation `σ` is performed on `f` if and only if the composed function `f ∘ σ` and `g` also monovary together. The theorem also implies that the permutation is made on the entries of `g`. This theorem is valid in the context of a linearly ordered ring `α`, a linearly ordered additive commutative group `β`, where `β` is a module over `α` and the scalar multiplication is ordered. Moreover, the domain of definition `ι` is assumed to be finite. The theorem is stated in terms of sums over the universal finite set of type `Finset ι`.
More concisely: Given functions `f` and `g` over a finite domain `ι` in a linearly ordered ring `α`, where `f` and `g` monovary together, their pointwise scalar multiplication results are equal before and after permuting the domain indices `σ(i)` if and only if the permuted functions `f ∘ σ` and `g` also monovary together.
|
MonovaryOn.sum_mul_comp_perm_le_sum_mul
theorem MonovaryOn.sum_mul_comp_perm_le_sum_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f i * g (σ i)) ≤ s.sum fun i => f i * g i
The **Rearrangement Inequality** theorem states that, for a set `s` of indices of type `ι` and two functions `f` and `g` mapping `ι` to a linearly ordered ring `α`, if `f` and `g` are monovariant on the set `s` (that is, for all `i, j` in `s`, if `g(i) < g(j)`, then `f(i) ≤ f(j)`), and a permutation `σ` of `ι` such that all the elements where `σ` differs from the identity are in `s`, then the sum of the products of `f(i)` and `g(σ(i))` over `s` is less than or equal to the sum of the products of `f(i)` and `g(i)` over `s`. In other words, the pointwise multiplication of `f` and `g` is maximized when `f` and `g` increase together, as stated by permuting the entries of `g`.
More concisely: For a set `s` of indices, two monovariant functions `f` and `g` mapping `ι` to a linearly ordered ring `α`, and a permutation `σ` of `ι` with non-identity differences only in `s`, the sum of the products `f(i) * g(σ(i))` over `s` is less than or equal to the sum of the products `f(i) * g(i)` over `s`.
|
MonovaryOn.sum_smul_comp_perm_le_sum_smul
theorem MonovaryOn.sum_smul_comp_perm_le_sum_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f i • g (σ i)) ≤ s.sum fun i => f i • g i
**Rearrangement Inequality Statement**: For any finite set `s` of indices and any two functions `f : ι → α` and `g : ι → β` that monovary together on `s` (meaning if `g i < g j` then `f i ≤ f j` for all `i, j ∈ s`), and any permutation `σ` of the indices such that any index `x` for which `σ x ≠ x` is in `s`, the sum over `s` of `f i • g (σ i)` (the pointwise scalar multiplication of `f` and `σ`-permuted `g`) is less than or equal to the sum over `s` of `f i • g i` (the pointwise scalar multiplication of `f` and `g`). Here, `•` denotes scalar multiplication in the context of a linearly ordered ring `α` and a linearly ordered additive commutative group `β` where `α` acts on `β`. This statement essentially suggests that rearranging the terms of `g` to match the order of `f` maximizes the sum of the pointwise scalar multiplication.
More concisely: For any finite set `s`, functions `f : ι → α` and `g : ι → β` that monovary together on `s`, and permutation `σ` of `s`, the pointwise scalar multiplication of `f` and `σ`-permuted `g` summed over `s` is less than or equal to the pointwise scalar multiplication of `f` and `g` summed over `s`.
|
Monovary.sum_smul_comp_perm_le_sum_smul
theorem Monovary.sum_smul_comp_perm_le_sum_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g → (Finset.univ.sum fun i => f i • g (σ i)) ≤ Finset.univ.sum fun i => f i • g i
This theorem, known as the "Rearrangement Inequality", states that for any types `ι`, `α`, `β`, with `α` being a linearly ordered ring, `β` being a linearly ordered additive commutative group, and also being a module over `α`, and `ι` being a finite type. If `f` is a function from `ι` to `α`, `g` is a function from `ι` to `β`, and `σ` is a bijection (permutation) from `ι` to `ι`, such that `f` and `g` monovary together (i.e., if `g i < g j` then `f i ≤ f j`), then the sum (over all elements in the universal set of `ι`) of the scalar multiplication of `f i` and `g (σ i)` is less than or equal to the sum of the scalar multiplication of `f i` and `g i`. This means that rearranging (or permuting) the entries of `g` does not increase the sum of the pointwise scalar multiplication of `f` and `g`.
More concisely: For a finite type `ι`, function `f: ι → α` from `ι` to a linearly ordered ring `α`, function `g: ι → β` from `ι` to a linearly ordered additive commutative group `β` that is a module over `α`, and a bijection `σ: ι → ι`, if `f` and `g` monovary together, then the sum of the scalar multiplications of `f i` and `g (σ i)` for all `i` in `ι` is less than or equal to the sum of the scalar multiplications of `f i` and `g i`.
|
MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff
theorem MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f (σ i) • g i) = s.sum fun i => f i • g i) ↔ MonovaryOn (f ∘ ⇑σ) g ↑s)
The **Equality case of Rearrangement Inequality** theorem states that for a given finite set of indices `s`, scalar multiplication functions `f` and `g` which monovary together, a permutation `σ`, and under certain conditions, the sum of pointwise scalar multiplication of `f` and `g` remains unchanged due to the permutation if and only if the composition of `f` and `σ` and `g` monovary together. The conditions are that the set of indices where the permutation differs from the identity is a subset of `s`, and the scalars are from a linearly ordered ring and the vectors are from a linearly ordered additive commutative group, where scalar multiplication is ordered. In essence, the theorem says that rearranging the entries of `f` does not change the sum if and only if the rearranged `f` and `g` still monovary together.
More concisely: For a finite set of indices `s`, scalar multiplication functions `f` and `g` monovarying together, a permutation `σ`, and scalars from a linearly ordered ring and vectors from a linearly ordered additive commutative group with ordered scalar multiplication, the sum of pointwise scalar multiplications of `f` and `g` is unchanged under `σ` if and only if `f ∘ σ` and `g` monovary together, provided that the indices where `σ` differs from the identity are in `s`.
|
Monovary.sum_mul_comp_perm_le_sum_mul
theorem Monovary.sum_mul_comp_perm_le_sum_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g → (Finset.univ.sum fun i => f i * g (σ i)) ≤ Finset.univ.sum fun i => f i * g i
The **Rearrangement Inequality Theorem** states that for any given types `ι` and `α`, where `α` is a linear ordered ring and `ι` is a finite type, and given functions `f` and `g` from `ι` to `α`, as well as a permutation `σ` of type `ι`, if the functions `f` and `g` satisfy a property called monovariation - meaning that whenever `g i` is less than `g j`, `f i` is less than or equal to `f j` - then the sum of the pointwise multiplication of `f` and `g` under the permutation `σ` over all elements of the type `ι` is less than or equal to the sum of the pointwise multiplication of `f` and `g` over all elements of the type `ι`. In other words, the maximum value of the pointwise multiplication of `f` and `g` is attained when `f` and `g` monovary together.
More concisely: For finite types `ι`, given functions `f: ι → α` and `g: ι → α` from a linear ordered ring `α` with monovariation property (`g i ≤ g j ⇒ f i ≤ f j`), the sum of their pointwise products under any permutation `σ` of `ι` is less than or equal to the sum of their pointwise products over the original order.
|
Antivary.sum_smul_le_sum_comp_perm_smul
theorem Antivary.sum_smul_le_sum_comp_perm_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g → (Finset.univ.sum fun i => f i • g i) ≤ Finset.univ.sum fun i => f (σ i) • g i
**Rearrangement Inequality**: For any type `ι` with a fintype instance, scalars `α` in a linearly ordered ring, and `β` in a linearly ordered additive commutative group, if we have a function `f : ι → α`, a function `g : ι → β`, and a permutation `σ : Equiv.Perm ι`, such that `f` and `g` antivary (meaning if `g i < g j` then `f j ≤ f i`), then the total sum of `f i` multiplied by `g i` across all `i` in the universe finite set is less than or equal to the total sum of `f (σ i)` multiplied by `g i` (i.e., with `f` permuted by `σ`) across all `i` in the universe finite set. This theorem states that the pointwise scalar multiplication of `f` and `g` is minimized when `f` and `g` antivary together.
More concisely: Given a finite type `ι`, scalars `α` in a linearly ordered ring, and `β` in a linearly ordered additive commutative group, if `f : ι → α`, `g : ι → β` are functions with `g` antivarying `f`, and `σ : Equiv.Perm ι` is a permutation, then the sum of `f i * g i` over all `i` is less than or equal to the sum of `f (σ i) * g i`.
|
MonovaryOn.sum_comp_perm_smul_le_sum_smul
theorem MonovaryOn.sum_comp_perm_smul_le_sum_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f (σ i) • g i) ≤ s.sum fun i => f i • g i
**Rearrangement Inequality**: Given a finite set `s` and two functions `f: ι → α` and `g: ι → β` (where `ι` is any type, `α` is a type forming a linear ordered ring, and `β` a type forming a linear ordered commutative additive group), this theorem states that if `f` and `g` monovary together on the set `s` (i.e., an increase in `g` implies a non-decrease in `f`) and we have a permutation `σ` that only permutes elements within `s`, then the sum of the product of `f` and `g` under this permutation (`f (σ i) • g i` summed over all `i` in `s`) is less than or equal to the sum of the product of `f` and `g` without permutation (`f i • g i` summed over all `i` in `s`). This essentially means that the pointwise scalar multiplication of `f` and `g` is maximized when `f` and `g` monovary together, and rearranging the elements of `f` can only decrease this sum.
More concisely: Given a finite set with functions `f:` `ι` `→` `α` (where `α` is a linearly ordered ring) and `g:` `ι` `→` `β` (where `β` is a linearly ordered commutative additive group), if `f` and `g` are monotonic together on `ι`, then the sum of their pointwise products under any permutation of their domain is less than or equal to the sum without permutation.
|
Monovary.sum_comp_perm_smul_le_sum_smul
theorem Monovary.sum_comp_perm_smul_le_sum_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g → (Finset.univ.sum fun i => f (σ i) • g i) ≤ Finset.univ.sum fun i => f i • g i
**Rearrangement Inequality Theorem**:
For any given types, `ι` (the index type), `α` (a linear order ring), and `β` (a linear ordered additive commutative group with a module structure over `α` and ordered scalar multiplication), along with a permutation `σ : Equiv.Perm ι`, and two functions `f : ι → α` and `g : ι → β` (where `ι` has a finite type), if `f` and `g` are monovariant, i.e., whenever `g i < g j`, we have `f i ≤ f j`, then the sum over all elements of the finite set `univ` of `f (σ i) • g i` (the reordered scalar multiplication of `f` and `g` according to the permutation `σ`) is less than or equal to the sum over all elements of the set `univ` of `f i • g i` (the pointwise scalar multiplication of `f` and `g`). That is, the pointwise scalar multiplication of `f` and `g` is maximized when `f` and `g` monovary together.
More concisely: For any finite index type `ι`, linear order ring `α`, linearly ordered additive commutative group `β` with a module structure over `α`, permutation `σ : Equiv.Perm ι`, and monovariant functions `f : ι → α` and `g : ι → β`, the sum of the reordered scalar multiplications `f (σ i) • g i` is less than or equal to the sum of the pointwise scalar multiplications `f i • g i`.
|
Antivary.sum_mul_eq_sum_comp_perm_mul_iff
theorem Antivary.sum_mul_eq_sum_comp_perm_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f (σ i) * g i) = Finset.univ.sum fun i => f i * g i) ↔ Antivary (f ∘ ⇑σ) g)
The theorem, named "Equality case of the Rearrangement Inequality", pertains to functions `f` and `g` that antivary together. In the context of this theorem, antivarying means that if `g i` is less than `g j`, then `f j` is less than or equal to `f i`. When `f` and `g` have this property, the sum of the pointwise multiplications `f (σ i) * g i` over all `i` in a universal finite set (implied by `Fintype ι`) is equal to the sum of the pointwise multiplications `f i * g i` over all `i` in the same set if and only if the function `f ∘ σ` (the composition of `f` and a permutation `σ`) also antivaries with `g`. This theorem relates the antivarying property to the invariance of the pointwise multiplication summation under a permutation of the arguments to `f`.
More concisely: Given functions `f` and `g` that antivary together over a finite set `ι`, the sum of their pointwise products is invariant under permutations `σ` of `ι` if and only if the function `f ∘ σ` also antivaries with `g`.
|
AntivaryOn.sum_smul_le_sum_comp_perm_smul
theorem AntivaryOn.sum_smul_le_sum_comp_perm_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f i • g i) ≤ s.sum fun i => f (σ i) • g i
This theorem is a statement of the **Rearrangement Inequality** in the context of summing scalar multiplications of two functions over a finite set. More specifically, for any finite set `s`, permutation `σ`, and functions `f : ι → α` and `g : ι → β` that antivary on `s` (i.e., if `g i < g j` then `f j ≤ f i` for all `i` and `j` in `s`), the sum of the scalar products `f i • g i` over `s` is less than or equal to the sum of the scalar products `f (σ i) • g i` over `s`. This is under the condition that any `x` for which `σ x ≠ x` is within `s`. Here, `•` denotes the scalar multiplication operation, `α` is a linear ordered ring, `β` is a linear ordered additive commutative group, and `α` is a module over `β`. The inequality is preserved when the values of `f` are permuted according to `σ`.
More concisely: For any finite set `s`, permutation `σ`, and functions `f : ι → α` and `g : ι → β` that antivary on `s`, the sum of the scalar products `f i • g i` over `s` is less than or equal to the sum of the scalar products `f (σ i) • g i` over `s`, provided any `x` for which `σ x neq x` is in `s`.
|
Antivary.sum_mul_lt_sum_comp_perm_mul_iff
theorem Antivary.sum_mul_lt_sum_comp_perm_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f i * g i) < Finset.univ.sum fun i => f (σ i) * g i) ↔ ¬Antivary (f ∘ ⇑σ) g)
The theorem, known as the "Strict inequality case of the Rearrangement Inequality", applies to the scenario where there exists a set of type 'ι', a linear ordered ring of type 'α', a bijection 'σ' from 'ι' to itself, and two functions 'f' and 'g' that map from 'ι' to 'α'. Suppose 'f' and 'g' are antivariant, meaning that if 'g' increases, 'f' decreases. The theorem states that the overall sum of the pointwise multiplication of 'f' and 'g' over the entire set is strictly less than the sum of the pointwise multiplication of the permuted 'f' (i.e., 'f' after applying the bijection 'σ') and 'g' if and only if the permuted 'f' and 'g' are not antivariant. In other words, permuting the entries of 'f' decreases the sum of the pointwise multiplications if and only if the permuted 'f' and 'g' do not show an inverse relationship.
More concisely: Given a set 'ι', a linear ordered ring 'α', a bijection 'σ' on 'ι', and antivariant functions 'f' and 'g' from 'ι' to 'α', the sum of the pointwise products of 'f' and 'g' is strictly less than the sum of the pointwise products of the permuted 'f' and 'g' if and only if the permuted 'f' and 'g' are not antivariant.
|
MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff
theorem MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f i * g (σ i)) = s.sum fun i => f i * g i) ↔ MonovaryOn f (g ∘ ⇑σ) ↑s)
The **Equality case of Rearrangement Inequality** theorem states that, for any given set `s` of a type `ι`, a permutation `σ` of type `ι`, and functions `f` and `g` from `ι` to a linearly ordered ring `α`, if `f` and `g` monovary over `s` (meaning that if `g i` is less than `g j` then `f i` is less than or equal to `f j` for all `i, j` in `s`), then the sum of the pointwise multiplication of `f` and `σ`-permuted `g` over `s` equals the sum of the pointwise multiplication of `f` and `g` over `s` if and only if `f` and `g` composed with `σ` monovary over `s`. Here, the set of points where `σ` does not equal identity must be a subset of `s`.
More concisely: For any set `s`, permutation `σ`, functions `f` and `g` from `s` to a linearly ordered ring `α`, if `f` and `g` monovary over `s` and the set where `σ` is non-identity is a subset of `s`, then the sum of the pointwise products of `f` and `σ`-permuted `g` equals the sum of the pointwise products of `f` and `g` if and only if `f` and `g` composed with `σ` monovary over `s`.
|
Monovary.sum_smul_comp_perm_lt_sum_smul_iff
theorem Monovary.sum_smul_comp_perm_lt_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f i • g (σ i)) < Finset.univ.sum fun i => f i • g i) ↔ ¬Monovary f (g ∘ ⇑σ))
The theorem named "Strict inequality case of Rearrangement Inequality" states that for any types `ι`, `α`, `β`, and any scalar multiplication `f : ι → α` and `g : ι → β` which are monovariant (i.e., `g` monotonically increases or decreases as `f` does), the sum of the scalar multiplication of `f` and `g`, after applying a permutation `σ`, is strictly less than the sum of `f` and `g` if and only if `f` and the composition of `g` and `σ` are not monovariant. The sum is taken over the universal finite set of type `ι`. The types `α` and `β` are constrained by the conditions that `α` is a linear ordered ring, `β` is a linear ordered additive commutative group, `α` acts on `β` via scalar multiplication in an order-preserving way, and `ι` is a finite type.
More concisely: For functions `f : ι -> α` and `g : ι -> β` being monovariant scalar multiplications over a finite type `ι`, where `α` is a linear ordered ring, `β` a linear ordered additive commutative group, and `α` acts on `β` order-preservingly, the permutation-induced inequality `∑ i in ι (f i + g (σ i)) < ∑ i in ι (f i + g i)` holds if and only if `f` and `g ∘ σ` are not monovariant.
|
MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff
theorem MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f i • g (σ i)) = s.sum fun i => f i • g i) ↔ MonovaryOn f (g ∘ ⇑σ) ↑s)
**Equality case of Rearrangement Inequality**: Given a set `s` of indices, a scalar-valued function `f`, and a vector-valued function `g`, if `f` and `g` are monovariant (i.e., increasing `g` implies non-decreasing `f`) on `s`, then the following holds: the total scalar product of `f` and `g` after applying a permutation `σ` is equal to the original total scalar product of `f` and `g` if and only if `f` and `g` after applying `σ` are monovariant on `s`. In this statement, the permutation `σ` only alters the entries of `g` and it is assumed that any index for which `σ` is not an identity mapping belongs to `s`.
More concisely: Given a set `s`, scalar-valued function `f`, and vector-valued function `g` on `s`, if `f` is non-decreasing and `g` is increasing, then the total scalar product of `f` and `g` is invariant under any permutation of `g`'s entries if and only if `f` and `g` after the permutation are non-decreasing.
|
Monovary.sum_smul_comp_perm_eq_sum_smul_iff
theorem Monovary.sum_smul_comp_perm_eq_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f i • g (σ i)) = Finset.univ.sum fun i => f i • g i) ↔ Monovary f (g ∘ ⇑σ))
The **Equality case of Rearrangement Inequality** theorem states that for any scalar multiplication of two functions `f` and `g`, which monovary together, the result remains the same even after applying a permutation if and only if `f` and the composition of `g` and permutation `σ` also monovary together. This is stated in terms of permuting the entries of `g`. In other words, for any linear ordered ring `α`, linear ordered add commutative group `β`, a module structure over `α` and `β`, an ordered scalar multiplication structure, and any finite type `ι`, if `f` and `g` are functions from `ι` to `α` and `β` respectively and monovary together, then the sum over all elements of `f(i) * g(σ(i))` is equal to the sum over all elements of `f(i) * g(i)` if and only if `f` and `g ∘ σ` monovary together.
More concisely: For functions $f:\kappa \to A$ and $g:\kappa \to B$ over linear ordered rings $A$ and $B$, monovarying with respect to a common order, the equality $\sum\_{i \in \kappa} f(i) \cdot g(\sigma(i)) = \sum\_{i \in \kappa} f(i) \cdot g(i)$ holds if and only if $f$ and the composition $g \circ \sigma$ monovary together.
|
Antivary.sum_smul_eq_sum_comp_perm_smul_iff
theorem Antivary.sum_smul_eq_sum_comp_perm_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f (σ i) • g i) = Finset.univ.sum fun i => f i • g i) ↔ Antivary (f ∘ ⇑σ) g)
The theorem, named as "Equality case of the Rearrangement Inequality", states that for any types ι, α, and β where α is a linearly ordered ring, β is a linearly ordered additive commutative group, and a module over α, and we have an ordered scalar multiplication of α and β, given a permutation σ of type ι, and functions f from ι to α and g from ι to β, and a finite set of type ι, if the function f antivaries with the function g, then the sum of the values obtained by applying f to each element of the permuted set and then scaling the corresponding value of g by the result is equal to the sum of the values obtained by applying f to each element of the set and then scaling the corresponding value of g by the result if and only if the function obtained by composing f with the permutation σ antivaries with the function g. In simpler terms, it means that changing the order of elements in the function f following a permutation σ doesn't affect the sum obtained by multiplying the results of functions f and g if and only if the permuted function f and g are in an antivarying relationship.
More concisely: For any linearly ordered ring α, linearly ordered additive commutative group and α-module β, and functions f : ι -> α and g : ι -> β, if f anticommutes with g and f is permuted by σ : ι -> ι, then the sum ∑ i in ι (f i * g σ i) equals the sum ∑ i in ι (f i * g i).
|
MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff
theorem MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f i • g (σ i)) < s.sum fun i => f i • g i) ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s)
The theorem "Strict inequality case of Rearrangement Inequality" states that, given a type of elements `ι`, a linear-ordered ring `α`, a linear-ordered additive commutative group `β`, a module over `α` and `β`, an ordered semigroup over `α` and `β`, a finite set `s` of elements of type `ι`, a permutation `σ` on `ι`, and two functions `f : ι → α` and `g : ι → β`. If `f` and `g` monovary on the set `s` and the elements `x` for which `σ` is not the identity are contained in `s`, then the sum of the pointwise scalar multiplication of `f` and `g` after applying the permutation `σ` is strictly less than the sum of the pointwise scalar multiplication of `f` and `g` if and only if `f` and `g` composed with `σ` do not monovary on the set `s`. This theorem is a precise formulation of a specific case of the rearrangement inequality, which states that the product of sequences, when sorted in opposite directions, results in the smallest possible product.
More concisely: Given functions `f : ι -> α` and `g : ι -> β` from a finite set `s` of a linear-ordered ring `α`, a linear-ordered additive commutative group `β`, and an ordered semigroup over `α` and `β`, if `f` and `g` monovary on `s` and are not monovary after applying a non-identity permutation `σ` on `s`, then the sum of the pointwise scalar multiplication of `f` and `g` after applying `σ` is strictly less than their sum without permutation.
|
Monovary.sum_mul_comp_perm_eq_sum_mul_iff
theorem Monovary.sum_mul_comp_perm_eq_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f i * g (σ i)) = Finset.univ.sum fun i => f i * g i) ↔ Monovary f (g ∘ ⇑σ))
This theorem is known as the "Equality case of Rearrangement Inequality". It states that for a certain index set `ι`, a specific type `α` that is a linear ordered ring, a specific permutation `σ` of the index set, and functions `f` and `g` that map from index set to `α`, given that `f` and `g` monovary, the pointwise multiplication of `f` and `g` remains the same when permuted by `σ` if and only if `f` and the composition function of `g` and `σ` monovary.
More specifically, the sum of the products of `f` and `g` applied to the permuted indices (from the universe of all indices) is equal to the sum of the products of `f` and `g` applied to the indices directly, if and only if `f` and the composition of `g` and the permutation monovary together. This theorem is proved by permuting the entries of `g`.
More concisely: For a linear ordered ring `α`, functions `f` and `g` from an index set `ι`, which are both monovarying, satisfy the pointwise product `∏ i, f i * g (σ i) = ∏ i, f i * g i` if and only if the composition of `g` and the permutation `σ` is also monovarying.
|
Antivary.sum_smul_lt_sum_comp_perm_smul_iff
theorem Antivary.sum_smul_lt_sum_comp_perm_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f i • g i) < Finset.univ.sum fun i => f (σ i) • g i) ↔ ¬Antivary (f ∘ ⇑σ) g)
This theorem, known as the Strict Inequality Case of the Rearrangement Inequality, states that for any types `ι`, `α`, and `β`, where `α` is a linear ordered ring and `β` is a linear ordered add comm group with `α` as its scalar and `β` as its module, and for any bijection `σ` from `ι` to itself, and any two functions `f : ι → α` and `g : ι → β`, if `f` and `g` antivary - meaning, if `g i < g j`, then `f j ≤ f i` - then the pointwise scalar multiplication of `f` and `g` is strictly decreased by the permutation `σ` if and only if the composition of `f` with `σ` and `g` do not antivary. In other words, the sum of scalar multiplications `f i • g i` over all `i` in `ι` is strictly less than the sum of scalar multiplications `f (σ i) • g i` over all `i` in `ι` if and only if `f ∘ σ` and `g` do not antivary.
More concisely: For functions $f:\ilon \to \alpha$ and $g:\ilon \to \beta$ between a linear ordered ring $\alpha$, a linear ordered abelian group $\beta$ with $\alpha$ as scalar and $\beta$ as module, and a bijection $\sigma:\ilon \to \ilon$: if $f$ and $g$ antivary and $f \circ \sigma$ and $g$ do not, then the sum of scalar multiplications $\sum\_{i \in \ilon} f(i) \cdot g(i) < \sum\_{i \in \ilon} f(\sigma(i)) \cdot g(i)$.
|
Antivary.sum_mul_le_sum_mul_comp_perm
theorem Antivary.sum_mul_le_sum_mul_comp_perm :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g → (Finset.univ.sum fun i => f i * g i) ≤ Finset.univ.sum fun i => f i * g (σ i)
The **Rearrangement Inequality** theorem states that for any types `ι` and `α` where `α` is a linear ordered ring and `ι` is a finite type, any permutation `σ` of the type `ι`, and any two functions `f` and `g` from `ι` to `α`, if `f` and `g` antivary (meaning `g i < g j` implies `f j ≤ f i`), then the sum of the pointwise multiplication of `f` and `g` over all elements of type `ι` is less than or equal to the sum of the pointwise multiplication of `f` and the permuted `g` over all elements of type `ι`. In other words, the total effect of `f` and `g` antivarying together minimizes the pointwise multiplication of `f` and `g`, and this is stated in terms of permuting the entries of `g`.
More concisely: For any finite type `ι`, linear ordered ring `α`, permutation `σ` of `ι`, and functions `f` and `g` from `ι` to `α` that antivary, the sum of the pointwise products of `f` and `g` over `ι` is less than or equal to the sum of the pointwise products of `f` and the permuted `g` over `ι`.
|
AntivaryOn.sum_smul_eq_sum_comp_perm_smul_iff
theorem AntivaryOn.sum_smul_eq_sum_comp_perm_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f (σ i) • g i) = s.sum fun i => f i • g i) ↔ AntivaryOn (f ∘ ⇑σ) g ↑s)
This theorem, referred to as the "Equality case of the Rearrangement Inequality", states that for a given set `s` of elements of type `ι`, a permutation `σ` of `ι`, and functions `f: ι → α` and `g : ι → β`, where `α` is a linear ordered ring and `β` is a linear ordered additive commutative group with a scalar multiplication, if `f` and `g` antivary on `s`, and all the elements `x` in the set `s` that are moved by the permutation `σ` are included in `s`, then the scalar multiplication of `f` and `g`, evaluated pointwise and summed over `s`, remains unchanged by the permutation `σ` if and only if `f ∘ σ` and `g` antivary on `s`. In other words, rearranging the entries of `f` according to the permutation `σ` does not change the sum if and only if the rearranged function `f` still antivaries with `g`.
More concisely: For functions $f:\Gamma \to \alpha$ and $g:\Gamma \to \beta$ over a set $\Gamma$ with a permutation $\sigma$, if $f$ and $g$ antivary over $\Gamma$, $s \subseteq \Gamma$ is invariant under $\sigma$, and $f \circ \sigma$ and $g$ continue to antivary over $s$, then the pointwise scalar multiplication of $f$ and $g$ over $s$ is equal to the pointwise scalar multiplication over $\sigma(s)$.
|
MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff
theorem MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f (σ i) * g i) < s.sum fun i => f i * g i) ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s)
This is the strict inequality case of the Rearrangement Inequality. It applies to a situation where you have two functions, `f` and `g`, that "monovary together" over a set `s`. In other words, when the output of `g` increases, the output of `f` also increases. We consider a permutation (rearrangement) `σ` of the inputs. The theorem states that the sum of the pointwise products of `f` and `g` over the set `s` is strictly less after applying the permutation `σ` to the inputs of `f` if and only if `f` and `g` do not monovary together after applying the permutation. It's required that the points where `σ` actually changes the input fall within the set `s`. Essentially, this theorem tells us about how rearranging the input values can affect the sum of the multiplied outputs of two functions that have this monovarying property.
More concisely: Given functions `f` and `g` that monovary together over a set `s`, if there exists a permutation `σ` of `s` such that the sum of the pointwise products of `f` and `g` over `s` strictly decreases after applying `σ`, then `f` and `g` do not monovary together after applying `σ`.
|
Monovary.sum_comp_perm_mul_lt_sum_mul_iff
theorem Monovary.sum_comp_perm_mul_lt_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f (σ i) * g i) < Finset.univ.sum fun i => f i * g i) ↔ ¬Monovary (f ∘ ⇑σ) g)
This theorem, known as the **Strict inequality case of the Rearrangement Inequality**, states that for any given types `ι` and `α` with `α` being a linear ordered ring, a permutation `σ` of type `ι`, and functions `f` and `g` from `ι` to `α`, if `f` and `g` monovary together (meaning that if the values of `g` increase, then the values of `f` do not decrease), then the sum of the products `f(σ(i)) * g(i)` over all `i` in the universal finite set `Finset.univ` is strictly less than the sum of the products `f(i) * g(i)` over all `i` in `Finset.univ` if and only if `f` composed with `σ` and `g` do not monovary together. The statement implies that rearranging the entries of `g` via the permutation `σ` disrupts the monovary relationship between `f` and `g`, leading to a strict decrease in the sum of their pointwise multiplication.
More concisely: For any linear ordered ring type `α`, functions `f` and `g` from a finite index set `ι` to `α`, and permutation `σ` of `ι`, if `f` monovaries with `g` (meaning `g(σ(i)) ≤ g(i)` for all `i` implies `f(σ(i)) ≤ f(i)` for all `i`) and `f ∘ σ` and `g` do not monovary together, then the sum of `f(i) * g(i)` over all `i` is strictly less than the sum of `f(σ(i)) * g(i)` over all `i`.
|
AntivaryOn.sum_smul_eq_sum_smul_comp_perm_iff
theorem AntivaryOn.sum_smul_eq_sum_smul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f i • g (σ i)) = s.sum fun i => f i • g i) ↔ AntivaryOn f (g ∘ ⇑σ) ↑s)
This theorem, often known as the "Equality case of the Rearrangement Inequality," states that for any types `ι`, `α`, `β` with `α` being a linearly ordered ring, `β` being a linearly ordered additive commutative group, and `ι` being permuted by a bijection `σ`, along with functions `f : ι → α` and `g : ι → β` that antivary on a finite set `s`, the pointwise scalar multiplication of `f` and `g` remains unchanged by this permutation if and only if `f` and `g ∘ σ` antivary together. This result is significant in ensuring the property of antivariance under permutations.
In other words, sum of scalar multiplication of `f i` and `g (σ i)` over all `i` in `s`, is equal to sum of scalar multiplication of `f i` and `g i` over all `i` in `s` if and only if `f` and the function obtained by composing `g` with `σ` antivary on `s`. Moreover, this theorem requires that the set of `i` for which `σ i` is not equal to `i` is a subset of `s`.
More concisely: For functions `f : ι → α` and `g : ι → β` over linearly ordered rings `α` and additive commutative groups `β`, antivarying on a finite set `s`, pointwise scalar multiplication `∑ i in s (f i * g i)` equals `∑ i in s (f i * g (σ i))` if and only if `f` and `g ∘ σ` antivary on `s`, where `σ` is a bijection on `ι` and `s` is the set of indices where `σ` is not the identity.
|
MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff
theorem MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f i • g (σ i)) < s.sum fun i => f i • g i) ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s)
The strict inequality case of the Rearrangement Inequality theorem states that for any type `ι`, any linear ordered ring `α`, any finite set `s` of type `ι`, any permutation `σ` of type `ι`, and any two functions `f` and `g` from `ι` to `α`, if `f` and `g` monotonically vary together on the set `s`, and the elements that the permutation `σ` changes are contained within `s`, then the sum of the pointwise scalar multiplication of `f` and `g` after applying the permutation `σ` is less than the sum of the pointwise scalar multiplication of `f` and `g` if and only if `f` and the composition of `g` and the permutation `σ` do not monotonically vary together on the set `s`. In simpler terms, rearranging the entries of `g` using the permutation `σ` can decrease the sum of the pointwise scalar multiplication of `f` and `g` only if `f` and this rearranged `g` stop varying together monotonically.
More concisely: For any linear ordered ring `α`, finite set `s` of type `ι`, permutation `σ` of type `ι`, functions `f` and `g` from `ι` to `α` that monotonically vary together on `s`, and if `σ(s)` is contained within `s`, then the sum of the pointwise scalar multiplication of `f` and `g` after applying `σ` is less than the sum before if and only if `f` and `g ∘ σ` are not monotonically increasing or decreasing on `s`.
|
Monovary.sum_mul_comp_perm_lt_sum_mul_iff
theorem Monovary.sum_mul_comp_perm_lt_sum_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f i * g (σ i)) < Finset.univ.sum fun i => f i * g i) ↔ ¬Monovary f (g ∘ ⇑σ))
This theorem, known as the "Strict inequality case of Rearrangement Inequality," applies to a specific situation where a pair of functions `f` and `g` monovary together. The theorem states that for any set `ι`, any linearly ordered ring `α`, any bijection `σ` from `ι` to itself, and any pair of functions `f` and `g` mapping from `ι` to `α` (given finite `ι`), if `f` and `g` monovary together, then the sum of the pointwise multiplication of `f` and `g` permuted by `σ` is strictly less than the unpermuted sum if and only if `f` and `g` composed with `σ` do not monovary together.
In other words, a permutation can strictly decrease the sum of pointwise multiplication of two monovarying functions `f` and `g` if and only if the permutation disrupts the monovarying property between `f` and the permuted `g`.
More concisely: For any set ι, linearly ordered ring α, bijection σ on ι, and functions f, g: ι → α that monovary together, the sum of their pointwise products ∑ i in ι (f i * g σ(i)) is strictly less than the unpermuted sum ∑ i in ι (f i * g i) if and only if f and g do not monovary when composed with σ.
|
Antivary.sum_mul_le_sum_comp_perm_mul
theorem Antivary.sum_mul_le_sum_comp_perm_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g → (Finset.univ.sum fun i => f i * g i) ≤ Finset.univ.sum fun i => f (σ i) * g i
The **Rearrangement Inequality** theorem asserts that for any given types `ι` and `α` , where `α` forms a linearly ordered ring, a permutation `σ` of type `ι`, and functions `f` and `g` from `ι` to `α` and `ι` is of finite type, if `f` antivaries with `g` (meaning that if `g i` is less than `g j`, then `f j` is less than or equal to `f i`), then the sum of the pointwise multiplication of `f` and `g` over all elements of a universal finite set of type `ι` is less than or equal to the sum of the multiplication of `f` and `g`, where `f` is evaluated at the permuted inputs. This implies that the minimum of the pointwise multiplication of `f` and `g` is achieved when `f` and `g` are arranged in a manner that they antivary.
More concisely: For any finite type `ι` with a linearly ordered ring `α`, functions `f` and `g` from `ι` to `α` with `f` antivariant with `g`, the sum of their pointwise product over a universal finite set of `ι` is less than or equal to the sum of their product evaluated at the permuted inputs.
|
MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff
theorem MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f (σ i) • g i) < s.sum fun i => f i • g i) ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s)
This theorem, known as the **Strict inequality case of Rearrangement Inequality**, states that for any ordered ring `α`, ordered additive commutative group `β`, and a module with a scalar multiplication that is order-preserving over `β` and `α`, let `f` be a function from a finite set `s` to `α` and `g` be a function from `s` to `β`. If `f` and `g` monovary together on `s`, then pointwise scalar multiplication of `f` and `g` is strictly decreased by a permutation `σ` if and only if the function `f` composed with the permutation `σ` and the function `g` do not monovary together on `s`. Here, monovarying together refers to a property where if `g i` is less than `g j` then `f i` is less than or equal to `f j` for all `i, j` in `s`. The theorem is stated by permuting the entries of `f`.
More concisely: For functions `f: s -> α` and `g: s -> β` from a finite set `s` to an ordered ring `α` and an ordered additive commutative group `β`, with scalar multiplication order-preserving over `β` and `α`, if `f` and `g` monovary together and permuting the entries of `f` results in a stricter inequality, then `f` and `g` do not monovary together.
|
Monovary.sum_comp_perm_smul_lt_sum_smul_iff
theorem Monovary.sum_comp_perm_smul_lt_sum_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g →
(((Finset.univ.sum fun i => f (σ i) • g i) < Finset.univ.sum fun i => f i • g i) ↔ ¬Monovary (f ∘ ⇑σ) g)
This theorem, known as the "Strict inequality case of Rearrangement Inequality", states that for any permutation `σ`, and any two functions `f` and `g` that monovary together (i.e., if `g i < g j` then `f i ≤ f j`), the pointwise scalar multiplication of `f` and `g` is strictly decreased by the permutation `σ` if and only if `f ∘ σ` and `g` do not monovary together. In this context, scalar multiplication is performed over a linearly ordered ring and a linearly ordered additive commutative group, with the results belonging to a module over the ring where scalar multiplication is also ordered. The summation is taken over all elements of a finite set of the same type as the domain of `f` and `g`.
More concisely: For any permutation σ and functions f and g that monotonically increase together, the pointwise product of f and g is strictly decreased by σ if and only if f ∘ σ and g are not monotonic together.
|
Antivary.sum_mul_eq_sum_mul_comp_perm_iff
theorem Antivary.sum_mul_eq_sum_mul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f i * g (σ i)) = Finset.univ.sum fun i => f i * g i) ↔ Antivary f (g ∘ ⇑σ))
The theorem, known as the "Equality case of the Rearrangement Inequality", establishes a relationship between a permutation and antivariance of two functions. Specifically, it states that the pointwise multiplication of two functions `f` and `g`, which antivary together, remains the same under a permutation if and only if `f` and the composition of `g` and the permutation (expressed as `g ∘ σ`) also antivary. This theorem is formalized considering all the elements of the set (`Finset.univ.sum`), expressing the multiplication of `f` and `g` before (`f i * g i`) and after (`f i * g (σ i)`) the permutation.
More concisely: Given functions `f` and `g` that antivary together, their pointwise product is equal to the pointwise product of `f` and the composition of `g` with any permutation `σ` if and only if `f` and `g ∘ σ` also antivary.
|
AntivaryOn.sum_mul_eq_sum_comp_perm_mul_iff
theorem AntivaryOn.sum_mul_eq_sum_comp_perm_mul_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s → (((s.sum fun i => f (σ i) * g i) = s.sum fun i => f i * g i) ↔ AntivaryOn (f ∘ ⇑σ) g ↑s)
The Rearrangement Inequality Equality Case Theorem states that for any ordered ring, finite set, and permutation, if a function `f` antivaries with a function `g` (that is, if `g(i) < g(j)` implies `f(j) <= f(i)` for all `i` and `j` in the set), and the set of elements where the permutation alters the value is a subset of the original set, then the pointwise multiplication of `f` and `g` remains the same under permutation if and only if `f` composed with the permutation antivaries with `g`. In other words, permuting the entries of `f` does not change the sum of the pointwise multiplication of `f` and `g` if and only if the permuted `f` and `g` also have an antivarying relationship.
More concisely: For an ordered ring, finite set, and permutation, if a function `f` antivaries with `g`, and the set of elements where the permutation changes the value of `f` is a subset of the original set, then the pointwise product of `f` and `g` is unchanged under permutation if and only if `f` composited with the permutation antivaries with `g`.
|
AntivaryOn.sum_mul_le_sum_comp_perm_mul
theorem AntivaryOn.sum_mul_le_sum_comp_perm_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f i * g i) ≤ s.sum fun i => f (σ i) * g i
The **Rearrangement Inequality** theorem states that for any finite set `s` of a certain type `ι` and any two functions `f` and `g` from `ι` to a linearly ordered ring `α`, if `f` and `g` antivary on `s` (meaning that whenever `g i` is less than `g j` for any `i` and `j` in `s`, then `f j` is less than or equal to `f i`), and if we have a permutation `σ` of `ι` such that every element `x` of `ι` where `σ x` does not equal `x` is in `s`, then the sum of the products of `f i` and `g i` over all `i` in `s` is less than or equal to the sum of the products of `f (σ i)` and `g i` over all `i` in `s`. This essentially means that the pointwise multiplication of `f` and `g` is minimized when `f` and `g` are rearranged (using the permutation `σ`) in such a way that they antivary together.
More concisely: For any finite set `s` and functions `f` and `g` from `s` to a linearly ordered ring, if `f` and `g` antivary on `s` and there exists a permutation `σ` of `s` such that `σ x != x` implies `x` is in `s`, then the sum of the products of `f i` and `g i` over `i` in `s` is less than or equal to the sum of the products of `f (σ i)` and `g i` over `i` in `s`.
|
AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff
theorem AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f i • g i) < s.sum fun i => f i • g (σ i)) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s)
The theorem, **Strict inequality case of the Rearrangement Inequality**, states that given a certain type of ordered ring `α` and an ordered additive commutative group `β` with a scalar multiplication operation, for a finite set `s` of a certain type `ι`, a bijection `σ` from `ι` to itself, and two functions `f : ι → α` and `g : ι → β`, if `f` and `g` antivary on the set `s`, then the scalar multiplication of `f` and `g`, when summed over all elements of `s`, is strictly decreased by the permutation `σ` if and only if `f` and the composition of `g` and `σ` do not antivary together. This is under the condition that the set of all `x`, where `σx ≠ x`, is a subset of `s`. Antivarying (or antivariance) here means that if the value of `g` increases at two points, then the value of `f` at these points decreases in the same order.
More concisely: Given an ordered ring `α`, an ordered additive commutative group `β` with scalar multiplication, a finite set `s` of a certain type `ι`, a bijection `σ` from `ι` to itself, functions `f : ι → α` and `g : ι → β`, and `s` containing the set of all `x` such that `σx neq x`, the scalar sum of `f` and `g` over `s` is strictly decreased by `σ` if and only if `f` and the composition `g ∘ σ` do not antivary together.
|
Antivary.sum_mul_lt_sum_mul_comp_perm_iff
theorem Antivary.sum_mul_lt_sum_mul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f i • g i) < Finset.univ.sum fun i => f i • g (σ i)) ↔ ¬Antivary f (g ∘ ⇑σ))
The theorem, named "Strict inequality case of the Rearrangement Inequality", states that for any universal finite set in a linear ordered ring, if a function `f` and another function `g` antivary (which means if `g` increases, `f` decreases), then the sum of the pointwise multiplication of `f` and `g` is strictly less than the sum of the pointwise multiplication of `f` and `g` permuted by a bijection `σ` if and only if `f` and the permutation of `g` by `σ` do not antivary. In other words, permuting the entries of `g` disrupts the antivarying relationship between `f` and `g` and increases the sum of the pointwise multiplication.
More concisely: For any function `f` and `g` in a linear ordered ring, if `g` antivaries with respect to `f` and `σ` is a bijection such that `f` does not antivary with respect to the permutation `g ∘ σ`, then the pointwise product `∑ i, f i * g i` is strictly less than `∑ i, f i * g (σ i)`.
|
AntivaryOn.sum_smul_le_sum_smul_comp_perm
theorem AntivaryOn.sum_smul_le_sum_smul_comp_perm :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f i • g i) ≤ s.sum fun i => f i • g (σ i)
The **Rearrangement Inequality** theorem states that for any set `s` and any two functions `f` and `g` from `ι` to the ordered ring `α` and the ordered additive commutative group `β` respectively, if `f` antivaries with `g` on `s` and if the permutation `σ` of `ι` only permutes elements within `s`, then the sum of the products of `f(i)` and `g(i)` over all `i` in `s` is less than or equal to the sum of the products of `f(i)` and `g(σ(i))` over all `i` in `s`. Here, `f(i) • g(i)` denotes scalar multiplication of `f(i)` and `g(i)`. This theorem states that pointwise scalar multiplication of `f` and `g` is minimized when `f` and `g` are antivarying together.
More concisely: For any set `s`, functions `f: ι -> α` and `g: ι -> β` from an ordered ring to an ordered additive commutative group respectively, and a permutation `σ` of `ι` that only permutes elements within `s`, if `f` antivaries with `g` on `s`, then the sum of the products of `f(i)` and `g(i)` over all `i` in `s` is less than or equal to the sum of the products of `f(i)` and `g(σ(i))` over all `i` in `s`.
|
Mathlib.Algebra.Order.Rearrangement._auxLemma.4
theorem Mathlib.Algebra.Order.Rearrangement._auxLemma.4 :
∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a < b) = (a ≤ b ∧ a ≠ b)
This theorem, `Mathlib.Algebra.Order.Rearrangement._auxLemma.4`, states that for all types `α` that have a partial order, given any two elements `a` and `b` of type `α`, `a < b` is equivalent to `a ≤ b` and `a ≠ b`. In other words, `a` is less than `b` if and only if `a` is less than or equal to `b` and `a` is not equal to `b`. This assertion is a common definition in the concept of ordering in algebra.
More concisely: For all types `α` with a partial order, `a < b` if and only if `a ≤ b` and `a ≠ b`.
|
Antivary.sum_smul_lt_sum_smul_comp_perm_iff
theorem Antivary.sum_smul_lt_sum_smul_comp_perm_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g →
(((Finset.univ.sum fun i => f i • g i) < Finset.univ.sum fun i => f i • g (σ i)) ↔ ¬Antivary f (g ∘ ⇑σ))
The theorem, referred to as the "Strict inequality case of the Rearrangement Inequality", states the following:
For any type `ι`, any linear ordered ring `α`, any linear ordered additive commutative group `β`, any module structure of `β` over `α`, an order-preserving scalar multiplication, a permutation `σ` of type `ι`, and functions `f : ι → α` and `g : ι → β`, given that `f` and `g` antivary together (i.e., if `g i < g j` then `f j ≤ f i`), the sum of the scalar multiplications `f i • g i` over all `i` in the universal set is strictly less than the sum of the scalar multiplications `f i • g (σ i)` over all `i` in the universal set if and only if `f` and the function obtained by composing `g` with `σ` do not antivary together.
In other words, if `f` and `g` antivary, then pointwise scalar multiplication of `f` and `g` is strictly decreased by permuting the entries of `g` with `σ` if and only if `f` and the permutation-adjusted `g` do not antivary. This basically explains a condition under which changing the order of elements in `g` impacts the relationship between `f` and `g` in terms of antivariance.
More concisely: For any order-preserving scalar multiplication, functions `f : ι → α` and `g : ι → β` over a linear ordered ring or group, if `f` and `g` antivary together and `f` does not antivary with `g ∘ σ`, then the sum of the scalar multiplications `f i • g i` is strictly less than the sum of `f i • g (σ i)` for all `i`.
|
AntivaryOn.sum_mul_le_sum_mul_comp_perm
theorem AntivaryOn.sum_mul_le_sum_mul_comp_perm :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f i * g i) ≤ s.sum fun i => f i * g (σ i)
This statement is known as the **Rearrangement Inequality**. The theorem states that for any index set `ι`, any linear ordered ring `α`, a finite subset `s` of `ι`, a permutation `σ` of `ι`, and two functions `f` and `g` from `ι` to `α`, if `f` and `g` antivary together on `s` (meaning that for all `i` and `j` in `s`, if `g i` is less than `g j`, then `f j` is less than or equal to `f i`) and the set of `x` where `σ x` is not equal to `x` is a subset of `s`, then the sum of the product of `f i` and `g i` over all `i` in `s` is less than or equal to the sum of the product of `f i` and `g (σ i)` over all `i` in `s`. Essentially, this theorem demonstrates that when `f` and `g` antivary together, the total sum of their pointwise products is minimized when the entries of `g` are rearranged by a permutation.
More concisely: Given a linear ordered ring `α`, a finite index set `ι`, a permutation `σ` of `ι`, and functions `f` and `g` from `ι` to `α` such that `s` is their common domain, `f` and `g` antivary on `s`, and the set where `σ x ≠ x` is a subset of `s`, the sum of the pointwise products of `f` and `g` over `s` is less than or equal to the sum of the pointwise products of `f` and `g` with the permuted indices.
|
AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff
theorem AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s →
{x | σ x ≠ x} ⊆ ↑s →
(((s.sum fun i => f i • g i) < s.sum fun i => f (σ i) • g i) ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s)
The **Strict inequality case of the Rearrangement Inequality** theorem states that for any finite set `s` of indices, a permutation `σ`, and functions `f : ι → α` and `g : ι → β`, where `α` is a linearly ordered ring and `β` is a linearly ordered additive commutative group with a scalar multiplication, if `f` and `g` antivary on `s` (meaning that if `g i` is less than `g j`, then `f j` is less than or equal to `f i` for all `i, j` in `s`), then the pointwise scalar multiplication of `f` and `g` is strictly less than that of `f ∘ σ` and `g` if and only if `f ∘ σ` and `g` do not antivary on `s`. The condition `{x | σ x ≠ x} ⊆ ↑s` ensures that the theorem only considers indices that are actually permuted by `σ`.
More concisely: For functions $f : I \to \alpha$ and $g : I \to \beta$ defined on a finite set $I$ with a permutation $\sigma$, if $f$ and $g$ antivary on $I$ and $\sigma(I) \cap I = \emptyset$, then $f \cdot g < (f \circ \sigma) \cdot g$ if and only if $f \circ \sigma$ and $g$ do not antivary on $I$, where $\cdot$ denotes pointwise scalar multiplication and $\circ$ denotes composition.
|
Monovary.sum_comp_perm_mul_le_sum_mul
theorem Monovary.sum_comp_perm_mul_le_sum_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {σ : Equiv.Perm ι} {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g → (Finset.univ.sum fun i => f (σ i) * g i) ≤ Finset.univ.sum fun i => f i * g i
This theorem, known as the Rearrangement Inequality, states that for any type `ι` and a linear ordered ring `α`, given a permutation `σ` of `ι` and two functions `f` and `g` from `ι` to `α`, if `f` and `g` monovary together (which means that if `g i` is less than `g j` then `f i` is less than or equal to `f j`), then the sum over all elements of `ι` of `f` applied to `σ i` times `g i` is less than or equal to the sum over all elements of `ι` of `f i` times `g i`. In simpler terms, the pointwise multiplication of `f` and `g` gives a maximum sum when `f` and `g` increase together, and rearranging the terms of `f` based on a permutation does not yield a larger sum.
More concisely: For any linear ordered ring `α` and type `ι` with a permutation `σ`, if functions `f` and `g` from `ι` to `α` monovary together, then the sum over all `i` in `ι` of `f σ i` \* `g i` is less than or equal to the sum over all `i` in `ι` of `f i` \* `g i`.
|
MonovaryOn.sum_comp_perm_mul_le_sum_mul
theorem MonovaryOn.sum_comp_perm_mul_le_sum_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (s.sum fun i => f (σ i) * g i) ≤ s.sum fun i => f i * g i
**Rearrangement Inequality Theorem**: Given a type `ι` and a linearly ordered ring `α`, for any finite set `s` of type `ι` and any two functions `f` and `g` from `ι` to `α`, if `f` and `g` monovary on the elements of `s`, and if the set of all elements `x` such that `x` is not fixed by a permutation `σ` is a subset of `s`, then the sum of the products of `f` and `g` after applying the permutation `σ` to the inputs of `f`, is less than or equal to the sum of the products of `f` and `g` without any permutation. In other words, the maximum value of pointwise multiplication of `f` and `g` is achieved when `f` and `g` monovary together.
More concisely: Given a linearly ordered ring `α`, for any finite set `s` and functions `f` and `g` from `s` to `α` that monovary on `s` and have no common fixed points under permutations, the sum of the products of `f` and `g` after applying any permutation is less than or equal to the sum without permutation.
|