Browse › Real and complex analysis › 072 Brennan's conjecture and the integral-means spectrum
A strict inverse-first-power bound for univalent functions
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Ilia Binder, Oleg Ivrii, István Prause, Stanislav Smirnov, Brennan's Conjecture and the Universal Integral Means Spectrum (arXiv:2610.23853 [math.CV], 16 Oct 2026). Cites this paper and states that $B_b(t)\le t^2/4$ on $[-2,2]$, with strict inequality for $t\in(-2,2)\setminus\{0\}$. It gives a full argument only for the non-strict inequality and defers the details of strictness to a separate paper. [family-level]
Comments and discussion
- Ilia Binder, Oleg Ivrii, István Prause, Stanislav Smirnov, §1.2–1.3 of Brennan's Conjecture and the Universal Integral Means Spectrum (arXiv:2610.23853, 16 Oct 2026). The authors summarize this paper's strictness mechanism: "The strict inequality is guaranteed by a global harmonic obstruction." They also write that the AI proofs contain derivations "that, while correct, are redundant". [family-level]
Formalization
- OpenAI math release, Lean scope notes for family 072 (lean/docs/072.md). Describes the release's Lean formalization of the uniform bound $M_{-1}[f'](r)\le C(1-r)^{-1/4+\varepsilon}$ and of $B_b(-1)<1/4$, with no numerical value of $\varepsilon$ specified. The comparator statement is
StrictMeans.lean. [family-level]
Related prior literature mentioned by others
- Lars V. Ahlfors, Quasiconformal reflections (Acta Mathematica 109, 1963). Binder et al. identify this as an antecedent of the papers' critical-point maps. [family-level]
- Oleg Ivrii, Quasicircles of dimension 1+k^2 do not exist (arXiv:1511.07240, 2015). Binder–Ivrii–Prause–Smirnov (arXiv:2610.23853) cite this among works with which "evidence against [Kraetzer's conjecture] began to accumulate".
- Kari Astala, Oleg Ivrii, Antti Perälä, István Prause, Asymptotic variance of the Beurling transform (arXiv:1502.00459; GAFA 25 (2015)). Cited in arXiv:2610.23853 in the same group of works on evidence against Kraetzer's conjecture.
- Håkan Hedenmalm, Bloch functions, asymptotic variance, and geometric zero packing (arXiv:1602.03358; Amer. J. Math. 142 (2020)). Cited in arXiv:2610.23853 in the same group of works on evidence against Kraetzer's conjecture.
- Oleg Ivrii, On Makarov's principle in conformal mapping (arXiv:1604.05619; IMRN 2019). Cited in arXiv:2610.23853 in the same group; it relates asymptotic variance to the second derivative of the integral means spectrum at $0$.
Digests and expositions
- AI Proved What?, Four thirds to four? Brennan’s conjecture and the integral-means spectrum (episode 072, October 2026). Animated exposition and transcript covering both claims, Koebe endpoint behavior, the probability-law construction, and the saddle–maximum comparison; its status discussion does not incorporate the Binder–Ivrii–Prause–Smirnov follow-up. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 072
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/072.md. The Lean statements have not been checked by people against the paper's claims.
Family 072: 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.
Other papers in this family:
- Brennan's conjecture and sharp inverse-square integral means · September 24, 2026