four_functions_theorem_univ
theorem four_functions_theorem_univ :
∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : LinearOrderedCommSemiring β]
[inst_2 : ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [inst_3 : Fintype α],
0 ≤ f₁ →
0 ≤ f₂ →
0 ≤ f₃ →
0 ≤ f₄ →
(∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) →
((Finset.univ.sum fun a => f₁ a) * Finset.univ.sum fun a => f₂ a) ≤
(Finset.univ.sum fun a => f₃ a) * Finset.univ.sum fun a => f₄ a
The theorem `four_functions_theorem_univ` is a specific case of the Four Functions Theorem, where both sets `s` and `t` are the universal finite set `univ`. It asserts that for any two types `α` and `β`, with `α` a distributive lattice and `β` a linear ordered commutative semiring with existence of addition for less than or equal to, and given four functions `f₁`, `f₂`, `f₃`, and `f₄` from `α` to `β` (with `α` being finite), if all these functions are nonnegative and for all elements `a` and `b` in `α`, the product of `f₁(a)` and `f₂(b)` is less than or equal to the product of `f₃(a inf b)` and `f₄(a sup b)`, then the product of the sum of all values of `f₁` and `f₂` over the universal set is less than or equal to the product of the sum of all values of `f₃` and `f₄` over the universal set.
More concisely: Given two types `α` (a finite distributive lattice) and `β` (a linear ordered commutative semiring with existence of addition for less than or equal to), if four functions `f₁`, `f₂`, `f₃`, and `f₄` from `α` to `β` are nonnegative and satisfy `f₁(a) * f₂(b) ≤ f₃(a ∧ b) * f₄(a ∨ b)` for all `a, b ∈ α`, then `∑₀ i, f₁ i + f₂ i ≤ ∑₀ i, f₃ i * f₄ i`.
|
Finset.le_card_infs_mul_card_sups
theorem Finset.le_card_infs_mul_card_sups :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] (s t : Finset α),
s.card * t.card ≤ (s ⊼ t).card * (s ⊻ t).card
The theorem `Finset.le_card_infs_mul_card_sups` is referred to as Daykin's inequality. For any type `α` that forms a distributive lattice, with a decidable equality relation, and any two finite sets `s` and `t` of this type `α`, the inequality asserts that the product of the cardinalities (sizes) of `s` and `t` is less than or equal to the product of the cardinalities of the sup-inf closure of `s` and `t` and the symmetric difference of `s` and `t`. Remarkably, any lattice where this inequality holds is distributive.
More concisely: For any distributive lattice α with decidable equality, the cardinality of a finite set's sup-inf closure times the cardinality of another finite set is greater than or equal to the product of their cardinalities and the cardinality of their symmetric difference.
|
Finset.four_functions_theorem
theorem Finset.four_functions_theorem :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : LinearOrderedCommSemiring β]
[inst_2 : ExistsAddOfLE β] {f₁ f₂ f₃ f₄ : Finset α → β} (u : Finset α),
0 ≤ f₁ →
0 ≤ f₂ →
0 ≤ f₃ →
0 ≤ f₄ →
(∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
∀ {𝒜 ℬ : Finset (Finset α)},
𝒜 ⊆ u.powerset →
ℬ ⊆ u.powerset →
((𝒜.sum fun s => f₁ s) * ℬ.sum fun s => f₂ s) ≤
((𝒜 ⊼ ℬ).sum fun s => f₃ s) * (𝒜 ⊻ ℬ).sum fun s => f₄ s
The **Four Functions Theorem** on a powerset algebra is a theorem applying to two mathematical types `α` and `β`. Here, `α` is any type with decidable equality and `β` is a type that is a linear ordered commutative semiring and has an existing addition operation for less than or equal values. Given four functions `f₁`, `f₂`, `f₃`, and `f₄` that map from finite sets of `α` to `β`, and a finite set `u` of `α`, if each of these functions is non-negative and for every subset `s` and `t` of `u`, the inequality `f₁(s) * f₂(t) ≤ f₃(s ∩ t) * f₄(s ∪ t)` holds, then for any two subsets `𝒜` and `ℬ` of the power set of `u`, the inequality `((𝒜.sum fun s => f₁ s) * ℬ.sum fun s => f₂ s) ≤ ((𝒜 ⊼ ℬ).sum fun s => f₃ s) * (𝒜 ⊻ ℬ).sum fun s => f₄ s)` also holds. The operations `⊼` and `⊻` represent the sum of the intersection and the sum of the symmetric difference respectively.
More concisely: Given two types `α` with decidable equality and `β` a linear ordered commutative semiring with addition for less than or equal values, if four functions `f₁`, `f₂`, `f₃`, and `f₄` from finite sets of `α` to `β` are non-negative and satisfy `f₁(s) * f₂(t) ≤ f₃(s ∩ t) * f₄(s ∪ t)` for all subsets `s` and `t` of a finite set `u`, then `(∑(s : finset α) f₁(s)) * (∑(s : finset α) f₂(s)) ≤ (∑(s : finset α) f₃(s)) * (∑(s : finset α) f₄(s))`, where the sums are taken over the power set of `u` and `⊼` and `⊻` represent the sum of intersection and symmetric difference, respectively.
|
Finset.le_card_diffs_mul_card_diffs
theorem Finset.le_card_diffs_mul_card_diffs :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
s.card * t.card ≤ (s.diffs t).card * (t.diffs s).card
This theorem is a slight generalization of the Marica-Schönheim Inequality. It states that for any type `α` with decidable equality and a generalized boolean algebra structure, and for any finite sets `s` and `t` of `α`, the product of the cardinalities (sizes) of `s` and `t` is less than or equal to the product of the cardinalities of the set of elements in `s` but not in `t` (i.e., `s.diffs t`) and the set of elements in `t` but not in `s` (i.e., `t.diffs s`).
More concisely: For any finite sets `s` and `t` of a type `α` with decidable equality and a generalized boolean algebra structure, the product of their sizes satisfies `|s||t| ≤ |s.diffs t||t.diffs s|`.
|
Finset.card_le_card_diffs
theorem Finset.card_le_card_diffs :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s : Finset α),
s.card ≤ (s.diffs s).card
The Marica-Schönheim Inequality theorem states that for any given finite set `s` of type `α`, where `α` is a type with decidable equality and is also a Generalized Boolean Algebra, the cardinality (or size) of `s` is less than or equal to the cardinality of the set of all differences between elements of `s`. In mathematical terms, if $s$ is a finite set in a Generalized Boolean Algebra with decidable equality, then $|s| \leq |s \setminus s|$.
More concisely: In a finite Generalized Boolean Algebra with decidable equality, the cardinality of a set is bounded above by the cardinality of its differences.
|
holley
theorem holley :
∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : LinearOrderedCommSemiring β]
[inst_2 : ExistsAddOfLE β] (f g μ : α → β) [inst_3 : Fintype α],
0 ≤ μ →
0 ≤ f →
0 ≤ g →
Monotone μ →
((Finset.univ.sum fun a => f a) = Finset.univ.sum fun a => g a) →
(∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) →
(Finset.univ.sum fun a => μ a * f a) ≤ Finset.univ.sum fun a => μ a * g a
The **Holley Inequality** is a theorem in the field of lattice theory and ordered algebraic structures. It states that for any types `α` and `β`, given `α` is a distributive lattice and `β` is a linear ordered commutative semiring where addition operation is defined for less than or equal relation, and for any three functions `f`, `g` and `μ` from `α` to `β`, if `μ` is non-negative, `f` is non-negative, `g` is non-negative, `μ` is monotone, the sum of values of `f` over all elements of universal finite set of `α` equals to the sum of values of `g` over all elements of universal finite set of `α`, and for all elements `a` and `b` of `α`, the product of `f(a)` and `g(b)` is less than or equal to the product of `f` of `a` meet `b` and `g` of `a` join `b`, then the inequality holds that the sum of the product of `μ(a)` and `f(a)` over all elements `a` in the universal finite set of `α` is less than or equal to the sum of the product of `μ(a)` and `g(a)` over all elements `a` in the universal finite set of `α`.
More concisely: If `α` is a distributive lattice, `β` is a linear ordered commutative semiring with additive order, `f`, `g` are non-negative functions from `α` to `β`, `μ` is a non-negative, monotone function from `α` to `β`, and for all `a`, `b` in `α`, `f(a) ⊓ b ≤ g(a) ⊔ b` and `f(a) + g(b) = g(a) + f(b)`, then the inequality holds: `Σ(a:α) μ(a) * f(a) ≤ Σ(a:α) μ(a) * g(a)`.
|
four_functions_theorem
theorem four_functions_theorem :
∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : LinearOrderedCommSemiring β]
[inst_2 : ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [inst_3 : DecidableEq α],
0 ≤ f₁ →
0 ≤ f₂ →
0 ≤ f₃ →
0 ≤ f₄ →
(∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) →
∀ (s t : Finset α),
((s.sum fun a => f₁ a) * t.sum fun a => f₂ a) ≤
((s ⊼ t).sum fun a => f₃ a) * (s ⊻ t).sum fun a => f₄ a
The Four Functions Theorem, also known as the Ahlswede-Daykin Inequality, states that for any types `α` and `β`, where `α` has a distribution lattice structure and `β` is a linearly ordered commutative semiring with an existing addition operation for lesser equal elements. Given four functions `f₁`, `f₂`, `f₃`, and `f₄` from `α` to `β`, and assuming that `α` has decidable equality and all four functions are non-negative. If for all `a` and `b` in `α`, the product of `f₁(a)` and `f₂(b)` is less than or equal to the product of `f₃(a∧b)` and `f₄(a∨b)`, then for any two finite sets `s` and `t` of `α`, the product of the sum of `f₁` values over `s` and the sum of `f₂` values over `t` is less than or equal to the product of the sum of `f₃` values over the join of `s` and `t`, and the sum of `f₄` values over the symmetric difference of `s` and `t`.
More concisely: Given types `α` with distribution lattice structure and linearly ordered commutative semiring `β`, and functions `f₁, f₂, f₃, f₄` from `α` to `β` with decidable equality and non-negative values, if for all `a, b ∈ α`, `f₁(a) ⊓ f₂(b) ≤ f₃(a ∧ b) ⊔ f₄(a ∨ b)`, then for any finite sets `s, t ⊆ α`, `∑(i ∈ s) f₁(i) ⊓ ∑(j ∈ t) f₂(j) ≤ ∑(k ∈ s ∩ t) f₃(k) ⊔ ∑(l ∈ s ⊖ t) f₄(l)`, where `⊓` and `⊔` denote lattice meet and join, respectively.
|
fkg
theorem fkg :
∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : LinearOrderedCommSemiring β]
[inst_2 : ExistsAddOfLE β] (f g μ : α → β) [inst_3 : Fintype α],
0 ≤ μ →
0 ≤ f →
0 ≤ g →
Monotone f →
Monotone g →
(∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) →
((Finset.univ.sum fun a => μ a * f a) * Finset.univ.sum fun a => μ a * g a) ≤
(Finset.univ.sum fun a => μ a) * Finset.univ.sum fun a => μ a * (f a * g a)
The **Fortuin-Kastelyn-Ginibre Inequality** states that for any types `α` and `β` where `α` is a distributive lattice and `β` is a linear ordered commutative semiring with an existing addition of less than or equal elements, given functions `f`, `g`, and `μ` from `α` to `β` and assuming that `α` is finite, if `μ`, `f` and `g` are all non-negative, `f` and `g` are monotone, and for all `a` and `b` of type `α`, the inequality `μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)` holds, then the inequality `((∑a, μ a * f a) * ∑a, μ a * g a) ≤ ((∑a, μ a) * ∑a, μ a * (f a * g a))`, where the sum is taken over all elements of the universal finite set of type `α`, also holds. Here, `⊓` denotes the infimum (greatest lower bound) operation and `⊔` denotes the supremum (least upper bound) operation in the distributive lattice.
More concisely: Given a finite distributive lattice `α` with a linear ordered commutative semiring `β`, if functions `f`, `g`, and `μ` from `α` to `β` are non-negative, monotone, and satisfy `μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)` for all `a` and `b` in `α`, then `(∑a, μ a * f a) * (∑a, μ a * g a) ≤ (∑a, μ a) * (∑a, μ a * (f a * g a))`.
|