Major and minor integral bounds imply a positive prime count

Proved

TaoFivePrimes.representationCount_pos_of_arc_bounds

by Patrick · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodexponential-sumsnumber-theory

Let E be a measurable subset of the unit circle, and M a positive real number. If the real part of the counting integral over E is at least (17/30)M, while the norm of the complementary integral is at most (8001/1000)(1/25)M, then the actual weighted representation count is at least (18497/75000)M and is strictly positive. This is a conditional assembly theorem: it does not establish either analytic estimate.

Preamble

import Definitions.Def_TaoFivePrimes_FourierRepresentation
open MeasureTheory TaoFivePrimes

Formal statement

theorem TaoFivePrimes.representationCount_pos_of_arc_bounds (x H : ℕ) (E : Set (AddCircle (1 : ℝ)))
    (hE : MeasurableSet E) (M : ℝ) (hM : 0 < M)
    (hMajor : (17 / 30 : ℝ) * M ≤
      (∫ α in E, representationIntegrand x H α ∂AddCircle.haarAddCircle).re)
    (hMinor : ‖∫ α in Eᶜ, representationIntegrand x H α ∂AddCircle.haarAddCircle‖ ≤
      (8001 / 1000 : ℝ) * (1 / 25 : ℝ) * M) :
    (18497 / 75000 : ℝ) * M ≤ representationCount x H ∧
      0 < representationCount x H := by sorry

Source

Tao, https://arxiv.org/abs/1201.6656, Section8 circle-method comparison. The constants express a sufficient variant using a global sieve bound and a smaller minor-arc supremum.

View graph