Probabilistic Tits alternative for circle diffeomorphisms

Let $\mu_1, \mu_2$ be probability measures on $\mathrm{Diff}^1_+(S^1)$ satisfying a suitable moment condition and such that their supports genererate discrete groups acting proximally on $S^1$. Let $(f^n_\omega)_{n \in \mathbb{N}}, (f^n_{\omega'})_{n \in \mathbb{N}}$ 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 nonabelian free group. The proof is inspired by the strategy by R. Aoun for linear groups and uses work of A. Gorodetski, V. Kleptsyn and G. Monakov, and of P. Barrientos and D. Malicet. A weaker (and easier) statement holds for measures supported on $\mathrm{Homeo}_+(S^1)$ with no moment conditions.