Tao's Optimization constant 1a / An autocorrelation constant related to Sidon sets

References:

• Tao's optimization constant 1a
• [M2010] Matolcsi, Máté, and Carlos Vinuesa. "Improved bounds on the supremum of autoconvolutions." Journal of mathematical analysis and applications 372.2 (2010): 439-447. arXiv:0907.1379
• [Y2026] Yuksekgonul, Mert et al., "Learning to Discover at Test Time," 2026, arXiv:2601.16175

noncomputable def Constant1a.C1a : ℝ

Tao's Optimization constant 1a / An autocorrelation constant related to Sidon sets: The biggest real number satisfying a certain inequality about (auto)convolutions and $L^2$-norms of functions. This number is related to the maximal size of Sidon sets in additive combinatorics.

Equations

• One or more equations did not get rendered due to their size.

theorem Constant1a.c1a_lower_bound : 1.2748 ≤ C1a

The best known lower bound, proven by Matolcsi-Vinuesa in [M2010]

theorem Constant1a.c1a_upper_bound : C1a ≤ 1.5029

The best known upper bound, proven by Yuksekgonul et al. in [Y2026]

theorem Constant1a.mem_Ico_c1a : sorry ∈ Set.Ico C1a 1.5029

How can the upper bound be improved?

theorem Constant1a.mem_Ioc_c1a : sorry ∈ Set.Ioc 1.2748 C1a

How can the lower bound be improved?

theorem Constant1a.c1a_eq : C1a = sorry

What is the exact value of the constant?