feat(measure_theory/integral/circle_transform): Circle transform results pt2

[CBirkbeck]

The contains the next set of results needed for #13500 . Note also the change of file name from pt1 since the name circle_integral_transform is no longer used (so the first 175 lines are not new).

---

[sgouezel]

Could you split this PR into two, one doing the renaming, and the other one adding the new content? This would make it easier to review.

[CBirkbeck]

Ok I changed the name here: #16387

[CBirkbeck]

• [x] depends on: #16387

[mcdoll]

Please add an empty line before the dashed line. Also you have to merge master and fix the merge conflicts (you can do that in github).

[CBirkbeck]

I just want to highlight this: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/compact.20limits.20of.20holomorphic.20functions/near/305131582