Tail three-family assembly from single tail quotient subset

Proved

Erdos390.tail_three_family_of_single_tail

by doctosil · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

asymptoticscombinatoricsnumber-theory

Let $n, h, D \in \mathbb{N}$ and let $\mathrm{tail} \subseteq (2n, 2n + h]$ be a finite subset such that $\left(\prod_{a \in \mathrm{tail}} a\right) \cdot D = \prod_{k \in (2n, 2n + h]} k$ . Then setting $\mathrm{fixed} = \mathrm{tail}$ and $\mathrm{bank} = \mathrm{candidates} = \emptyset$ produces three pairwise disjoint subsets of $(2n, 2n + h]$ satisfying:

\left(\prod_{a \in \mathrm{fixed}} a\right) \cdot \left(\prod_{b \in \mathrm{bank}} b\right) \cdot \left(\prod_{c \in \mathrm{candidates}} c\right) \cdot D = \prod_{k \in (2n, 2n + h]} k.

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_three_family_of_single_tail
    {n h D : ℕ} {tail : Finset ℕ}
    (htail_sub : tail ⊆ factorInterval (2 * n) (2 * n + h))
    (hprod : tail.prod id * D = (factorInterval (2 * n) (2 * n + h)).prod id) :
    ∃ (fixed bank candidates : Finset ℕ),
      fixed ⊆ factorInterval (2 * n) (2 * n + h) ∧
      bank ⊆ factorInterval (2 * n) (2 * n + h) ∧
      candidates ⊆ factorInterval (2 * n) (2 * n + h) ∧
      Disjoint fixed bank ∧
      Disjoint fixed candidates ∧
      Disjoint bank candidates ∧
      fixed.prod id * bank.prod id * candidates.prod id * D =
        (factorInterval (2 * n) (2 * n + h)).prod id := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Erdős Problem 390 tail three-family assembly

View graph