[Merged by Bors] - feat: volume of a complex ball

[xroblot]

We prove the formula for the area of a disc

theorem volume_ball (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) :
    volume (Metric.ball x r) = NNReal.pi * (ENNReal.ofReal r) ^ 2 

and deduce from this, the volume of complex balls

theorem volume_ball (a : ℂ) (r : ℝ) :  
    volume (Metric.ball a r) = NNReal.pi * (ENNReal.ofReal r) ^ 2

Co-authored-by: James Arthur
Co-authored-by: Benjamin Davidson
Co-authored-by: Andrew Souther

---

• depends on: [Merged by Bors] - feat: remove the diamond for Complex.measureSpace #6832
• depends on: [Merged by Bors] - feat: compute the integral of sqrt (1 - x ^ 2) #6905
• depends on: [Merged by Bors] - feat: Prove that the measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving  #7037

[jsm28]

Can Archive.Wiedijk100Theorems.AreaOfACircle be refactored in terms of this (or alternatively the 100.yaml entry repointed to this result, with something done about the doc string discussing how there should be a more general result for the n-ball)? I don't think we should need to have two completely separate proofs of essentially the same result.

[xroblot]

Can Archive.Wiedijk100Theorems.AreaOfACircle be refactored in terms of this (or alternatively the 100.yaml entry repointed to this result, with something done about the doc string discussing how there should be a more general result for the n-ball)? I don't think we should need to have two completely separate proofs of essentially the same result.

As the matter of fact, I took some ideas from AreaOfACircle for this PR (and I am planning to add the authors of this file as co-authors of this PR when I write down the description), the main difference being the way the integral of $\sqrt {1 - x ^2 }$ is computed. I did not explicitly state the result about the area of the disc since I was not sure where to put it, but now that I rethink about it, it could belong in theEuclideanSpace namespace (with a doc string about the $n$-dimensional ball).

In any case, I think it is fine to keep AreaOfACircle with the same proof since it is in Archive and was historically the first one to solve the corresponding 100.yaml problem.

[hrmacbeth]

with something done about the doc string discussing how there should be a more general result for the n-ball

By the way, @fpvandoorn and I recently proved the n-ball result. We will PR it soon (I hope) but had not discussed where it should go.

[xroblot]

with something done about the doc string discussing how there should be a more general result for the n-ball

By the way, @fpvandoorn and I recently proved the n-ball result. We will PR it soon (I hope) but had not discussed where it should go.

Great! I'll will wait until you PR your result with Floris and then use it to prove the volume of the complex ball.

Do you think #6905 is still worth keeping?

[hrmacbeth]

Actually, I think there's no reason to kill this PR -- it can join mathlib now and when ours is ready we can generalize it.

[xroblot]

Ok, in that case, I think it would be better to also have the result on the area of the disc in this PR and the question of where it belongs is still open...

[xroblot]

So we do have Euclidean.ball

[eric-wieser]

I think Euclidean.ball is intended only as an implementation detail elsewhere

[xroblot]

I think Euclidean.ball is intended only as an implementation detail elsewhere

So something like

example : volume (Euclidean.ball (0 : Fin 2 → ℝ) 1) = NNReal.pi 

is not the right way to state the result?

[eric-wieser]

In any case, I think it is fine to keep AreaOfACircle with the same proof since it is in Archive and was historically the first one to solve the corresponding 100.yaml problem.

I think we should replace the proof anyway, though perhaps leave the statement as is for now. If people want to see the historical solution, they can always look at the git history for that file. If you don't agree, it's perhaps worth starting a Zulip thread to see what the wider opinion on this is.

My view is that Archive should be demonstrations of the best way to do things with current mathlib, not just a historical leaderboard.

[xroblot]

By the way, @fpvandoorn and I recently proved the n-ball result. We will PR it soon (I hope) but had not discussed where it should go.

@hrmacbeth can you please share the statement that you proved with Floris. I am still not sure of the best way to state the dimension 2 version...

[eric-wieser]

Do you think it makes sense to add the ProdLp case now too (refactoring the existing proof), or leave that to a future PR?

[xroblot]

Do you think it makes sense to add the ProdLp case now too (refactoring the existing proof), or leave that to a future PR?

I think that will be for a future PR. The proof for this case is completely different than the one in this PR and, in any case, I think the more general proof in the future PR by @hrmacbeth and @fpvandoorn should be easier to adapt to the case Lp.

[eric-wieser]

bors d+

Thanks! sorry for forgetting about this.

[bors]

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

[xroblot]

bors d+

Thanks! sorry for forgetting about this.

Thanks. In fact, I have a new PR coming soon with the computation of the volume of the unit ball in all dimensions, for all Lp norms over the real and over the complex using #7693. I just need to do some clean up and finish proving one or two easy lemmas (famous last words).

[xroblot]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style