Formalizing Jung's theorem and minimal bounding spheres

Stream: maths

[Julien Michel]

Hi all, I've formalized Jung's theorem here over the last few weeks. It is in the 1000's theorems unformalized list, so I'm assuming it would be of interest to mathlib.
As I've never contributed to mathlib, I would be happy to have some general feedback about my code, to adress any major issues before thinking of making PR's to mathlib.

Note that after some restructuring and simplifications, I ended up creating a few API's such as:

noncomputable def supEDist {α} [EDist α] (X : Set α) c := sSup {edist s c | s ∈ X}

noncomputable def supDist (X : Set α) c := (supEDist X c).toReal

noncomputable def BoundingSphere.radius (X : Set α) := sInf (Set.range (supDist X))

I couldn't find any preexisting work about those, but please let me know if I'm reinventing the wheel.
Most of the proof lies in a BoundingSphere namespace, where I develop some basic theory about minimal bounding spheres. Most properties are expressed on the radius and center of a minimal bounding sphere. (Again I did not find anything in mathlib about this but let me know if I'm wrong).

Jung's theorem is at the bottom and expressed as an inequality on the radius.
My formalization is based on this blog post
Any feedback appreciated!

[Julien Michel]

I realized there is already EMetric.infEdist and Metric.infDist in this mathlib file.
I suppose I will first imitate that file and define EMetric.supEdist and Metric.supDist in a similar way, and then will start submitting PR's.

Could a maintainer tell me if adding to mathlib the theory of minimal bounding spheres in euclidean spaces seems reasonable ?

I am not aware of more general settings but I suppose that the existence or uniqueness of the sphere wouldn't be always granted, so a euclidean space seems like a simpler setting where one can directly talk about the center and radius of such spheres.

Note that I'm not an expert on the topic, but since I got familiar with it while working on Jung's theorem, I'm definitely interested in contributing to that.

Thanks for comments or suggestions!

[Yaël Dillies]

Aren't they docs#Metric.diam and docs#EMetric.diam? (btw the latter name is terrible because infinite diameter sets are a thing even in metric spaces)

[Julien Michel]

I don't think so. diam is the sup distance between any two points in a set. I want the sup distance between a fixed point and the set

[Aaron Liu]

Yaël Dillies said:

(btw the latter name is terrible because infinite diameter sets are a thing even in metric spaces)

Should that be something like Metric.ediam? And I feel like Metric.diam wouldn't not be useful in emetric spaces too.

[Yaël Dillies]

Yes, exactly. I personally think that the EMetric namespace should be used only for concepts that bear no relevance outside of extended metric spaces

[Julien Michel]

Hi all, here are some updates. This week, I’ve worked on improving the code quality and bringing it closer to Mathlib’s standards and conventions. I’ve split it into three files:

SupDistance.lean containing sup distance theory in pseudo (e)metric spaces.
Basic.lean containing minimal bounding sphere theory in a Euclidean affine space.
Jung.lean containg Jung’s theorem in a Euclidean space.
I think SupDistance.lean is mostly ready for PR’s so I might start doing that next week.

A few questions:
1)
To model a Euclidean affine space setting in Basic.lean I’m using the following typeclasses:

variable {V} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
variable {P} [MetricSpace P] [NormedAddTorsor V P]

Where V represents the vector type, and P represents the point type.
I’d like to confirm: Is this a valid way to represent Euclidean affine spaces?
2)
In Jung.lean, I ended up working in a Euclidean space instead

variable {V} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]

The reason for this less general approach is that I need to define and use a lemma on convex hulls which appear to be only available in a regular vector space. Is there anything like convexHull in an affine space setting?
Thanks!