Using some results from classical differential geometry, I will collect a wish list of necessary analytical results. I will also explore which of these already exist within Mathlib, which are close, and speculate on how we might approach those that are not.