Small solutions of diagonal congruences

TheoremSum-product sets cover the integers modulo a prime#●ready to prove

Let \(p\) be a prime and let \(A_1, A_2, A_3, D\) be subsets of \(\mathbb{Z}/p\mathbb{Z}\) with \(|A_1| |A_2| |A_3| |D| > p^3\). Then every residue class modulo \(p\) can be written as \(a_1 d + a_2 + a_3\) with \(a_1 \in A_1\), \(d \in D\), \(a_2 \in A_2\) and \(a_3 \in A_3\); that is, \(A_1 D + A_2 + A_3 = \mathbb{Z}/p\mathbb{Z}\).

public theorem_wanted product_add_add_eq_univ_of_card_mul_gt (p : ℕ) [Fact p.Prime]
    (A₁ A₂ A₃ D : Finset (ZMod p))
    (h : p ^ 3 < A₁.card * A₂.card * A₃.card * D.card) :
    A₁ * D + A₂ + A₃ = Finset.univ
Sources
  • Todd Cochrane, Misty Ostergaard, Craig Spencer, and Kathryn Wilson, A Note on Small Solutions to Diagonal Congruences, INTEGERS 26 (2026), Article A14, Lemma 3, quoting Lemma 8.3 of their reference [5] (a consequence of Sárközy's Corollary A).

TheoremDiagonal congruences in \(k\) variables are solvable#●ready to prove

Let \(p\) be a prime and \(k \ge 1\). For all integers \(a_1, \dots, a_k\) not divisible by \(p\) and every integer \(c\), there are integers \(x_1, \dots, x_k\) with \(a_1 x_1^k + \dots + a_k x_k^k \equiv c \pmod p\).

Equivalently, \(\Gamma(k, p) \le k\), where \(\Gamma(k, p)\) is the least \(n\) such that every such congruence in \(n\) variables is solvable; extra variables can be set to \(0\).

public theorem_wanted diagonal_congruence_solvable_of_card_eq_exponent (p : ℕ) [Fact p.Prime]
    {k : ℕ} (hk : 1 ≤ k) (a : Fin k → ℤ) (ha : ∀ i, ¬ (p : ℤ) ∣ a i) (c : ℤ) :
    ∃ x : Fin k → ℤ, ∑ i, a i * x i ^ k ≡ c [ZMOD p]
Sources
  • Todd Cochrane, Misty Ostergaard, Craig Spencer, and Kathryn Wilson, A Note on Small Solutions to Diagonal Congruences, INTEGERS 26 (2026), Article A14, Lemma 2.

TheoremSmooth solutions of diagonal equations (Chow–Lindqvist–Prendiville)#●ready to prove

For a natural number \(N\) and real \(\eta > 0\), let \(A(N, N^\eta)\) be the set of integers \(1 \le x \le N\) all of whose prime factors are at most \(N^\eta\). There is a real-valued function \(g\) on the natural numbers with \(g(k) = O(\log \log k / \log k)\) as \(k \to \infty\) such that for every \(k \ge 2\) there is \(\eta_0 > 0\) with the following property. Let \(c_1, \dots, c_s\) be nonzero integers such that \(\sum_{i \in I} c_i = 0\) for some nonempty \(I \subseteq \{1, \dots, s\}\), and suppose \(s \ge 5\) if \(k = 2\), \(s \ge 8\) if \(k = 3\), and \(s \ge k (\log k + \log \log k + 2 + g(k))\) if \(k \ge 4\). Then for every \(0 < \eta \le \eta_0\) there are a natural number \(N_0\) and constants \(C_1, C_2 > 0\) such that for all \(N \ge N_0\) the number of \(x \in A(N, N^\eta)^s\) with \(c_1 x_1^k + \dots + c_s x_s^k = 0\) is at least \(C_1 N^{s-k}\) and at most \(C_2 N^{s-k}\).

MetaMathlibExt.smooth_diagonal_solution_count_asymp · 17 lines 
public theorem_wanted smooth_diagonal_solution_count_asymp :
    ∃ g : ℕ → ℝ, (g =O[Filter.atTop] fun k : ℕ => Real.log (Real.log k) / Real.log k) ∧
      ∀ k : ℕ, 2 ≤ k → ∃ η₀ : ℝ, 0 < η₀ ∧
        ∀ (s : ℕ) (c : Fin s → ℤ), (∀ i, c i ≠ 0) →
          (∃ I : Finset (Fin s), I.Nonempty ∧ ∑ i ∈ I, c i = 0) →
          (k = 2 → 5 ≤ s) → (k = 3 → 8 ≤ s) →
          (4 ≤ k → (k : ℝ) * (Real.log k + Real.log (Real.log k) + 2 + g k) ≤ s) →
          ∀ η : ℝ, 0 < η → η ≤ η₀ →
            ∃ (N₀ : ℕ) (C₁ C₂ : ℝ), 0 < C₁ ∧ 0 < C₂ ∧ ∀ N : ℕ, N₀ ≤ N →
              C₁ * (N : ℝ) ^ ((s : ℝ) - k) ≤
                (((Fintype.piFinset fun _ : Fin s =>
                    Nat.smoothNumbersUpTo N (⌊(N : ℝ) ^ η⌋₊ + 1)).filter
                  fun x => ∑ i, c i * (x i : ℤ) ^ k = 0).card : ℝ) ∧
              (((Fintype.piFinset fun _ : Fin s =>
                    Nat.smoothNumbersUpTo N (⌊(N : ℝ) ^ η⌋₊ + 1)).filter
                  fun x => ∑ i, c i * (x i : ℤ) ^ k = 0).card : ℝ) ≤
                C₂ * (N : ℝ) ^ ((s : ℝ) - k)
Sources
  • Todd Cochrane, Misty Ostergaard, Craig Spencer, and Kathryn Wilson, A Note on Small Solutions to Diagonal Congruences, INTEGERS 26 (2026), Article A14, Theorem 2, quoting Chow, Lindqvist and Prendiville, Rado's criterion over squares and higher powers, J. Eur. Math. Soc. 23 (2021), Theorem B.1.

TheoremMany values of a smooth diagonal form modulo a prime#●ready to prove

For a natural number \(B\) and real \(\eta > 0\), let \(A(B, B^\eta)\) be the set of integers \(1 \le x \le B\) all of whose prime factors are at most \(B^\eta\). There is a real-valued function \(g\) on the natural numbers with \(g(k) = O(\log \log k / \log k)\) as \(k \to \infty\) such that for every \(k \ge 2\) there is \(\eta_0 > 0\) with the following property. Let \(0 < \eta \le \eta_0\) and let \(n \ge 1\) satisfy \(2n \ge 5\) if \(k = 2\), \(2n \ge 8\) if \(k = 3\), and \(2n \ge k (\log k + \log \log k + 2 + g(k))\) if \(k \ge 4\). Then there is \(C > 0\) such that for every prime \(p\), every natural number \(B \ge 1\) with \(n B^k \le p\) and all integers \(a_1, \dots, a_n\) not divisible by \(p\), the set of residues modulo \(p\) of \(a_1 x_1^k + \dots + a_n x_n^k\) with \(x \in A(B, B^\eta)^n\) has at least \(C B^k\) elements.

public theorem_wanted card_smooth_diagonal_values_ge :
    ∃ g : ℕ → ℝ, (g =O[Filter.atTop] fun k : ℕ => Real.log (Real.log k) / Real.log k) ∧
      ∀ k : ℕ, 2 ≤ k → ∃ η₀ : ℝ, 0 < η₀ ∧
        ∀ η : ℝ, 0 < η → η ≤ η₀ → ∀ n : ℕ, 1 ≤ n →
          (k = 2 → 5 ≤ 2 * n) → (k = 3 → 8 ≤ 2 * n) →
          (4 ≤ k → (k : ℝ) * (Real.log k + Real.log (Real.log k) + 2 + g k) ≤ 2 * n) →
          ∃ C : ℝ, 0 < C ∧ ∀ (p : ℕ) [Fact p.Prime] (B : ℕ), 1 ≤ B → n * B ^ k ≤ p →
            ∀ a : Fin n → ℤ, (∀ i, ¬ (p : ℤ) ∣ a i) →
              C * (B : ℝ) ^ k ≤
                (((Fintype.piFinset fun _ : Fin n =>
                    Nat.smoothNumbersUpTo B (⌊(B : ℝ) ^ η⌋₊ + 1)).image
                  fun x => ∑ i, (a i : ZMod p) * (x i : ZMod p) ^ k).card : ℝ)
Sources
  • Todd Cochrane, Misty Ostergaard, Craig Spencer, and Kathryn Wilson, A Note on Small Solutions to Diagonal Congruences, INTEGERS 26 (2026), Article A14, Lemma 1.

TheoremSmall solutions of diagonal congruences#●ready to prove

There is a real-valued function \(g\) on the natural numbers with \(g(k) = O(\log \log k / \log k)\) as \(k \to \infty\) such that for every \(k \ge 2\) there is a constant \(C > 0\) with the following property. Let \(n\) satisfy \(n \ge 9\) if \(k = 2\), \(n \ge 12\) if \(k = 3\), and \(n \ge \frac{3}{2} k (\log k + \log \log k + 2 + g(k))\) if \(k \ge 4\). Then for every prime \(p\), every integer \(c\) and all integers \(a_1, \dots, a_n\) not divisible by \(p\), the congruence \(a_1 x_1^k + \dots + a_n x_n^k \equiv c \pmod p\) has a solution in natural numbers \(x_1, \dots, x_n\) with \(1 \le x_i \le C p^{1/k}\) for every \(i\).

public theorem_wanted exists_small_solution_diagonal_congruence :
    ∃ g : ℕ → ℝ, (g =O[Filter.atTop] fun k : ℕ => Real.log (Real.log k) / Real.log k) ∧
      ∀ k : ℕ, 2 ≤ k → ∃ C : ℝ, 0 < C ∧
        ∀ n : ℕ, (k = 2 → 9 ≤ n) → (k = 3 → 12 ≤ n) →
          (4 ≤ k → 3 / 2 * (k : ℝ) * (Real.log k + Real.log (Real.log k) + 2 + g k) ≤ n) →
          ∀ (p : ℕ) [Fact p.Prime] (c : ℤ) (a : Fin n → ℤ), (∀ i, ¬ (p : ℤ) ∣ a i) →
            ∃ x : Fin n → ℕ, (∀ i, 1 ≤ x i ∧ (x i : ℝ) ≤ C * (p : ℝ) ^ ((1 : ℝ) / k)) ∧
              ∑ i, a i * (x i : ℤ) ^ k ≡ c [ZMOD p]
Sources
  • Todd Cochrane, Misty Ostergaard, Craig Spencer, and Kathryn Wilson, A Note on Small Solutions to Diagonal Congruences, INTEGERS 26 (2026), Article A14, Theorem 1.
5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.