Circle Hilbert bound with constant five

Proved

OddGoldbach19.circle_cosecant_bound_five

by Yuxuan Xu · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

large-sievenumber-theory

For every finite family of real frequencies theta_r and complex coefficients v_r with circular gaps delta_r positive and at most1, assume delta_r <= |theta_r-theta_s+m| for all distinct r,s and all integers m. Then the norm of the off-diagonal sum v_rconj(v_s)/sin(pi(theta_r-theta_s)) is at most5 times the sum of |v_r|^2/delta_r. This improves the previously proved constant16 under the same hypotheses.

Preamble

import Mathlib
open scoped BigOperators ComplexConjugate

Formal statement

theorem OddGoldbach19.circle_cosecant_bound_five {ι : Type} [Fintype ι] [DecidableEq ι]
    (θ δ : ι → ℝ) (v : ι → ℂ)
    (hpos : ∀ r, 0 < δ r) (hunit : ∀ r, δ r ≤ 1)
    (hgap : ∀ r s, r ≠ s → ∀ m : ℤ, δ r ≤ |θ r - θ s + m|) :
    ‖∑ r, ∑ s, if r = s then (0 : ℂ) else
      v r * conj (v s) /
        Complex.sin ((Real.pi : ℂ) * ((θ r - θ s : ℝ) : ℂ))‖ ≤
      5 * ∑ r, ‖v r‖ ^ 2 / δ r := by sorry

Source

Derived refinement of existing public Prove2Me weighted Hilbert and pair-sieve proof chain; see proof explanation for precise reused accepted submission IDs.

View graph