Green functions and higher Deligne--Lusztig characters

We give a generalisation of the character formula of Deligne--Lusztig representations from the finite field case to the truncated formal power series case. Motivated by this generalisation, we give a definition of Green functions for these local rings, and we prove some basic properties along the lines of the finite field case, like a summation formula. Among the applications we show that the higher Deligne--Lusztig characters and G\'erardin's characters agree at regular semisimple elements. We also derive a generalisation of Braverman and Kazhdan's result on gamma functions for Deligne--Lusztig characters, with a more elementary argument.