Functional Analysis with Compact Integral Operators

Stream: Is there code for X?

[Sayantan Majumdar]

I need to proove a few Integral Operators are Compact and I am having some trouble, I probably made a mistake somewhere. Are compact sets, integral operators and compact operators implemented in mathlib and lean4 already?

[Moritz Doll]

docs#IsCompactOperator and docs#IsCompact, I don't think that we have integral operators, would be an easy thing to add.

[Sayantan Majumdar]

Thanks a lot. I checked that docs page many times but dont know why I missed it.