[Merged by Bors] - Prove that the diameter of a Euclidean ball is twice its radius.

[Vilin97]

feat(Analysis/InnerProductSpace/EuclideanDist): prove that the diameter of a sphere and a ball is twice its radius

All lemmas and theorems: Metric.diam_sphere_eq, Metric.diam_closedBall_eq', Metric.diam_ball_eq. Also, fold a variable declaration inside convexHull_sphere_eq_closedBall.

@Aristotle-Harmonic gave the initial version of the proofs (with many aesops and using v4.24). Leo Mayer and I restructured and cleaned them up.

Co-authored-by: Leo Mayer leomayer@uw.edu and @Aristotle-Harmonic

[github-actions]

PR summary 975952b53f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Metric.diam_ball_eq
+ Metric.diam_closedBall_eq
+ Metric.diam_sphere_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"

[themathqueen]

Also, maybe add Aristotle as a co-author since it provided the initial proofs?

[Vilin97]

@themathqueen , just want to say thank you for your review! I learned several things, e.g. that when I the lemma starts with a namespace, it automatically opens it, so I don't have to use Metric. in the proof body.

[j-loreaux]

This review is not intended as criticism or frustration, so please don't read it that way. The only purpose is to inform about matters important to library design (i.e., minimizing use of high-powered theorems to reduce import requirements).

[j-loreaux]

I know you wrote this proof because you think its "simpler", but it's not. The fact is that you've just hit a nail with a wrecking ball; in less colorful language, you have used a high-powered theorem to prove a comparatively trivial fact. Note how the convexHull_sphere_eq_closedBall theorem was rather a lot of work to prove, but the two theorems on which the previous proof relied were relatively easy.

Note also, by using this theorem you are forcing (without someone rewriting the proof) this theorem to stay in this file, whereas the previous proof would have let it live in Analysis/Normed/Module/Basic.lean (so it should probably go there instead).

It's a bit sad even that the ball version has to live in this file because of closure_ball. (EDIT: wait, why did you put these in this file, why not in Analysis/Normed/Module/RCLike/Real.lean? It's possible I'm overlooking something I suppose, as I didn't attempt it myself.)

[Vilin97]

I see, thank you for the explanation. I did not know that we try to avoid using powerful theorems. I reverted to the proof you gave.

Regarding the location, I searched with #find_home! Metric.diam_ball_eq and got

[Mathlib.Analysis.Normed.Module.Convex, Mathlib.Analysis.Normed.Module.Ball.Pointwise, Mathlib.Analysis.SpecialFunctions.Log.Basic, Mathlib.Analysis.Normed.Module.RieszLemma]

I then thought that it makes sense to put it in Convex since the ball is the convex hull of the sphere (maybe not the best reason). I don't claim to have a good understand of the logic behind where lemmas go, I try to just guess based on similarity to other lemmas in the files.

I now moved all three lemmas into Analysis/Normed/Module/RCLike/Real.lean. It did require me to add an additional import.

[Vilin97]

With the new import, I got the scary red large-import tag, which I don't love.
Also, thank you for educating me!

[j-loreaux]

please also add a comment to the PR description explaining why the other code is moving within the file. Arguably that should be a separate PR, but I'm not going to force it.

[Vilin97]

I moved the lemmas, removed the import following your suggestion, and instead of moving the lemma in Convex simply folded the variable in the lemma statement, which results in a smaller change.

[j-loreaux]

I've contributed a lot here, so I won't merge it myself.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Post-Build Step
• Lint style