On the stability of the overconvergence under the direct image by a proper smooth morphism

Up to a translation in the language of arithmetic $\text{D}$-modules, we prove a conjecture of Berthelot on the preservation of the overconvergence under the direct image by a smooth proper morphism of varieties over a perfect field of characteristic $p>0$.