circle integral

Stream: maths

[Yury G. Kudryashov]

In order to make #100000 more readable, I'm going to define circle_integral (f : ℂ → E) (c : ℂ) (R : ℝ) : E to be $\int_{|z-c|=R} f(z)\,dz$ defined as $\int_0^{2\pi} Re^{i\theta}if(c+Re^{i\theta})\,d\theta$. Most theorems will assume various facts about the restriction of f to metric.sphere c R or metric.closed_ball c R. For $R < 0$, these sets are empty, and I need to use |R| instead of R. Which way of dealing with this fact do you prefer?

[Yury G. Kudryashov]

/poll What should be the type of R?
ℝ≥0, then we have 0 ≤ R automatically but users need to lift R to ℝ≥0 if it is ℝ;
ℝ and assume 0 ≤ R as needed;
ℝ and use sphere c |R|, closed_ball c |R|.

[Johan Commelin]

I hope you are talking about #10000 :wink:

[Yury G. Kudryashov]

Johan Commelin said:

I hope you are talking about #10000 :wink:

Fixed. I should learn to count to 4.