Koebe quarter theorem

Stream: Is there code for X?

[Geoffrey Irving]

Do we have the Koebe quarter theorem: https://en.wikipedia.org/wiki/Koebe_quarter_theorem?

theorem koebe {f : ℂ → ℂ} (fa : AnalyticOn ℂ f (ball 0 1)) (fi : InjOn f (ball 0 1)) :
    ball (f 0) (deriv f 0 / 4) ⊆ f '' ball 0 1 := sorry

[Patrick Massot]

I would be surprised.

[Geoffrey Irving]

Okay, I'll prove it at some point. I need it to make pretty pictures.

[Patrick Massot]

Don't forget to use the momentum to prove the crazy generalization whose name I forgot.

[Patrick Massot]

But Wikipedia knows what I mean: https://en.wikipedia.org/wiki/De_Branges%27s_theorem

[Geoffrey Irving]

Yes, I know about that too, but isn't it way harder? :)

[Patrick Massot]

Sure, it is crazily harder. :grinning_face_with_smiling_eyes:

[Patrick Massot]

But sometimes when you don't tell people something is hard they find an easy way.

[Geoffrey Irving]

Too late: I read that Wikipedia page long ago. :)

[Patrick Massot]

So close...

[Vincent Beffara]

There is docs#DiffContOnCl.ball_subset_image_closedBall which kind of goes in the direction of the Koebe quarter theorem but is not what you are asking. I also have code somewhere proving the existence of primitives (and hence holomorphic square roots) in star-like domains, which IIRC is useful in the proof of Köbe.