Approximate a compact by a finite-dimensional compact

Stream: maths

[Yury G. Kudryashov]

What are ther right typeclass assumptions for the following theorem? Let E and F be real topological vector spaces (with some extra assumptions). Let f : E → F be a continuous function, let K be a compact set in E. Then there exists a finite dimensional subspace S in E, a continuous linear projection π : E → S, π ∘ π = π, and a continuous function g : π '' K → F such that f is uniformly close to g ∘ π on K.

#xy: I want to generalize our formalization of the Weierstrass approximation theorem to say that docs#CPolynomialOn functions are dense in C(E, F).

[Yury G. Kudryashov]

... and drop unneeded assumptions in docs#ContinuousMap.dense_setOf_contDiff

[Anatole Dedecker]

Just want to point out #21959 since you're working in this area

[Sébastien Gouëzel]

I wouldn't expect much beyond finite-dimensional spaces, even in Banach spaces. For instance, there is a Banach space E and a compact set K for which there is no continuous linear map with finite-dimensional range which is close to the identity on K. This means that for f = g = id there is no π which satisfies your condition. The keyword here is (failure of the) approximation property, see https://en.wikipedia.org/wiki/Approximation_property

[Yury G. Kudryashov]

Thanks!

[Kevin Buzzard]

In a p-adic Banach space every compact operator is a limit of finite rank operators so you might be ok there!

[Sébastien Gouëzel]

p-adic analysis is too easy, almost a joke :-)

[Yury G. Kudryashov]

So, this is true in Hilbert spaces, finite dimensional spaces, and padics. Should we introduce a type class?

[Sébastien Gouëzel]

I would only introduce typeclasses for properties that people who have thought deeply about this have found interesting and fruitful. So, a typeclass for the approximation property definitely makes sense -- but it's not clear to me if it would really help you for your original question. On the other hand, I don't think we should have a typeclass tailored to your question, though, unless you have convincing applications where the generality really helps you.