Archive results added to Mathlib

Stream: general

[Xavier Roblot]

The PR #6907 (ready for review :grinning_face_with_smiling_eyes: ) proves the formula for the area of a circle. This result has been proved already in Lean and is part of the Archive, see AreaOfACircle (and in fact #6907 uses some ideas from this proof). In the PR, there is a discussion about what to do about the Archive result (and the entry in the 100 theorems list that links to it) when this PR is merged. Should we keep the Archive result as such, or should we delete it and update the link to point to the result in Mathlib? Or maybe some other options...

I think it is worth having a discussion here before making a decision.

[Yaël Dillies]

I think it's fine to remove the archive result if mathlib acquires a more general result.

[Eric Wieser]

Arguably the truly analogous result is the one about the area of discs in WithLp 2 (ℝ × ℝ), which needs #6136

[Eric Wieser]

Perhaps we should keep the file AreaOfACircle, and have it contain aliases for all three of:

• Area of a circle in the complex numbers
• Area of a circle in EuclideanSpace
• Area of a circle in WithLp 2 (ℝ × ℝ) (to be added later)

[Kevin Buzzard]

Area of a circle in the "unoriented complexes", any algebraic closure of the reals

[Yury G. Kudryashov]

Can we have it in a 2-dimensional inner product space?

[Yury G. Kudryashov]

Or better have a formula for the volume of a ball in n-dimensional inner product space.

[Yaël Dillies]

If anyone gets to doing that, the best formulas I know for the volume and surface of a ball are equations (32) and (33) from the Tau Manifesto.

[Yaël Dillies]

They involve no case splitting between even and odd n, and are written in terms of π/2 and the double factorial.

[Kevin Buzzard]

We have the gamma function so why not just use that :-)

[Yaël Dillies]

Because it's non-elementary and over-powered here?

[Kevin Buzzard]

Use Gamma and prove the results relating special values to double factorials then

[Yaël Dillies]

You know that the volume calculation is naturally inductive (with a step of 2) and shows that V_{n + 2} = 2 * pi / (n + 2) * V_n? I don't see how to justify dragging an import as huge as the Gamma function to encode such a simple relation. You aren't going to use $\frac 4 3$-dimensional spheres (if that is even a thing), are you?

[Antoine Chambert-Loir]

The Beta/Gamma relation is a really fundamental result in analysis. It has to belong to Mathlib.

[Yaël Dillies]

Sure, I'm just saying it should not be imported where a simple two-step recurrence relation suffices.

[Sebastien Gouezel]

There is a direct non-inductive volume calculation, where the volumes comes out directly in terms of the Gamma function.

[Sebastien Gouezel]

(search for "Gaussian integrals" in https://en.wikipedia.org/wiki/Volume_of_an_n-ball)

[Eric Wieser]

I'm pretty sure @Floris van Doorn said they already had the n-ball result ready

[Floris van Doorn]

Yes, @Heather Macbeth and I proved it on a branch. We will start PR-ing this (somewhat) soon:
https://github.com/leanprover-community/mathlib4/blob/marginal/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeBall.lean#L367
Our current result is formulated for ι → ℝ, and we indeed defined the Beta function for this:

def Real.Beta (a b : ℝ) : ℝ := Gamma a * Gamma b / Gamma (a + b)