convex hull of spheres

Stream: Is there code for X?

[Filippo A. E. Nuccio]

I was unable to find

theorem convexHull_sphere_eq_closedBall [Nontrivial F] (x : F) {r : ℝ} (hr : 0 ≤ r) :
    convexHull ℝ (sphere x r) = closedBall x r := by

(so I added it to #29033, but I'm happy to remove it if it was already there). The proof is not difficult, but I expected by exact? to work.

[Sébastien Gouëzel]

Do you really need hr?

[Kenny Lau]

what happens if F is trivial?

[Filippo A. E. Nuccio]

The two questions are related, and we don't need hr, while triviality of F gets in the way if r is positive. I don't have much time now, but will minimise the assumptions in the PR soon. In the meantime, I am still curious to see if this is really not already there.

[Anatole Dedecker]

Kenny Lau said:

what happens if F is trivial?

If F is trivial and r is nonzero the sphere is empty but the closed ball isn't.

[Filippo A. E. Nuccio]

Exactly, thanks (I am on mobile this we)

[Etienne Marion]

@loogle convexHull, Metric.closedBall

[loogle]

:shrug: nothing found

[Alex Meiburg]

Is this not a specific instance of a more general idea? That Metric.closedBall is a convex body, and sphere is its frontier, so this is about the convex hull of the boundary of a convex body giving the original body. A form of Krein-Milman

(Maybe you're looking to apply this to cases more generally though.)
Edit: Yeah this more general version should work in the same assumptions as the PR (any NormedSpace ℝ E). Then it's frontier_closedBall or frontier_closedBall' depending on whether you want the Nontrivial or r = 0 case.

[Filippo A. E. Nuccio]

Very nice, thanks!

[Anatole Dedecker]

Alex Meiburg said:

Is this not a specific instance of a more general idea? That Metric.closedBall is a convex body, and sphere is its frontier, so this is about the convex hull of the boundary of a convex body giving the original body. A form of Krein-Milman

(Maybe you're looking to apply this to cases more generally though.)
Edit: Yeah this more general version should work in the same assumptions as the PR (any NormedSpace ℝ E). Then it's frontier_closedBall or frontier_closedBall' depending on whether you want the Nontrivial or r = 0 case.

Coming back to this, I can't see how this would work if the ball is not compact. Am I misunderstanding your definition of "convex body" ?

[Alex Meiburg]

"convex body" is typically defined as "is a compact convex set with non-empty interior"