I've seen a few questions that speculate as to how much current is available from the HDMI socket but I can't find any concrete values. I've gotten away with using a couple of different HDMI to VGA/3.5mm analogue audio converters, but it would be useful to know a definitive value.
Related but unconfirmed reading seems to suggest that the HDMI socket supplies power directly from the 5V rail:
Total speculation: it's reasonably likely that the Raspberry Pi wires the 5V HDMI directly to the Pi's 5V input. If so, the VGA converter will have power equal to 1A minus whatever the Pi uses.
[Using a 1200mA PSU] The Pi grabs 500mA for itself, the HDMI adapter grabs another 200mA, and I intend to connect a 100mA keyboard, yielding a total of 800mA, which should still be in the safe 1A limit the Pi can handle.
Is this right, or is available HDMI current determined by something else? Do values vary between Pi models and, if so, how?