Definition pcmIntegerEncodeUnsigned
  (depth     : nat)
  (amplitude : R)
: R :=
  let s : R := Rplus (Rdiv amplitude 2%R) 0.5%R in
    Rmult s (pow 2 depth).
