Coverings and chainings

Stream: Brownian motion

[Sébastien Gouëzel]

I just want to mention that we already have in mathlib a discussion of minimal covering by balls, in the files on topological entropy made by @Damien Thomine (see for instance docs#Dynamics.coverMincard). The language is probably too different so that the results can't be reused directly, but maybe there is something to be learned from the way he developed the API.

[Rémy Degenne]

Thanks! I did not know about that part of the library. I'll have a look.

[Damien Thomine]

There is alse some work by Yaël Dillies (see e.g. MetricSeparated). He is currently working on putting the metric and dynamical notions on a common framework, but I don't know when this will be available, so it's probably best to ignore this part for now.

The files on dynamical systems lack anything about chaining (which is one of their weaknesses) so I don't think they will be much help on this point.