Gaps between divisors

DefinitionDivisor-gap sums (Erdős Problem 884)#✓fully proved

The statement that there is a real constant \(C > 0\) such that for every positive integer \(n\), if \(d_1 < d_2 < \dots < d_t\) are all the divisors of \(n\) in increasing order, then \(\sum_{1 \le i < j \le t} \frac{1}{d_j - d_i} \le C \left(1 + \sum_{1 \le i < t} \frac{1}{d_{i+1} - d_i}\right)\).

def Statement : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 0 < n → ∀ t : ℕ, ∀ d : Fin t → ℕ,
    (StrictMono d ∧ (∀ k, d k ∣ n) ∧ ∀ m : ℕ, m ∣ n → ∃ k, d k = m) →
    (∑ i : Fin t, ∑ j : Fin t, if i < j then (1 : ℝ) / (((d j - d i : ℕ) : ℝ)) else 0) ≤
      C * (1 +
        (∑ i : Fin t, ∑ j : Fin t,
          if j.val = i.val + 1 then (1 : ℝ) / (((d j - d i : ℕ) : ℝ)) else 0))

Used by 1

Used byErdős Problem 884 is false (Larsen)

TheoremErdős Problem 884 is false (Larsen)#●ready to prove

For every real constant \(C > 0\) there is a positive integer \(n\) whose divisors \(d_1 < d_2 < \dots < d_t\), listed in increasing order, satisfy \(\sum_{1 \le i < j \le t} \frac{1}{d_j - d_i} > C \left(1 + \sum_{1 \le i < t} \frac{1}{d_{i+1} - d_i}\right)\).

public theorem_wanted Statement_refuted : ¬ Statement

Sources

• Lean proof of the negative answer to Erdős Problem 884, https://github.com/Jayyhk/erdos-lean/blob/f8a51976fd2e66a52b4928c109fb9ae877a1a507/problems/884/Erdos884.lean.

Uses 1

Statement usesDivisor-gap sums (Erdős Problem 884)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.