LeanAide GPT-4 documentation

Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

IsUpperSet.card_inter_le_finset

theorem IsUpperSet.card_inter_le_finset : โˆ€ {ฮฑ : Type u_1} [inst : DecidableEq ฮฑ] {๐’œ โ„ฌ : Finset (Finset ฮฑ)} [inst_1 : Fintype ฮฑ], IsUpperSet โ†‘๐’œ โ†’ IsLowerSet โ†‘โ„ฌ โ†’ 2 ^ Fintype.card ฮฑ * (๐’œ โˆฉ โ„ฌ).card โ‰ค ๐’œ.card * โ„ฌ.card

The **Harris-Kleitman Inequality** states that for any two finite sets ๐’œ and โ„ฌ in a larger universe set ฮฑ, where ๐’œ is an upper set and โ„ฌ is a lower set, the inequality $2^{|ฮฑ|} \times |๐’œ \cap โ„ฌ| \leq |๐’œ| \times |โ„ฌ|$ holds, where |ยท| denotes the cardinality of a set. In other words, the size of the intersection of an upper set and a lower set, when multiplied by the size of the universe set raised to the power of two, is less than or equal to the product of the sizes of the original two sets. This theorem captures a notion of anti-correlation between upper sets and lower sets in finite sets.

More concisely: For any finite upper set A and lower set B in a universe set ฮฑ, the cardinality of their intersection satisfies the inequality |A โˆฉ B| โ‰ค |A| |B| โ‹… 2^|ฮฑ|.

IsLowerSet.card_inter_le_finset

theorem IsLowerSet.card_inter_le_finset : โˆ€ {ฮฑ : Type u_1} [inst : DecidableEq ฮฑ] {๐’œ โ„ฌ : Finset (Finset ฮฑ)} [inst_1 : Fintype ฮฑ], IsLowerSet โ†‘๐’œ โ†’ IsUpperSet โ†‘โ„ฌ โ†’ 2 ^ Fintype.card ฮฑ * (๐’œ โˆฉ โ„ฌ).card โ‰ค ๐’œ.card * โ„ฌ.card

The Harris-Kleitman inequality states that the number of elements in the intersection of two sets, ๐’œ and โ„ฌ, each of which is a set of finite sets of elements of some type ฮฑ, is bounded above by the product of the number of elements in ๐’œ and โ„ฌ. More specifically, the number of elements in the intersection, multiplied by 2 raised to the power of the number of elements in ฮฑ, is at most the product of the number of elements in ๐’œ and โ„ฌ. This holds under the conditions that ๐’œ is a lower set and โ„ฌ is an upper set. Here, a lower set is a set such that any element less than one of its members is also a member, while an upper set is a set such that any element greater than one of its members is also a member. The type ฮฑ is required to have decidable equality, meaning that equality between any two elements of ฮฑ can be decided.

More concisely: The number of elements in the intersection of two finite sets ๐’œ and โ„ฌ of type ฮฑ, each being a lower set and an upper set respectively with decidable equality, is bounded above by the product of their respective sizes.

IsLowerSet.le_card_inter_finset

theorem IsLowerSet.le_card_inter_finset : โˆ€ {ฮฑ : Type u_1} [inst : DecidableEq ฮฑ] {๐’œ โ„ฌ : Finset (Finset ฮฑ)} [inst_1 : Fintype ฮฑ], IsLowerSet โ†‘๐’œ โ†’ IsLowerSet โ†‘โ„ฌ โ†’ ๐’œ.card * โ„ฌ.card โ‰ค 2 ^ Fintype.card ฮฑ * (๐’œ โˆฉ โ„ฌ).card

The theorem stated is known as the **Harris-Kleitman inequality**. It asserts that for any type `ฮฑ` with decidable equality and two finsets `๐’œ` and `โ„ฌ` of finsets of `ฮฑ`, if both `๐’œ` and `โ„ฌ` are lower sets, then the product of the cardinalities of `๐’œ` and `โ„ฌ` is less than or equal to two to the power of the cardinality of `ฮฑ` times the cardinality of the intersection of `๐’œ` and `โ„ฌ`. This theorem is a key result in the theory of posets and has many applications. It shows a fundamental correlation between any two lower sets of finsets.

More concisely: For any decidably equal type `ฮฑ` and lower sets `๐’œ` and `โ„ฌ` of finsets of `ฮฑ`, the product of their cardinalities is bounded above by 2^(|ฮฑ|) * |๐’œ โˆฉ โ„ฌ|.

IsUpperSet.le_card_inter_finset

theorem IsUpperSet.le_card_inter_finset : โˆ€ {ฮฑ : Type u_1} [inst : DecidableEq ฮฑ] {๐’œ โ„ฌ : Finset (Finset ฮฑ)} [inst_1 : Fintype ฮฑ], IsUpperSet โ†‘๐’œ โ†’ IsUpperSet โ†‘โ„ฌ โ†’ ๐’œ.card * โ„ฌ.card โ‰ค 2 ^ Fintype.card ฮฑ * (๐’œ โˆฉ โ„ฌ).card

The **Harris-Kleitman Inequality** theorem states that for any two upper sets of finite sets (`๐’œ` and `โ„ฌ`), the product of the cardinalities of `๐’œ` and `โ„ฌ` is less than or equal to two raised to the power of the cardinality of a certain finite type `ฮฑ` times the cardinality of the intersection of `๐’œ` and `โ„ฌ`. An upper set in this context is a set such that if an element is a member of the set, then any element greater than or equal to it is also a member of the set. This theorem requires that `ฮฑ` has decidable equality and is a finite type.

More concisely: For any two finite sets of upper sets `๐’œ` and `โ„ฌ` over a finite type `ฮฑ` with decidable equality, the product of their cardinalities is bounded above by 2^|ฮฑ| \* |๐’œ โˆฉ โ„ฌ|.

IsLowerSet.le_card_inter_finset'

theorem IsLowerSet.le_card_inter_finset' : โˆ€ {ฮฑ : Type u_1} [inst : DecidableEq ฮฑ] {๐’œ โ„ฌ : Finset (Finset ฮฑ)} {s : Finset ฮฑ}, IsLowerSet โ†‘๐’œ โ†’ IsLowerSet โ†‘โ„ฌ โ†’ (โˆ€ t โˆˆ ๐’œ, t โŠ† s) โ†’ (โˆ€ t โˆˆ โ„ฌ, t โŠ† s) โ†’ ๐’œ.card * โ„ฌ.card โ‰ค 2 ^ s.card * (๐’œ โˆฉ โ„ฌ).card

**Harris-Kleitman inequality**: Given any two lower sets of finite sets, denoted as `๐’œ` and `โ„ฌ` respectively, and assuming that each set `t` in both `๐’œ` and `โ„ฌ` is a subset of a certain finite set `s`, the product of the cardinality of `๐’œ` and `โ„ฌ` is less than or equal to two raised to the power of the cardinality of `s` times the cardinality of the intersection of `๐’œ` and `โ„ฌ`. Here, a lower set is defined in an ordered set `ฮฑ` as a set in which any element less than or equal to one of its members is also a member. Also, `ฮฑ` is assumed to have decidable equality, meaning that equality between any two elements in `ฮฑ` is decidable.

More concisely: Given two lower sets `๐’œ` and `โ„ฌ` of finite subsets of a finite set `s` with decidable equality, the product of their cardinalities is less than or equal to 2 raised to the power of the cardinality of `s` times the cardinality of their intersection.