We report on progress formalizing the basics of Sobolev spaces based on Fourier analysis using tempered distributions. This formalization includes a simple version of the Sobolev embedding theorem and the trace theorem, as well as elementary mapping properties of constant coefficient differential operators. The main challenge in the formalization is to define various objects on different spaces and find the right abstractions and notations to maintain readability and to avoid code duplication.