Roughly, Lipschitzness of the inverse of `exp (t * I)`

Stream: Is there code for X?

[Geoffrey Irving]

Do we have this, or something which can easily get to it:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Complex (abs exp I)
open scoped Real

lemma lipschitz_inv_exp_mul_I {t : ℝ} (m : t ∈ Set.Ioc (-π) π) :
    |t| ≤ π / 2 * abs (exp (t * I) - 1) := by
  sorry

[Geoffrey Irving]

It's equivalent to t^2 ≤ π^2/2 * (1 - cos t).

[Yaël Dillies]

I just proved this in a PR

[Yaël Dillies]

I needed to show the arc-distance and chord distance on the circle are equivalent

[Geoffrey Irving]

Yes, that’s also why I need it.

[Geoffrey Irving]

Which PR?

[Yaël Dillies]

#10226

[Geoffrey Irving]

Thanks! I will steal it for now with comments to strip it once it’s in.

[Geoffrey Irving]

Actually might just leave mine as sorry, as it’ll probably be in before I finish the rest of Koebe.

[Yaël Dillies]

(best way to make sure it's in is to review it :pray:)

[Geoffrey Irving]

Happy to! Anything I need to do prior to that, or should I just do it now? (Might end up as this evening.)

[Yaël Dillies]

Nothing to do prior to that. Anybody can review anything anytime

[Eric Wieser]

There is a review guide at https://leanprover-community.github.io/contribute/pr-review.html, which has lots of Lean-specific advice even if you're no stranger to code review.

[Geoffrey Irving]

Great, will read through that and review this evening.

[Geoffrey Irving]

Though there are already several reviewers? Not sure what the norms are in such situations.

[Jireh Loreaux]

You're always welcome to add your review, regardless of who else has reviewed.

[Jireh Loreaux]

Of course, you may want to read through what prior reviews have said so you don't duplicate.

[Geoffrey Irving]

"Approved", FWIW. But to check: where is the result I wanted in that PR? Is it elsewhere in the angle theory, and now there's a bridge between the two?

[Yaël Dillies]

Whoops sorry I meant #10525, not #10226

[Yaël Dillies]

Seems like my clipboard played me

[Geoffrey Irving]

I'll review that one too in a moment.