Cotangent-to-cosecant transfer without a factor-three loss
ProvedOddGoldbach19.cosecant_bound_of_cotangent_sharphilbert-inequalitylarge-sievenumber-theory
Assume a real constant C bounds the cotangent quadratic form for every finite family of real frequencies with positive admissible circular gaps at most1, by C times the sum of squared complex coefficients divided by their gaps. Then, for every such family, the quadratic form with kernel pi/sin(pi*(theta_r-theta_s)) obeys the same bound with the same C. Both quadratic forms omit diagonal terms. Admissible circular gap means delta_r <= |theta_r-theta_s+m| for every distinct pair and every integer m. This is a conditional transfer theorem preserving the assumed constant; it does not itself assert that a particular cotangent bound holds.
Preamble
import Mathlib open scoped BigOperators ComplexConjugate
Formal statement
theorem OddGoldbach19.cosecant_bound_of_cotangent_sharp (C : ℝ)
(hCot : ∀ (κ : Type) [Fintype κ] [DecidableEq κ]
(θ δ : κ → ℝ) (v : κ → ℂ),
(∀ r, 0 < δ r) → (∀ r, δ r ≤ 1) →
(∀ r s, r ≠ s → ∀ m : ℤ, δ r ≤ |θ r - θ s + m|) →
‖∑ r, ∑ s, if r = s then (0 : ℂ) else
v r * conj (v s) * ((Real.pi : ℂ) *
Complex.cot ((Real.pi : ℂ) * ((θ r - θ s : ℝ) : ℂ)))‖ ≤
C * ∑ r, ‖v r‖ ^ 2 / δ r)
{ι : 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) * ((Real.pi : ℂ) *
(Complex.sin ((Real.pi : ℂ) * ((θ r - θ s : ℝ) : ℂ)))⁻¹)‖ ≤
C * ∑ r, ‖v r‖ ^ 2 / δ r := by sorrySource
Antiperiodic two-copy transfer of the cotangent Hilbert form. Refinement of the transfer used in platform WeightedHilbert_circle_cosecant_bound_sixteen, https://prove2.me/theorems/de62b18a-6cc5-46cb-9555-8b45ad09f4bf . Identity and proof derived locally; no quoted literature constant or priority claim.