Lemmas re-exported from Mathlib (formerly PR31960)

The toSphereBallBound definitions and their key estimates that this file used to provide have since been upstreamed to Mathlib. This module re-exports them via the relevant Mathlib import so existing import sites continue to resolve.