[Merged by Bors] - Prove that the diameter of a Euclidean ball is twice its radius. by Vilin97 · Pull Request #32824 · leanprover-community/mathlib4

Vilin97 · 2025-12-13T01:14:14Z

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 [email protected] and @Aristotle-Harmonic

github-actions · 2025-12-13T01:15:22Z

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 · 2025-12-13T01:15:32Z

🚨 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 · 2025-12-16T10:28:22Z

@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.

…idean spaces

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 · 2025-12-22T23:11:17Z

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 · 2025-12-22T23:22:16Z

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

maintainer merge

github-actions · 2025-12-22T23:22:31Z

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

sgouezel · 2025-12-24T10:00:01Z

bors r+

@Aristotle-Harmonic

) 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 `aesop`s and using v4.24). Leo Mayer and I restructured and cleaned them up. Co-authored-by: Leo Mayer [email protected] and @Aristotle-Harmonic

mathlib-bors · 2025-12-24T10:57:47Z

Pull request successfully merged into master.

Build succeeded:

@Aristotle-Harmonic

…nprover-community#32824) 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 `aesop`s and using v4.24). Leo Mayer and I restructured and cleaned them up. Co-authored-by: Leo Mayer [email protected] and @Aristotle-Harmonic

@Aristotle-Harmonic

…nprover-community#32824) 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 `aesop`s and using v4.24). Leo Mayer and I restructured and cleaned them up. Co-authored-by: Leo Mayer [email protected] and @Aristotle-Harmonic

Vilin97 added 2 commits December 12, 2025 17:09

Prove that the diameter of a Euclidean ball is twice its radius.

bfa4e36

rename theorem to lemma

8c56554

github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) labels Dec 13, 2025

remove unused argument.

50e9015

Vilin97 requested a review from urkud December 13, 2025 03:04

themathqueen reviewed Dec 13, 2025

View reviewed changes

Comment thread Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean Outdated

themathqueen reviewed Dec 13, 2025

View reviewed changes

Comment thread Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean Outdated

themathqueen reviewed Dec 13, 2025

View reviewed changes

Comment thread Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean Outdated

fix indents and shorten proof.

1fd4658

Vilin97 requested a review from themathqueen December 15, 2025 02:06

Merge branch 'master' into uw-math-ai

bb2aef4

themathqueen reviewed Dec 15, 2025

View reviewed changes

golf

1741505

Vilin97 requested a review from themathqueen December 16, 2025 08:30

fix lemma names

0735cf2

themathqueen reviewed Dec 16, 2025

View reviewed changes

use appropriate namespaces and further golf.

fad7d5b

Vilin97 requested a review from themathqueen December 16, 2025 10:01

themathqueen reviewed Dec 16, 2025

View reviewed changes

more golf

37aee14

j-loreaux reviewed Dec 16, 2025

View reviewed changes

Comment thread Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean Outdated

Comment thread Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean Outdated

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 16, 2025

Vilin97 added 2 commits December 17, 2025 17:24

make the lemmas more general -- about real normed spaces instead eucl…

ad9c181

…idean spaces

remove newline

c29577f

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 17, 2025

change variable name

58838b7

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 18, 2025

Move lemmas to RCLike/Real

2c504e4

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 18, 2025

Move the sphere lemma as well

6140430

Vilin97 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 18, 2025

Vilin97 requested a review from j-loreaux December 21, 2025 10:27

leanprover-community-bot-assistant assigned sgouezel Dec 22, 2025

j-loreaux reviewed Dec 22, 2025

View reviewed changes

Comment thread Mathlib/Analysis/Normed/Module/RCLike/Real.lean Outdated

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 22, 2025

move lemmas to Basic.lean and avoid an additional import.

15794a6

github-actions Bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 22, 2025

fold variable inside the statement

2d0ef01

Vilin97 requested a review from j-loreaux December 22, 2025 23:10

Vilin97 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 22, 2025

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 22, 2025

themathqueen reviewed Dec 23, 2025

View reviewed changes

Comment thread Mathlib/Analysis/Normed/Module/Convex.lean Outdated

format

9d84cbe

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Dec 24, 2025

mathlib-bors Bot changed the title ~~Prove that the diameter of a Euclidean ball is twice its radius.~~ [Merged by Bors] - Prove that the diameter of a Euclidean ball is twice its radius. Dec 24, 2025

mathlib-bors Bot closed this Dec 24, 2025

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 16, 2026

Uh oh!

Conversation

Vilin97 commented Dec 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Co-authored-by: Leo Mayer [email protected] and @Aristotle-Harmonic

Uh oh!

github-actions Bot commented Dec 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 975952b53f

Import changes for modified files

Declarations diff

Uh oh!

github-actions Bot commented Dec 13, 2025

🚨 PR Title Needs Formatting

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vilin97 commented Dec 16, 2025

Uh oh!

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Vilin97 commented Dec 22, 2025

Uh oh!

j-loreaux commented Dec 22, 2025

Uh oh!

github-actions Bot commented Dec 22, 2025

Uh oh!

Uh oh!

sgouezel commented Dec 24, 2025

Uh oh!

mathlib-bors Bot commented Dec 24, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Vilin97 commented Dec 13, 2025 •

edited

Loading

github-actions Bot commented Dec 13, 2025 •

edited

Loading