I must say I'm surprised it can do doubles so fast. Do you have data for division? With division algorithms, you'll need to test a wide range of denominators to get a good feel.
I just tried it with several different denominators & always get a result in the range of 34 microseconds. So floating point division is about 3-4 times slower than multiplication (9 usec).
Even so, that's about 30,000 divisions per second. This seems fast enough for (much) government work! :
BTW, double is supposed to be 8-bytes: http://www.arduino.cc/en/Reference/Double
I don't know why sizeof() would return 4.
I would tend to believe what the compiler is reporting, but I just posted something on this in Bugs/Suggestions, so we will see.