ThreeGPFree — Mathlib

English

For all N with N ≥ 4096, N·exp(−4√(ln N)) < rothNumberNat N.

Русский

Для всех N с N ≥ 4096 выполняется N e^{−4√(ln N)} < rothNumberNat N.

LaTeX

$$$$ N \\cdot \\exp(-4 \\sqrt{\\log N}) < rothNumberNat N \\quad (N \\ge 4096). $$$$

Lean4

/-- A set is **3GP-free** if it does not contain any non-trivial geometric progression of length
three. -/
@[to_additive /-- A set is **3AP-free** if it does not contain any non-trivial arithmetic
    progression of length three.

    This is also sometimes called a **non-averaging set** or **Salem-Spencer set**. -/
    ]
def ThreeGPFree : Prop :=
  ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a * c = b * b → a = b

Похожие утверждения