Infinite diameter

Stream: Brownian motion

[Markus Himmel]

@Rémy Degenne, I'm currently looking at integral_sup_rpow_edist_cover_rescale with a friend and we're wondering about the case $\varepsilon_0 = \infty$, which corresponds to $\operatorname{diam}T = \infty$ in the later applications. With the current Lean phrasing of the lemma, we would set $m=0$ due to how the junk values work out, which breaks the first line of the proof and we're not sure how to fix it.

[Rémy Degenne]

We will assume finite diameter for $T$. That's also implied by the bounded covering number hypothesis that we put on T.
So if $\varepsilon_0 = \infty$ is problematic, simply add a hypothesis to exclude it.