Had a quick look at it and I can confirm that changing PWM_FREQUENCY in
Arduino/variant.h at ide-1.5.x · arduino/Arduino · GitHub does change the freq. So if you just need the 4k freq it'll work fine. Still, a way to change the freq in the sketch would be preferred.