Antivary.card_mul_sum_le_sum_mul_sum
theorem Antivary.card_mul_sum_le_sum_mul_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} [inst_1 : Fintype ι],
Antivary f g →
(↑(Fintype.card ι) * Finset.univ.sum fun i => f i * g i) ≤
(Finset.univ.sum fun i => f i) * Finset.univ.sum fun i => g i
**Chebyshev's Sum Inequality Theorem**: Given a set of type `ι` of finite size, and two functions `f` and `g` mapping from `ι` to a linearly ordered ring `α`, if `f` and `g` antivary (i.e., when `g` increases, `f` decreases), then the product of the size of the set and the sum of the pairwise products of `f` and `g` over the entire set is less than or equal to the product of the sum of `f` values over the set and the sum of `g` values over the set.
More concisely: For a set of finite size ι and functions f, g from ι to a linearly ordered ring α that antivary, the product of the set size and the sum of their pairwise products is less than or equal to the product of the sums of f and g values.
|
AntivaryOn.card_smul_sum_le_sum_smul_sum
theorem AntivaryOn.card_smul_sum_le_sum_smul_sum :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {f : ι → α} {g : ι → β},
AntivaryOn f g ↑s → (s.card • s.sum fun i => f i • g i) ≤ (s.sum fun i => f i) • s.sum fun i => g i
**Chebyshev's Sum Inequality**: Given a finite set `s` and two functions `f` and `g` that antivary on `s` (for instance, one is increasing and the other is decreasing), the scalar multiplication of the sum of their products is less than or equal to the product of the sums of `f` and `g`, each multiplied by the size of the set `s`. This means that the inequality `(size of s * sum(f(i) * g(i))) ≤ (sum(f(i)) * sum(g(i)))` holds for all `i` in the set `s`.
More concisely: For any finite set $S$, and functions $f$ and $g$ that antivary on $S$, the product of the sums of $f$ and $g$ is greater than or equal to the sum of the products of $f$ and $g$ for all elements in $S$, i.e., $\sum_{i \in S} f(i)g(i) \leq (\sum_{i \in S} f(i))(\sum_{i \in S} g(i))$.
|
AntivaryOn.card_mul_sum_le_sum_mul_sum
theorem AntivaryOn.card_mul_sum_le_sum_mul_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {f g : ι → α},
AntivaryOn f g ↑s → (↑s.card * s.sum fun i => f i * g i) ≤ (s.sum fun i => f i) * s.sum fun i => g i
**Chebyshev's Sum Inequality**: Given a finite set `s` of elements of some type `ι`, and two functions `f` and `g` from `ι` to a linearly ordered ring `α`, if `f` and `g` antivary on `s` (in other words, whenever `g(i)` is less than `g(j)` for any two elements `i` and `j` in `s`, then `f(j)` is less than or equal to `f(i)`), then the product of the sum of the results of `f` and `g` over `s` is greater than or equal to the size of `s` times the sum of the product of the results of `f` and `g` over `s`. In mathematical terms, if `f` and `g` antivary on `s`, then `(size of s) * ∑(f(i)*g(i)) ≤ ∑f(i) * ∑g(i)` for all `i` in `s`.
More concisely: If `f` and `g` are functions from a finite set `s` to a linearly ordered ring, with `f` and `g` antivarying on `s`, then the product of the sums of `f` and `g` over `s` satisfies `(size of s) * ∑(f(i)*g(i)) ≤ ∑f(i) * ∑g(i)`.
|
sq_sum_le_card_mul_sum_sq
theorem sq_sum_le_card_mul_sum_sq :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {f : ι → α},
(s.sum fun i => f i) ^ 2 ≤ ↑s.card * s.sum fun i => f i ^ 2
This theorem is a special case of either Chebyshev's Sum Inequality or the Cauchy-Schwarz Inequality. It states that for any finite set `s` and any function `f` from the elements of `s` to a linearly ordered ring `α`, the square of the sum of the function values across the set `s` is less than or equal to the size of the set `s` times the sum of the squares of the function values.
More concisely: For any finite set `s` and function `f` from its elements to a linearly ordered ring `α`, the sum of the squares of `f` values is less than or equal to the size of `s` times the square of the sum of the `f` values. (This is the square version of the Cauchy-Schwarz Inequality or Chebyshev's Sum Inequality.)
|
Antivary.card_smul_sum_le_sum_smul_sum
theorem Antivary.card_smul_sum_le_sum_smul_sum :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Antivary f g →
(Fintype.card ι • Finset.univ.sum fun i => f i • g i) ≤
(Finset.univ.sum fun i => f i) • Finset.univ.sum fun i => g i
**Chebyshev's Sum Inequality**: Given two functions `f` and `g` that antivary (i.e., one function is increasing while the other function is decreasing), the scalar product of the sum of their inputs is less than or equal to the product of their individual sums, scaled by the size of the input set. This is defined over a finite input set `ι`, where `f` maps `ι` to a type `α` in a linear ordered ring, and `g` maps `ι` to a type `β` in a linear ordered additive commutative group. Furthermore, `α` and `β` are modules, which ensure the scalar multiplication operation in the inequality.
More concisely: For functions `f : ι → α` and `g : ι → β` that antivary over a finite set `ι` with `α` a linear ordered ring and `β` a linear ordered additive commutative group, where `α` and `β` are modules, we have: ∑ i in ι (|f i| * |g i|) ≤ (∑ i in ι |f i|) * (∑ i in ι |g i|).
|
MonovaryOn.sum_mul_sum_le_card_mul_sum
theorem MonovaryOn.sum_mul_sum_le_card_mul_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {s : Finset ι} {f g : ι → α},
MonovaryOn f g ↑s → ((s.sum fun i => f i) * s.sum fun i => g i) ≤ ↑s.card * s.sum fun i => f i * g i
**Chebyshev's Sum Inequality** states that for any two functions `f` and `g` that monovary together (i.e., they are either both increasing or both decreasing), given a finite set `s`, the product of the sums of `f` and `g` over `s` is less than or equal to the size of `s` multiplied by the sum of the product of `f` and `g` over `s`. In mathematical notation, if `f` and `g` are either both increasing or both decreasing, then for any finite set `s`, we have $\left(\sum_{i \in s} f(i)\right) \cdot \left(\sum_{i \in s} g(i)\right) \leq |s| \cdot \sum_{i \in s} f(i)g(i)$.
More concisely: For two monovarying functions `f` and `g` over a finite set `s`, the product of their sums obeys the inequality $|s| \cdot \sum_{i \in s} f(i)g(i) \geq \left(\sum_{i \in s} f(i)\right) \cdot \left(\sum_{i \in s} g(i)\right)$.
|
Monovary.sum_mul_sum_le_card_mul_sum
theorem Monovary.sum_mul_sum_le_card_mul_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} [inst_1 : Fintype ι],
Monovary f g →
((Finset.univ.sum fun i => f i) * Finset.univ.sum fun i => g i) ≤
↑(Fintype.card ι) * Finset.univ.sum fun i => f i * g i
**Chebyshev's Sum Inequality Theorem**: This theorem states that for any finite set, represented by the type `ι` with a linear ordered ring structure `α`, if two functions `f` and `g` monovary together (that is, they are either both monotone or both antitone), then the product of the sums of `f` and `g` over all elements of the set is less than or equal to the size of the set times the sum of the product of `f` and `g` over all elements of the set. In mathematical notation: $\left(\sum_i f(i)\right)\left(\sum_i g(i)\right) \leq |ι| \sum_i f(i)g(i)$, where the sum is taken over all elements in the set `ι` and $|ι|$ is the cardinality of the set `ι`.
More concisely: For a finite set `ι` with a linear ordered ring structure `α`, if functions `f` and `g` are monotone or antitone together, then $\left(\sum\_{i \in ι} f(i)\right)\left(\sum\_{i \in ι} g(i)\right) \leq |ι| \sum\_{i \in ι} f(i)g(i)$.
|
MonovaryOn.sum_smul_sum_le_card_smul_sum
theorem MonovaryOn.sum_smul_sum_le_card_smul_sum :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {s : Finset ι} {f : ι → α} {g : ι → β},
MonovaryOn f g ↑s → ((s.sum fun i => f i) • s.sum fun i => g i) ≤ s.card • s.sum fun i => f i • g i
**Chebyshev's Sum Inequality**: This theorem states that for any set `s` and functions `f` and `g` that monovary together (that is, both are either monotone or antitone), the scalar multiplication of the sum of `f` values by the sum of `g` values is less than or equal to the size of the set `s` times the sum of scalar multiplications of `f` and `g` for each element in the set. In mathematical notation, if `f` and `g` monovary on `s`, then the inequality $(\sum_{i \in s} f(i)) \cdot (\sum_{i \in s} g(i)) \leq |s| \cdot (\sum_{i \in s} f(i) \cdot g(i))$ holds.
More concisely: For sets \(s\), monovarying functions \(f\) and \(g\): \(\sum\_{i \in s} f(i) \cdot g(i) \geq \dfrac{1}{|s|} (\sum\_{i \in s} f(i)) (\sum\_{i \in s} g(i))\). (Note that this is the opposite inequality to the one stated in the given Lean theorem, but it is a common way to state Chebyshev's Sum Inequality in mathematics literature.)
|
Monovary.sum_smul_sum_le_card_smul_sum
theorem Monovary.sum_smul_sum_le_card_smul_sum :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} [inst_4 : Fintype ι],
Monovary f g →
((Finset.univ.sum fun i => f i) • Finset.univ.sum fun i => g i) ≤
Fintype.card ι • Finset.univ.sum fun i => f i • g i
**Chebyshev's Sum Inequality**: Given a type `ι` with a finite number of elements, two functions `f` and `g` from `ι` to ordered rings `α` and `β`, respectively, if `f` monovaries with `g` (meaning that when `g(i) < g(j)`, we have `f(i) ≤ f(j)`), then the scalar product of the sum of `f(i)` over all `i` and the sum of `g(i)` over all `i` is less than or equal to the number of elements in `ι` times the sum of the scalar product of `f(i)` and `g(i)` over all `i`. This theorem is an implementation of Chebyshev's Sum Inequality, which states that under these conditions, the sum-product of the sums of two sequences is less than or equal to the size of the set times the sum of the sum-products of the sequences.
More concisely: Given a finite set `ι` and functions `f : ι → ℝ` and `g : ι → ℝ` with `f` monotone with respect to `g`, the sum of their products satisfies the inequality $\sum\_{i \in ι} f(i)g(i) \leq |\ι| \cdot \sum\_{i \in ι} f(i)$.
|