Brennan's conjecture and the integral-means spectrum

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. (Lean)

Manuscripts (2)

Brennan's conjecture and sharp inverse-square integral means

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Brennans-conjecture-and-sharp-inverse-square-integral-means-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.

A strict inverse-first-power bound for univalent functions

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:A-strict-inverse-first-power-bound-for-univalent-functions-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.

Result 072 · Real and complex analysis. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.