# Lower Bounds for Size of Independent Set in a Graph?

I recently learnt that for any instance of a k-SAT problem with $m$ clauses and $n$ literals , we have an assignment of literals such that at least $m(1 - 2^{-k})$ clauses are satisfied.

I was wondering if we can we show a (non trivial) lower bound of the kind that any graph $G = (V,E)$ has an independent set of size $S$ where $S$ is some function in the number of vertices and edges or the like?

Since in the optimisation version we try to find a maximum independent subset, the tighter the lower bound, the better. Hence I was wondering if there is such a lower bound exists, how tight can we make it?

The relevant result is known as Turán's theorem. It states that if a graph has less than (roughly) $n(n-1)/(2r)$ edges then it has an independent set of size $r+1$, and this is tight.
There is also an algorithmic kind of result. Given an $n$-vertex planar graph $G=(V,E),$ one can compute in linear time an independent set of vertices of degree less than $12$ whose size is at least $\left\lceil\frac{n}{24}\right\rceil.$ See e.g. Das, Goodrich, On the complexity of optimization problems for 3-dimensional convex polyhedra and decision trees