Hölder spaces

Stream: maths

[Floris van Doorn]

Do we already have Hölder spaces in mathlib? @Heather Macbeth claims here that @Yury G. Kudryashov has defined them, but I cannot find them in mathlib. I only found Hölder-continuous functions: docs#HolderWith

[Heather Macbeth]

I think you're probably right, but let's see what Yury says

[Yury G. Kudryashov]

I didn't define the spaces.

[Yury G. Kudryashov]

I was going to do that, then got distracted.

[Yury G. Kudryashov]

If you're going to define them, are you going to use (n, r) as a parameter or an ENNReal (with a norm instance for finite r)?

[Yury G. Kudryashov]

The difference is that C^{2+1} says "C^2 and Lipschitz second derivative" while C^3 is stronger.