English
For a finite set s in α, mulRothNumber s is defined as the maximum size of a GP-free subset of s.
Русский
Для конечного множества s в α число mulRothNumber s есть максимальный размер подмножества GP-free внутри s.
LaTeX
$$$mulRothNumber(s) = \max\{ |t| : t \subseteq s \land ThreeGPFree(t)\}$$$
Lean4
/-- The multiplicative Roth number of a finset is the cardinality of its biggest 3GP-free subset. -/
@[to_additive /-- The additive Roth number of a finset is the cardinality of its biggest 3AP-free
subset.
The usual Roth number corresponds to `addRothNumber (Finset.range n)`, see `rothNumberNat`. -/
]
def mulRothNumber : Finset α →o ℕ :=
⟨fun s ↦ Nat.findGreatest (fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (t : Set α)) #s,
by
rintro t u htu
refine Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)
rintro ⟨v, hvt, hv⟩
exact ⟨v, hvt.trans htu, hv⟩⟩
