[Merged by Bors] - feat(measure_theory/integral): Circle integral transform

[CBirkbeck]

Some basic definitions and results related to circle integrals of a function. These form part of #13500

---

[loefflerd]

Some cosmetic code-style fixes

[CBirkbeck]

Some cosmetic code-style fixes

Done. Thank you!

[sgouezel]

Can you merge master to fix the build? (The linting problem is not your fault, the solution is to merge master where it has been solved).

[loefflerd]

More stylistic nitpicking

[loefflerd]

I golfed it a bit, and rearranged the code to make things slightly more readable. The only change to functionality is that I made a few arguments to lemmas implicit (curly braces rather than brackets).

[loefflerd]

Here are some comments of a little more mathematical substance.

• How do you distinguish between what goes in circle_integral.lean and what goes in circle_integral_transform.lean? In particular the last few lemmas of the existing file explicitly involve the Cauchy integral formula, so the distinction between the two files seems a bit unclear to me.
• There is a lot of juggling between different versions of intervals -- we have [0, 2 * π], interval 0 (2 * π), and Ι 0 (2 * π) (the last being particularly unfortunate for readability since the Greek capital Iota is visually identical to roman I). May I suggest standardizing all statements to [0, 2 * π]? If you need to call lemmas from other files which expect a half-open interval, you can just use an Ioc_subset_Icc_self inline, rather than making a separate lemma for it.

[CBirkbeck]

There is a lot of juggling between different versions of intervals -- we have [0, 2 * π], interval 0 (2 * π), and Ι 0 (2 * π) (the last being particularly unfortunate for readability since the Greek capital Iota is visually identical to roman I). May I suggest standardizing all statements to [0, 2 * π]? If you need to call lemmas from other files which expect a half-open interval, you can just use an Ioc_subset_Icc_self inline, rather than making a separate lemma for it.

This is a good point. I've removed some of the lemmas that are now redundant.

[CBirkbeck]

How do you distinguish between what goes in circle_integral.lean and what goes in circle_integral_transform.lean? In particular the last few lemmas of the existing file explicitly involve the Cauchy integral formula, so the distinction between the two files seems a bit unclear to me.

I really don't know how to distinguish. I just thought it would be easier having it in a separate file, but if its preferable I could just put this in a section of circle_integral. But once the rest of the #13500 is added it might be a bit long...

[bors]

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[CBirkbeck]

bors r+

[bors]

Canceled.

[CBirkbeck]

bors r+

[bors]

Build failed:

• Build mathlib

[CBirkbeck]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[CBirkbeck]

bors d+ Thanks!

I think I did things in the wrong order and now bors isnt working for me. Does it need to be delegated again?

[bors]

Build failed:

• Build mathlib

[loefflerd]

You need to fix the build error or it won't merge. It you click through to bors' build log it says something about a failure at circle_integral_transform.lean:62

[CBirkbeck]

bors r+

[CBirkbeck]

You need to fix the build error or it won't merge. It you click through to bors' build log it says something about a failure at circle_integral_transform.lean:62

Thanks, I couldn't see the error as I hadn't bumped my version of lean.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests