Now that I am almost done with my dissertation, I have decided to switch focus and concentrate on doing math that can be formally checked by the Lean Theorem Prover. The ideal sub-field of math for me to start formalizing would be Teichüller theory, and results on mapping class groups …

I have of late begun using Things as a planner app on my mobile devices, to supplement the usage of Orgmode on my computers. Ideally I would have liked to use an Orgmode based app on my mobile devices, and beorg seemed like a fairly good choice. However, I wanted …

An observation I made a while ago while peeking over people's shoulders (with their consent, of course) is that even when they're writing TeX in a powerful text editor, like Emacs or Vim, most people don't really harness the extensive programmability of their text editor (especially MM¹). For instance …

Another 9 months have gone by without a blog post, and this time I don't even have lack of time as an excuse my lack of writing. This summer turned out to be quite different from what I had planned, which probably goes to show one shouldn't plan too far …

In the previous post, we proved Sullivan's shadow lemma, which gave us concrete estimates for special subsets of the boundary, namely shadows. Recall that the shadow of a ball of radius \(r\) based at \(y\), with the source at \(x\), denoted by \(\mathcal{O}_r(x, y)\), is the set …

In the previous post, we saw how to get an asymptotic count of orbit points under a lattice action, i.e. a finite covolume Fuchsian group. To do so, we needed the fact that the geodesic flow on the associated quotient was mixing with respect to the Liouville measure. That …