In the comments on EDP18 we are considering a certain decomposition problem that can be understood in its own right. At various points I have asserted that if we can find a decomposition of a particular kind then we will have a positive solution to EDP. And at various points in the past I have even sketched proofs of this. But I think it would be a good idea to do more than merely sketch a proof. So in this post I shall (I hope) give a completely rigorous derivation of EDP from the existence of an appropriate decomposition. (Well, I may be slightly sketchy in places, but only about details where it is obvious that they can be made precise.) I shall also review some material from earlier posts and comments, rather than giving links.
Representing diagonal matrices
First, let me briefly look again at how the ROD (representation of diagonal) approach works. If and are HAPs, I shall write for the matrix such that if and 0 otherwise. The main thing we need to know about is that for every
Suppose now that is a diagonal matrix with diagonal entries and that we can write it as where each and each is a HAP. Then
If and for every then it follows that there exists such that
and from that it follows that there is a HAP such that So if we can make arbitrarily small, then EDP is proved.