I temporarily retract that claim, I made a mistake in my measurements. I’ll do them again tomorrow morning.
EDIT: Rendering times with 16 samples/pixel and 1 pass:
- 8192x4096 HDR map: 94 seconds, out of which almost 6 seconds are spent building the HDR sampling structure, which is a fixed cost and should be excluded, so about 88 seconds
- 512x256 HDR map: 82 seconds
To conclude, the resolution of the HDR map has a rather small impact on rendering times.