Regarding the addendum: Thank you very much for this observation! Indeed it works for $r$ independent points; and this should yield, as in the paper by Amoroso and David, the truth of the original elliptic Lehmer conjecture for points $P$ such that $\mathbb{Q}(P)/\mathbb{Q}$ is Galois. I wonder if Masser (or someone else) has a similar counting theorem for points of small height on higher dimensional abelian varieties (thus refining his estimate $\hat{h}(P) > cd^{-\kappa}$)?

@ACL: Thanks! I knew about that paper, but I had not looked at it, so I didn't know this question was formulated as a conjecture there. It seems as if there has been no progress on this problem for $r > 1$?

Lang's conjecture demands a uniform $c$, independent of $E$. Here I ask for a $c$ depending on both $E$ and $r$.

Thank you very much for this reference, that was very helpful! That is exactly what I wanted to know. By the way, the reference also indicates that $1/2$ is the critical exponent for which one can prove zero density unconditionally, i.e. without assuming GRH. (They refer to the paper by Pappalardi, where this was shown.)

Thank you very much indeed for all those explanations, and especially for the references!

Thank you very much for those explanations! Thus, the [SUZ] equidist. thm. implies that the lim inf (under Zariski topology) of the height of a totally real point is bounded away from zero; but to get a lower bound over all non-torsion totally real points, you need Ullmo's idea. And to get an effective lower bound on the height of a non-torsion point, you need the David-Philippon analytic geometry approach. However, the bound on the lim inf from [SUZ] is already effective - do I understand this right? Thus, I wondered whether your p-adic equid. thm. would likewise give effective $U$ and $c$.