Ben Green's Open Problem 35

Estimate the infimum of the $L^p$ norm of the self-convolution of a nonnegative integrable function supported on $[0,1]$ with total integral $1$.

We model a function f : [0,1] → ℝ≥0 as a function f : ℝ → ℝ that is nonnegative, integrable, supported on [0,1], and has total integral 1.

References:

• Ben Green's Open Problem 35
• Gr01 B. J. Green, The number of squares and $B_h[g]$-sets, Acta Arith. 100 (2001), no. 4, 365-390.
• CS17 A. Cloninger and S. Steinerberger, On suprema of autoconvolutions with an application to Sidon sets, Proc. Amer. Math. Soc. 145 (2017), no. 8, 3191-3200.
• MV10 M. Matolcsi and C. Vinuesa, Improved bounds on the supremum of autoconvolutions, J. Math. Anal. Appl. 372 (2010), 439-447.

def Green35.IsUnitIntervalDensity (f : ℝ → ℝ) : Prop

A nonnegative integrable function on $[0,1]$ with total integral $1$.

Equations

• Green35.IsUnitIntervalDensity f = (MeasureTheory.Integrable f MeasureTheory.volume ∧ (∀ (x : ℝ), 0 ≤ f x) ∧ Function.support f ⊆ Set.Icc 0 1 ∧ ∫ (x : ℝ), f x = 1)

noncomputable def Green35.c (p : ENNReal) : ENNReal

The infimum of $\|f \ast f\|_p$ over unit-interval densities.

Equations

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

theorem Green35.green_35.lower : have lb := sorry; (∀ (p : ENNReal), 1 < p → lb p ≤ c p) ∧ (ENNReal.ofReal √(4 / 7) < c 2 ∨ 0.64 < c ⊤)

Lower bound for $c(p)$ for $1 < p \le \infty$, improving the known value at $p = 2$ or $p = \infty$.

theorem Green35.green_35.upper : have ub := sorry; (∀ (p : ENNReal), 1 < p → c p ≤ ub p) ∧ ub ⊤ < 0.7505

Upper bound for $c(p)$ for $1 < p \le \infty$, improving the best-known value at $p = \infty$.

Known bounds and comparisons.

theorem Green35.variants.c_2_lower : ENNReal.ofReal √(4 / 7) ≤ c 2

Lower bound for $c(2)$ from Green's first paper ([Gr01]); the constant is sqrt(4/7) (about 0.7559).

theorem Green35.variants.c_inf_lower : 0.64 ≤ c ⊤

Best-known lower bound for $c(\infty)$ due to Cloninger and Steinerberger ([CS17]).

theorem Green35.variants.c_inf_upper : c ⊤ ≤ 0.7505

Best-known upper bound for $c(\infty)$ due to Matolcsi and Vinuesa ([MV10]).

theorem Green35.variants.c_inf_lower_young : c 2 ^ 2 ≤ c ⊤

A comparison bound from Young's inequality.