rothNumberNat_add_le
theorem rothNumberNat_add_le : ∀ (M N : ℕ), rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N
This theorem states that the Roth number is a subadditive function. In other words, for any two natural numbers M and N, the Roth number of the sum of M and N is less than or equal to the sum of the Roth number of M and the Roth number of N. This theorem is important because it implies, via Fekete's lemma, that the limit of `rothNumberNat N / N` as `N` approaches infinity exists. However, a stronger result, known as Roth's theorem, shows that this limit is actually zero.
More concisely: The Roth number of the sum of two natural numbers is less than or equal to the sum of their individual Roth numbers.
|
addRothNumber_spec
theorem addRothNumber_spec :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α),
∃ t ⊆ s, t.card = addRothNumber s ∧ AddSalemSpencer ↑t
The theorem `addRothNumber_spec` states that for any type `α` that has decidable equality and an addition operation, and for any finite set `s` of elements of the type `α`, there exists a subset `t` of `s` such that the cardinality of `t` is equal to the additive Roth number of `s` and `t` is a Salem-Spencer set. A Salem-Spencer set, in the context of an additive monoid, is a set in which the average of any two distinct elements is never in the set. The additive Roth number of a finite set is defined as the size of its largest Salem-Spencer subset.
More concisely: For any finite additive monoid (α, +) with decidable equality, there exists a Salem-Spencer subset of cardinality equal to the size of its largest Salem-Spencer subset.
|
addSalemSpencer_frontier
theorem addSalemSpencer_frontier :
∀ {𝕜 : Type u_4} {E : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace E]
[inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] {s : Set E},
IsClosed s → StrictConvex 𝕜 s → AddSalemSpencer (frontier s)
The theorem `addSalemSpencer_frontier` states that for any closed strictly convex set `s` over a linearly ordered field `𝕜` and topological space `E` with an additional structure of an additive commutative monoid and a `𝕜`-module, the frontier of `s` (the set of points between the closure and interior of `s`) only contains trivial arithmetic progressions. In other words, the frontier of `s` is a Salem-Spencer set, which means that the average of any two distinct elements of the frontier is not in the frontier. This is due to the fact that an arithmetic progression can only be contained on a line, whereas a strictly convex set does not contain any lines within its frontier.
More concisely: The frontier of a closed, strictly convex set over a linearly ordered field in a topological space with an additive commutative monoid and a module structure only contains trivial arithmetic progressions, making it a Salem-Spencer set.
|
rothNumberNat_isBigO_id
theorem rothNumberNat_isBigO_id : (fun N => ↑(rothNumberNat N)) =O[Filter.atTop] fun N => ↑N
This theorem, `rothNumberNat_isBigO_id`, establishes that the function mapping a natural number `N` to its Roth number `rothNumberNat N` is asymptotically bounded above by the identity function on `N`. Specifically, it states that `rothNumberNat N` is Big O of `N` as `N` approaches infinity, denoted by `Filter.atTop`. In other words, the growth rate of `rothNumberNat N` is at most linear in the size of `N` for large `N`.
More concisely: The Roth number function is Big O of the identity function as the natural number input approaches infinity.
|
addRothNumber_le
theorem addRothNumber_le :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α), addRothNumber s ≤ s.card
The theorem `addRothNumber_le` states that for any given finite set `s` of elements of an additive monoid `α` (with decidable equality), the additive Roth number of `s` is always less than or equal to the cardinality of `s`. The additive Roth number of a finite set is defined as the size of its largest additive Salem-Spencer subset. An additive Salem-Spencer subset is a set where no three elements have the property that two of them add to the third.
More concisely: The additive Roth number of a finite set in an additive monoid with decidable equality is bounded above by the set's cardinality.
|
AddSalemSpencer.mono
theorem AddSalemSpencer.mono :
∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α}, t ⊆ s → AddSalemSpencer s → AddSalemSpencer t
This theorem states that for any type `α` that forms an additive monoid, given two sets `s` and `t` of elements of this type, if `t` is a subset of `s` and `s` is a Salem-Spencer (non-averaging) set, then `t` is also a Salem-Spencer set. In other words, the property of being a Salem-Spencer set is preserved under taking subsets. A Salem-Spencer set is defined as a set in which the average of any two distinct elements does not belong to the set, or equivalently, if the sum of two distinct elements equals twice a third element in the set, then the two original elements must be equal.
More concisely: If `α` is an additive monoid type, `s` is a Salem-Spencer set, and `t` is a subset of `s`, then `t` is also a Salem-Spencer set.
|
mulRothNumber_spec
theorem mulRothNumber_spec :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α),
∃ t ⊆ s, t.card = mulRothNumber s ∧ MulSalemSpencer ↑t
The theorem `mulRothNumber_spec` asserts that for all types `α` with decidable equality and monoid structure, and for any finite set `s` of type `α`, there exists a subset `t` of `s` such that the cardinality of `t` equals the multiplicative Roth number of `s` and `t` is a multiplicative Salem-Spencer set. A multiplicative Salem-Spencer set is a set where the product of any two distinct elements cannot be the square of any element in the set. The multiplicative Roth number of a set is defined as the size of its largest multiplicative Salem-Spencer subset.
More concisely: For any finite set `s` with type `α` having decidable equality and monoid structure, there exists a multiplicative Salem-Spencer subset `t` of `s` with the same cardinality as the multiplicative Roth number of `s`, such that the pairwise products of distinct elements in `t` are not squares of elements in `t`.
|
MulSalemSpencer.le_mulRothNumber
theorem MulSalemSpencer.le_mulRothNumber :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s t : Finset α},
MulSalemSpencer ↑s → s ⊆ t → s.card ≤ mulRothNumber t
The theorem `MulSalemSpencer.le_mulRothNumber` asserts that for any type `α` which has decidable equality and is a monoid, and for any finite sets `s` and `t` of `α`, if `s` is a multiplicative Salem-Spencer set (i.e., for any distinct elements `a`, `b`, and `c` in `s`, if `a * b = c * c`, then `a = b`) and `s` is a subset of `t`, then the cardinality of `s` is less than or equal to the multiplicative Roth number of `t`. The multiplicative Roth number of a finite set is defined as the size of its largest multiplicative Salem-Spencer subset.
More concisely: For any finite subset `s` of a monoid `α` with decidable equality that is a multiplicative Salem-Spencer set, the size of `s` is bounded above by the multiplicative Roth number of any larger finite subset of `α` containing `s`.
|
AddSalemSpencer.le_addRothNumber
theorem AddSalemSpencer.le_addRothNumber :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s t : Finset α},
AddSalemSpencer ↑s → s ⊆ t → s.card ≤ addRothNumber t
The theorem `AddSalemSpencer.le_addRothNumber` states that for any type `α` that has decidable equality and an additive monoid structure, and for any two finite sets `s` and `t` of this type, if `s` is a Salem-Spencer set (meaning that the average of any two distinct elements of `s` is not in `s`) and `s` is a subset of `t`, then the cardinality (or size) of `s` is less than or equal to the additive Roth number of `t`. The additive Roth number of a finite set is the maximum size of a Salem-Spencer subset of that set.
More concisely: For any type `α` with decidable equality and additive monoid structure, if `s` is a finite Salem-Spencer subset of a larger finite set `t`, then the cardinality of `s` is bounded above by the additive Roth number of `t`.
|
AddSalemSpencer.le_rothNumberNat
theorem AddSalemSpencer.le_rothNumberNat :
∀ {k n : ℕ} (s : Finset ℕ), AddSalemSpencer ↑s → (∀ x ∈ s, x < n) → s.card = k → k ≤ rothNumberNat n
This theorem states that for any natural numbers `k` and `n`, and any finite set `s` of natural numbers, if `s` is a Salem-Spencer set (that is, a set such that the average of any two distinct elements is not in the set), every element `x` in `s` is less than `n`, and the cardinality of `s` is `k`, then `k` is less than or equal to the Roth number of `n`. The Roth number of a natural number `n` is the maximum size of any subset of the integers from `1` to `n-1` that does not contain a solution to the equation `x + y = 2z` for distinct `x`, `y`, and `z`.
More concisely: For any natural numbers `k`, `n`, and finite set `s` of natural numbers such that `s` is a Salem-Spencer set, every `x` in `s` is less than `n`, and the cardinality of `s` is `k`, it holds that `k` is bounded above by the Roth number of `n`.
|