FormalConjectures.OptimizationConstants.«1a»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtil

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

[T2026] Together AI, "EinsteinArena-new-SOTA: State-of-the-art results on open math problems," 2026, GitHub

[PBV2026] Piterbarg, Andrei, Jai Bajaj, and Derrick Vincent. "A multi-scale arcsine lower bound for the Sidon autocorrelation constant $C_{1a}$," 2026, GitHub

@[expose] public sectionopen MeasureTheory Setnamespace Constant1a

Tao's Optimization constant 1a / An autocorrelation constant related to Sidon sets: The largest constant $C$ such that $$\max_{-1/2 \le t \le 1/2} \int_{\mathbb{R}} f(t - x) f(x),dx \ge C \left(\int_{-1/4}^{1/4} f(x),dx\right)^2$$ for all nonnegative $f \colon \mathbb{R} \to \mathbb{R}$.

The inequality is only required for square-integrable $f$. This does not change the constant (see [M2010, §2]), and it guarantees that every autoconvolution integral exists and that the supremum over $t$ is finite. This number is related to the maximal size of Sidon sets in additive combinatorics.

noncomputable def C1a : ℝ :=
  sSup {C : ℝ | ∀ ⦃f : ℝ → ℝ⦄, 0 ≤ f → MemLp f 2 →
    C * (∫ x in (- 1 / 4)..(1 / 4), f x) ^ 2
      ≤ sSup {∫ x, f (t - x) * f x | t ∈ Icc (- 1 / 2 : ℝ) (1 / 2)}}

A lower bound, proven by Matolcsi-Vinuesa in [M2010].

@[category research solved, AMS 5 11 26]
theorem c1a_lower_bound : 1.2748 ≤ C1a := by⊢ 1.2748 ≤ C1a
  sorryAll goals completed! 🐙

An upper bound, proven by Yuksekgonul et al. in [Y2026].

@[category research solved, AMS 5 11 26]
theorem c1a_upper_bound : C1a ≤ 1.5029 := by⊢ C1a ≤ 1.5029
  sorryAll goals completed! 🐙

How can the best known upper bound $1.502862$ of [T2026] be improved?

@[category research open, AMS 5 11 26]
theorem mem_Ico_c1a : answer(sorry) ∈ Set.Ico C1a 1.502862 := by⊢ sorry ∈ Ico C1a 1.502862
  sorryAll goals completed! 🐙

How can the best known lower bound $1.292$ of [PBV2026] be improved?

@[category research open, AMS 5 11 26]
theorem mem_Ioc_c1a : answer(sorry) ∈ Set.Ioc 1.292 C1a := by⊢ sorry ∈ Ioc 1.292 C1a
  sorryAll goals completed! 🐙

What is the exact value of the constant?

@[category research open, AMS 5 11 26]
theorem c1a_eq : C1a = answer(sorry) := by⊢ C1a = sorry
  sorryAll goals completed! 🐙

-- TODO: Formalise relationship to Sidon sets.
-- TODO: State results from https://arxiv.org/abs/2602.07292

end Constant1a