[Merged by Bors] - feat: compute the integral of sqrt (1 - x ^ 2)

[xroblot]

We prove

theorem integral_sqrt_one_sub_sq : ∫ x in (-1 : ℝ)..1, sqrt (1 - x ^ 2) = π / 2

which will in turn be used to compute the area of the disc and then the volume of the unit complex ball in #6907

---

[Ruben-VandeVelde]

I'd probably move this theorem to the end of the file, rather than putting it between two sections about trig integrals

[xroblot]

I'd probably move this theorem to the end of the file, rather than putting it between two sections about trig integrals

Yes, I thought about that but then I would have to add a new doc section since the last one is Integral of sin x ^ m * cos x ^ n (maybe Integral of misc. functions?). Another possibility is to leave it where it is and add a docstring to explain why it's there.

[sgouezel]

How do this PR and the next one relate to Archive/AreaOfACircle?

[xroblot]

It is basically the same result and in fact some of the ideas of AreaOfACircle were used in #6907. The main difference is that the fact volume {x : ℝ × ℝ : x.1 ^ 2 + x.2 ^2 < 1 } = NNReal.pi is not explicitly stated in #6907 yet but that's probably going to change, see the discussion there.

[xroblot]

I'd probably move this theorem to the end of the file, rather than putting it between two sections about trig integrals

Yes, I thought about that but then I would have to add a new doc section since the last one is Integral of sin x ^ m * cos x ^ n (maybe Integral of misc. functions?). Another possibility is to leave it where it is and add a docstring to explain why it's there.

In the end, I put the result in a new section at the end of the file.

[jcommelin]

Thanks 🎉 Let's hope that in the future we can golf the proof to a 1-liner using some integration tactic.

bors merge

[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