# Brennan's conjecture and the integral-means spectrum

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

- [Brennan's conjecture and sharp inverse-square integral means](../../preprints/Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026/paper.pdf)
- [A strict inverse-first-power bound for univalent functions](../../preprints/A-strict-inverse-first-power-bound-for-univalent-functions-September-24-2026/paper.pdf)

## 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](../ComparatorChallenges/Brennan.lean) |
| Sharp endpoint divergence | [BrennanSharp.lean](../ComparatorChallenges/BrennanSharp.lean) |
| Strict inverse-first-power bound and consequences | [StrictMeans.lean](../ComparatorChallenges/StrictMeans.lean) |