35.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 8 contain sorry, 0 declared as axioms

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.
AE25 A. Novikov et al., AlphaEvolve: A coding agent for scientific and algorithmic discovery, arXiv:2506.13131 (2025), Appendix B.1.
GGTW25 B. Georgiev, J. Gómez-Serrano, T. Tao and A. Z. Wagner, Mathematical exploration and discovery at scale, arXiv:2511.02864 (2025), Section 6.2.

The constants of [CS17], [MV10], [AE25] and [GGTW25] are stated for functions supported on $[-1/4, 1/4]$; rescaling to $[0, 1]$ halves them.

Imports (1)

FormalConjecturesUtil

def Green35.IsUnitIntervalDensity A nonnegative integrable function on $[0,1]$ with total integral $1$ line 58 source
Source documentation
A nonnegative integrable function on $[0,1]$ with total integral $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: And, MeasureTheory.Integrable, MeasureTheory.MeasureSpace.volume, LE.le, OfNat.ofNat, Set, Function.support, Set.Icc, Eq, MeasureTheory.integral
24 instances, coercions and auxiliary constants left out.
```
def IsUnitIntervalDensity (f : ℝ → ℝ) : Prop :=
…
```
def Green35.c The infimum of $\|f \ast f\|_p$ over unit-interval densities line 62 source
Source documentation
The infimum of $\|f \ast f\|_p$ over unit-interval densities.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal
Proof uses: InfSet.sInf, Set.ofPred, Exists, Real, And, Green35.IsUnitIntervalDensity, Eq, MeasureTheory.eLpNorm, MeasureTheory.convolution, ContinuousLinearMap.lsmul, MeasureTheory.MeasureSpace.volume
36 instances, coercions and auxiliary constants left out.
```
noncomputable def c (p : ℝ≥0∞) : ℝ≥0∞ :=
…
```
theorem Green35.green_35.lower Lower bound for $c(p)$ for $1 < p \le \infty$, improving the known value $\sqrt{4/7}$ at $p = 2$ or the known value $0.64$ at $p = \infty$ sorry line 68 source
Source documentation
Lower bound for $c(p)$ for $1 < p \le \infty$, improving the known value $\sqrt{4/7}$ at $p = 2$ or the known value $0.64$ at $p = \infty$.

depends on sorry what this means
Statement uses: ENNReal, sorryAx, Bool.false, And, LT.lt, OfNat.ofNat, LE.le, Green35.c, Or, ENNReal.ofReal, Real.sqrt, HDiv.hDiv, Real, Nat, OfScientific.ofScientific, Bool.true, Top.top
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_35.lower :
    let lb : ℝ≥0∞ → ℝ≥0∞ := answer(sorry)
…
```
theorem Green35.green_35.upper Upper bound for $c(p)$ for $1 < p \le \infty$, improving the best-known value $0.7516$ at $p = \infty$ sorry line 77 source
Source documentation
Upper bound for $c(p)$ for $1 < p \le \infty$, improving the best-known value $0.7516$ at $p = \infty$.

depends on sorry what this means
Statement uses: ENNReal, sorryAx, Bool.false, And, LT.lt, OfNat.ofNat, LE.le, Green35.c, Top.top, OfScientific.ofScientific, Bool.true
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_35.upper :
    let ub : ℝ≥0∞ → ℝ≥0∞ := answer(sorry)
…
```
theorem Green35.variants.c_2_lower Lower bound for $c(2)$ from Green's first paper ([Gr01]); the constant is sqrt(4/7) (about 0.7559) sorry line 87 source
Source documentation
Lower bound for $c(2)$ from Green's first paper ([Gr01]); the constant is sqrt(4/7) (about 0.7559).

depends on sorry what this means
Statement uses: LE.le, ENNReal, ENNReal.ofReal, Real.sqrt, HDiv.hDiv, Real, OfNat.ofNat, Nat, Green35.c
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem c_2_lower : ENNReal.ofReal (Real.sqrt (4 / 7)) ≤ c 2 := by
…
```
Mentions: Green35.c
theorem Green35.variants.c_inf_lower Best-known lower bound for $c(\infty)$ due to Cloninger and Steinerberger ([CS17]) sorry line 92 source
Source documentation
Best-known lower bound for $c(\infty)$ due to Cloninger and Steinerberger ([CS17]).

depends on sorry what this means
Statement uses: LE.le, ENNReal, OfScientific.ofScientific, Bool.true, Green35.c, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem c_inf_lower : 0.64 ≤ c ∞ := by
…
```
Mentions: Green35.c
theorem Green35.variants.c_inf_upper Upper bound for $c(\infty)$ due to Matolcsi and Vinuesa ([MV10]); their step function has autoconvolution supremum $1.50972\ldots$, which rescales to $0.75486\ldots$ sorry line 98 source
Source documentation
Upper bound for $c(\infty)$ due to Matolcsi and Vinuesa ([MV10]); their step function has autoconvolution supremum $1.50972\ldots$, which rescales to $0.75486\ldots$.

depends on sorry what this means
Statement uses: LE.le, ENNReal, Green35.c, Top.top, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem c_inf_upper : c ∞ ≤ 0.7549 := by
…
```
Mentions: Green35.c
theorem Green35.variants.c_inf_upper_ae25 Documented declaration: c_inf_upper_ae25 sorry line 105 source
Source documentation
Upper bound for $c(\infty)$ found by AlphaEvolve ([AE25]) and recorded in Green's 2025 update; the step function there has autoconvolution supremum at most $1.5053$, which rescales to $0.75265$.

depends on sorry what this means
Statement uses: LE.le, ENNReal, Green35.c, Top.top, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem c_inf_upper_ae25 : c ∞ ≤ 0.75265 := by
…
```
Mentions: Green35.c
theorem Green35.variants.c_inf_upper_ggtw25 Best-known upper bound for $c(\infty)$ ([GGTW25], §6.2): a step function with autoconvolution supremum at most $1.5032$, which rescales to $0.7516$ sorry line 111 source
Source documentation
Best-known upper bound for $c(\infty)$ ([GGTW25], §6.2): a step function with autoconvolution supremum at most $1.5032$, which rescales to $0.7516$.

depends on sorry what this means
Statement uses: LE.le, ENNReal, Green35.c, Top.top, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem c_inf_upper_ggtw25 : c ∞ ≤ 0.7516 := by
…
```
Mentions: Green35.c
theorem Green35.variants.c_inf_lower_young A comparison bound from Young's inequality sorry line 116 source
Source documentation
A comparison bound from Young's inequality.

depends on sorry what this means
Statement uses: LE.le, ENNReal, HPow.hPow, Nat, Green35.c, OfNat.ofNat, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem c_inf_lower_young : (c 2) ^ 2 ≤ c ∞ := by
…
```
Mentions: Green35.c