What's with equivariant homotopy theory over a compact Lie group? For some reason -- I'm not quite sure why -- I've developed the impression that I'm supposed to "tiptoe" around equivariant homotopy theory over groups that are not finite. Should I?
Let me explain. Please correct me / tell me what I'm missing.


*

*Elmendorff's theorem holds for an arbitrary compact group. So I'm pretty sure at least that there's no disagreement over what the $G$-equivariant categories -- stable and unstable -- should be for an arbitary compact group. Please correct me if I'm wrong here.

*I sometimes get the impression that there are real problems in setting up $G$-equivariant homotopy theory when $G$ is not finite -- for example, all the foundational $\infty$-categorical work of late seems to be done in the finite or profinite case. But I don't know what these problems could possibly be! By (1), it's perfectly clear what the orbit category should be. When stabilizing, the Haar measure should allow the kind of "sums" required to construct transfers. Where's the problem? If it's possible to do motivic equivariant homotopy theory over non-finite algebraic groups, then surely it's possible to work over compact Lie groups!

*It's true that non-discrete Lie groups are inconvenient to model as simplicial groups. Is this really a stumbling block?

*Perhaps people just focus on the groups they actually intend to work with. I don't know many existing or potential applications of equivariant homotopy theory over infinite groups. This is probably just my ignorance, since for that matter I don't know many existing or potential applications even over finite groups. For example in this overflow question I see Kervaire invariant one, the Segal conjecture, Galois descent for $\mathbb{C}$ over $\mathbb{R}$, and the study of spaces with $G$-action. These are all for $G$ finite, except maybe the last one, but it's also the vaguest. The other application that comes to mind is cyclotomic spectra and THH, where $G = S^1$ (but we use a universe with only the proper closed subgroups), which brings me to another confusion:

*THH should admit a genuine $S^1$-equivariant structure, but people tend to just use the cyclotomic part, using only the proper closed subgroups (which are all finite). Is this because (a) we'd like to use the $S^1$ part, but there's no model of it that's reasonable to work with, (b) we wouldn't have any use for the $S^1$ part even if we could get our hands on it (seems unlikely -- shouldn't this correspond to information at the infinite place?), or (c) even if we could get our hands on the $S^1$ part, thinking about it in equivariant terms would be the "wrong" approach, or require additional corrections, or (d) some other reason?
 A: Regarding 2, there is no difficulty in defining $G$-spectra in the setting of $\infty$-categories. The only complications I can think of are that (1) the orbit category $\mathrm{Orb}^G$ is now an $\infty$-category and (2) the stabilization process necessarily involves infinitely many representation spheres. Nevertheless, the $\infty$-category of $G$-spaces $\mathrm{Spc}^G$ can still be defined either as presheaves on $\mathrm{Orb}^G$ or by formally inverting the homotopy equivalences in the category of $G$-CW-complexes, and $\mathrm{Spc}^G_*\to\mathrm{Spt}^G$ is still the universal symmetric monoidal colimit-preserving functor that sends representation spheres to invertible objects.
However, there is a difficulty in defining $G$-spectra as spectral Mackey functors, because the transfers are dimension-shifting and so cannot be encoded in a simple $2$-category of spans.
Regarding 3, it is not clear to me that the orbit $\infty$-category $\mathrm{Orb}^G$ can be reconstructed from the simplicial group $\mathrm{Sing}(G)$ (one would also need the orbits $\mathrm{Sing}(G/H)$).
Regarding 5, I believe the answer is (d): THH should not be considered as a genuine $S^1$-spectrum (even though it can be in many ways). This becomes clear when the cyclotomic structure on THH is understood in terms of factorization homology: there is nothing in factorization homology that would induce a genuine $S^1$-equivariant structure on THH.
