Brennan's conjecture and the integral-means spectrum

2 papersLean

Proves Brennan's conjecture: for every conformal bijection ϕ from a simply connected plane domain onto the disk, \(|\phi'|^s\) is area-integrable for \(4/3\lt s\lt 4\). The sharp universal integral-means identity is \(B_{\mathcal S}(t)=|t|-1\) for t ≤ −2. A strict bound \(B_b(-1)\lt 1/4\) for bounded univalent functions disproves Kraetzer's prediction at that parameter.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Brennan's conjecture and sharp inverse-square integral means

OpenAI · September 24, 2026

We prove Brennan's conjecture: if a simply connected plane domain admits a conformal bijection φ onto the unit disk, then \(|\varphi'|^s\) is area-integrable for every \(4/3\lt s\lt 4\). We also prove the sharp inverse-square integral-means exponent \(B_{\mathcal S}(-2)=1\) for the normalized schlicht class \(\mathcal S\).

Read PDF Download Source

Cite

@misc{OAI:Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026,
  author = {{OpenAI}},
  title = {{Brennan's conjecture and sharp inverse-square integral means}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026/paper.pdf}{OAI:Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026}},
  year = {2026}
}

A strict inverse-first-power bound for univalent functions

OpenAI · September 24, 2026

We prove a uniform upper bound for inverse-first-power integral means of normalized univalent disk maps with exponent strictly below 1/4. Consequently, the bounded universal integral-means spectrum satisfies \(B_b(-1)\lt 1/4\), disproving Kraetzer's conjectured spectrum at p = −1.

Read PDF Download Source

Cite

@misc{OAI:A-strict-inverse-first-power-bound-for-univalent-functions-September-24-2026,
  author = {{OpenAI}},
  title = {{A strict inverse-first-power bound for univalent functions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-strict-inverse-first-power-bound-for-univalent-functions-September-24-2026/paper.pdf}{OAI:A-strict-inverse-first-power-bound-for-univalent-functions-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Brennan's conjecture asserts that \(|\phi'|^s\) is area-integrable for \(4/3<s<4\) when \(\phi\) conformally maps a simply connected plane domain with nontrivial spherical boundary onto the disk. The formalization establishes this interval, along with area integrability of \(|f'|^t\) for univalent disk maps when \(-2<t<2/3\).

It also gives the uniform inverse-square radial-mean bound with exponent \(-1-\varepsilon\) for every \(\varepsilon>0\) and the spectrum value \(B_{\mathcal S}(-2)=1\). The Koebe map and its inverse give divergence at all four boundary exponents.

Kraetzer's proposed integral-means spectrum predicts \(B_b(-1)=1/4\) for bounded univalent maps. The formalized result proves \(B_b(-1)<1/4\), contradicting that prediction.

The underlying estimate gives constants \(0<\varepsilon<1/4\) and \(C<\infty\) such that the normalized circular mean of \(|f'|^{-1}\) is at most \(C(1-r)^{-1/4+\varepsilon}\) for every normalized univalent disk map and \(1/2\le r<1\). The bound requires neither bounded image nor boundary regularity, and no numerical value of \(\varepsilon\) is specified.

Comparator links

Result	Comparator statement
Brennan and inverse-square integral-means bounds	Brennan.lean
Sharp endpoint divergence	BrennanSharp.lean
Strict inverse-first-power bound and consequences	StrictMeans.lean

Scope note on GitHub →