De Branges's theorem (Bieberbach conjecture)

deBranges_theorem

Submitter: Junyan Xu.

Notes: Unavailable.

Source: John B. Conway, *Functions of One Complex Variable II*, Chapter 17.

Informal solution: Unavailable.

theorem declaration uses `sorry`deBranges (f : ℂ → ℂ) (diff : DifferentiableOn ℂ f (ball 0 1)) (inj : (ball 0 1).InjOn f)
    (h0 : f 0 = 0) (h1 : deriv f 0 = 1) (n : ℕ) : ‖iteratedDeriv n f 0 / n.factorial‖ ≤ n := byf:ℂ → ℂdiff:DifferentiableOn ℂ f (ball 0 1)inj:Set.InjOn f (ball 0 1)h0:f 0 = 0h1:deriv f 0 = 1n:ℕ⊢ ‖iteratedDeriv n f 0 / ↑n.factorial‖ ≤ ↑n
  sorryAll goals completed! 🐙

Solved by

• @ZhengyangZhang06 with Humanifa + GPT 5.6 sol on Jul 28, 2026

• @hanwenzhu with Seed Prover (ByteDance) on Jul 31, 2026