Almost coherence of higher direct images

For a flat proper morphism of finite presentation between schemes with almost coherent structural sheaves (in the sense of Faltings), we prove that the higher direct images of quasi-coherent and almost coherent modules are quasi-coherent and almost coherent. Our proof uses Noetherian approximation, inspired by Kiehl's proof of the pseudo-coherence of higher direct images. Our result allows us to extend Abbes–Gros' proof of Faltings' main $p$-adic comparison theorem in the relative case for projective log-smooth morphisms of schemes to proper ones, and thus also their construction of the relative Hodge–Tate spectral sequence.