Definable normal measures

A normal measure U on a measurable cardinal κ   cannot be definable over H(κ+)H(κ+), as otherwise it would belong to its own ultrapower. In this article we show that it may however be Δ1Δ1 definable over H(κ++)H(κ++) when the GCH fails at κ. In [7] it is shown that there can be a unique normal measure on κ when the GCH fails at κ  ; we show here that this unique normal measure can in addition be Δ1Δ1 definable over H(κ++)H(κ++).