Brennan's Conjecture

Reference:

• Wikipedia
• arXiv:2409.15074
• arXiv:2512.09330

def BrennanConjecture.unitDisk : Set ℂ

Equations

• BrennanConjecture.unitDisk = {z : ℂ | ‖z‖ < 1}

structure BrennanConjecture.IsUnivalentNormalized (f : ℂ → ℂ) : Prop

The standard class $\mathcal{S}$ of normalised univalent functions on $\mathbb{D}$.

• analyticOn : AnalyticOn ℂ f unitDisk
• injOn : Set.InjOn f unitDisk
• map_zero : f 0 = 0
• deriv_zero : deriv f 0 = 1

noncomputable def BrennanConjecture.integralMeansSpectrum (f : ℂ → ℂ) (τ : ℝ) : ℝ

$\beta_f(\tau) := \limsup_{r \to 1^-} \frac{\log \int_{-\pi}^{\pi} |f'(re^{i\theta})|^\tau \, d\theta}{|\log(1-r)|}$

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BrennanConjecture.universalSpectrum (τ : ℝ) : ℝ

Equations

• BrennanConjecture.universalSpectrum τ = sSup {β : ℝ | ∃ (f : ℂ → ℂ), BrennanConjecture.IsUnivalentNormalized f ∧ β = BrennanConjecture.integralMeansSpectrum f τ}

noncomputable def BrennanConjecture.universalSpectrumBounded (τ : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem BrennanConjecture.universalSpectrumBounded_le (τ : ℝ) : universalSpectrumBounded τ ≤ universalSpectrum τ

theorem BrennanConjecture.integralMeansSpectrum_id (τ : ℝ) : integralMeansSpectrum id τ = 0

theorem BrennanConjecture.brennan_universalSpectrum : universalSpectrum (-2) = 1

Brennan's conjecture, part 1: $B(-2) = 1$.

theorem BrennanConjecture.brennan_universalSpectrumBounded : universalSpectrumBounded (-2) = 1

Brennan's conjecture, part 2: $B_b(-2) = 1$.

theorem BrennanConjecture.brennan_spectra_eq : universalSpectrum (-2) = universalSpectrumBounded (-2)

Brennan's conjecture, part 3: $B(-2) = B_b(-2)$.

theorem BrennanConjecture.brennan : universalSpectrum (-2) = 1 ∧ universalSpectrumBounded (-2) = 1

Brennan's conjecture: $B(-2) = B_b(-2) = 1$.