Probabilistic Tits alternative for circle diffeomorphisms

Let \mu_{1} , \mu_{2} be probability measures on \operatorname{Diff}^{1}_{+}(S^{1}) satisfying a suitable moment condition and such that their supports generate discrete groups acting proximally on S^{1} . Let (f^{n}_{\omega})_{n \geq 0} , (f^{n}_{\omega'})_{n \geq 0} be two independent realizations of the random walk driven by \mu_{1} , \mu_{2} , respectively. We show that almost surely there is an N \in \mathbb{N} such that for all n \geq N the elements f^{n}_{\omega} , f^{n}_{\omega'} generate a non-abelian free group. The proof is inspired by the strategy by R. Aoun for linear groups. A weaker (and easier) statement holds for measures supported on \operatorname{Homeo}_{+}(S^{1}) with no moment conditions.