Following the discussion on lower bounds for 3SAT , I'm wondering what are the main lower bound results formulated as space-time tradeoffs. I'm excluding results such as, say, Savitch's theorem; a good entry would focus on a single problem and its bounds. An example would be :
"Let T and S be the running time and space bound of any SAT algorithm. Then we must have T⋅S≥n2cos(π/7)−o(1) infinitely often." (Given in  by Ryan Williams.)
"SAT cannot be solved simultaneously in n1+0(1) time and n1-ε space for any ε>0 on general random-access nondeterministic Turing machines." (Lance Fortnow in 10.1109/CCC.1997.612300)
Further, I'm including definitions of natural space-time tradeoff complexity classes (excluding circuit classes).