Hindman.FP.mul
theorem Hindman.FP.mul :
∀ {M : Type u_1} [inst : Semigroup M] {a : Stream' M} {m : M},
m ∈ Hindman.FP a → ∃ n, ∀ m' ∈ Hindman.FP (Stream'.drop n a), m * m' ∈ Hindman.FP a
The theorem `Hindman.FP.mul` states that for any type `M` with a semigroup structure, any stream `a` of elements from `M`, and any element `m` from the Hindman finite product set of `a`, there exists a natural number `n` such that for any element `m'` from the Hindman finite product set of the subsequence of `a` starting from the `n`th position, the product of `m` and `m'` is also in the Hindman finite product set of `a`. In other words, the product of any two finite products in a Hindman sequence is again a finite product in that sequence, provided that the second product is obtained from a sufficiently late subsequence.
More concisely: For any semigroup type `M` and stream `a` of elements from `M`, if `m` is in the Hindman finite product set of `a` and `m'` is in the Hindman finite product set of the subsequence starting from some index `n`, then their product `m * m'` is also in the Hindman finite product set of `a`.
|
Hindman.FS_partition_regular
theorem Hindman.FS_partition_regular :
∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (s : Set (Set M)),
s.Finite → Hindman.FS a ⊆ s.sUnion → ∃ c ∈ s, ∃ b, Hindman.FS b ⊆ c
The strong form of Hindman's theorem states that for any type `M` endowed with an addition operation (`AddSemigroup`), given an infinite stream `a` of type `M` and a finite cover `s` of an FS-set of `a`, there exists a part `c` in `s` and an infinite stream `b` such that `b` is an FS-set and is contained within `c`. In other words, no matter how you partition an FS-set with a finite number of subsets, you can always find a subset that still contains an FS-set. Here, `FS` stands for Finite Sums, indicating that the set contains all possible sums of finite nonempty subsequences of the original sequence.
More concisely: For any infinite sequence `a` in an additive semigroup `M`, and any finite cover `s` of the finite sums set of `a`, there exists a subset `c` in `s` and an infinite subsequence `b` of `a` such that `b` is a finite sum set contained in `c`.
|
Hindman.FP_partition_regular
theorem Hindman.FP_partition_regular :
∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (s : Set (Set M)),
s.Finite → Hindman.FP a ⊆ s.sUnion → ∃ c ∈ s, ∃ b, Hindman.FP b ⊆ c
The strong form of Hindman's theorem states that for any type `M` that forms a semigroup, given an infinite stream `a` of type `M`, and a finite cover `s` of a Furstenberg-Peterson (FP) set of `a`, if the FP set of `a` is a subset of the union of sets in `s`, then there exists a set `c` within `s` and an infinite stream `b` such that the FP set of `b` is a subset of `c`. In simpler terms, this theorem assures us that within any finite cover of an FP-set, we can always find a set that also contains an FP-set.
More concisely: Given an infinite semigroup sequence `a` and a finite cover `s` of its Furstenberg-Peterson set, if the Furstenberg-Peterson set is contained in the union of sets in `s`, then there exists a set `c` in `s` containing another infinite semigroup sequence `b` with its Furstenberg-Peterson set contained in `c`.
|
Hindman.exists_FS_of_finite_cover
theorem Hindman.exists_FS_of_finite_cover :
∀ {M : Type u_1} [inst : AddSemigroup M] [inst_1 : Nonempty M] (s : Set (Set M)),
s.Finite → ⊤ ⊆ s.sUnion → ∃ c ∈ s, ∃ a, Hindman.FS a ⊆ c
This is the weak form of Hindman's theorem: For any nonempty additive semigroup `M` and any finite cover `s` of `M` (a collection of sets whose union includes all elements of `M`), there exists a set `c` in the cover and an element `a` such that the FS-set of `a` (a set of all finite sums that can be obtained from an infinite sequence starting with `a`) is contained within `c`. Here, an additive semigroup is a set equipped with an associative addition operation.
More concisely: For any nonempty additive semigroup and finite cover, there exists an element and a set in the cover containing all finite sums of the element.
|
Hindman.FS.add
theorem Hindman.FS.add :
∀ {M : Type u_1} [inst : AddSemigroup M] {a : Stream' M} {m : M},
m ∈ Hindman.FS a → ∃ n, ∀ m' ∈ Hindman.FS (Stream'.drop n a), m + m' ∈ Hindman.FS a
The theorem, named `Hindman.FS.add`, states the following in the context of a type `M` that forms an additive semigroup: Given an infinite stream `a` of elements in `M`, and a finite sum `m` that belongs to the Hindman's Finite Sums (FS) of `a`, there exists a natural number `n` such that for every finite sum `m'` that belongs to the Hindman's FS of the stream obtained by dropping the first `n` elements of `a`, the sum of `m` and `m'` also belongs to the Hindman's FS of `a`.
To clarify, the Hindman's Finite Sums (FS) of a stream is the set of all sums that can be made from finite subsequences of the stream. Here, a finite sum is said to belong to the Hindman's FS of a stream if it can be obtained as the sum of some finite subsequence of the stream.
More concisely: Given an infinite additive semigroup sequence `a`, for any finite sum `m` in the set of Hindman's Finite Sums and for infinitely many natural numbers `n`, every finite sum in the Hindman's Finite Sums of the subsequence starting from index `n` also sums to a member in the Hindman's Finite Sums of `a`.
|
Hindman.exists_FP_of_finite_cover
theorem Hindman.exists_FP_of_finite_cover :
∀ {M : Type u_1} [inst : Semigroup M] [inst_1 : Nonempty M] (s : Set (Set M)),
s.Finite → ⊤ ⊆ s.sUnion → ∃ c ∈ s, ∃ a, Hindman.FP a ⊆ c
This is a weak form of Hindman's theorem stated in the context of semigroup theory. The theorem states that for any semigroup `M` (which must be nonempty), given a finite cover `s` of `M` (i.e., a collection of subsets of `M` whose union includes every element of `M`), there exists a subset `c` within this cover and an element `a` such that every future instance of `a` (i.e., every element in the FP-set of `a` as per Hindman's definition) is contained within `c`. Essentially, this theorem asserts that in a setting where a nonempty semigroup is covered with a finite number of subsets, you can always find a subset and an element within it that will generate a sequence of elements (through the semigroup operation) all contained within the same subset.
More concisely: For any nonempty semigroup and finite cover of subsets, there exists a subset and an element such that every instance of the element's FP-set lies within the subset.
|