[`Analysis/MeanInequalities`] Fill in API

[SnirBroshi]

• Strict versions of HM-GM / Hölder's / Minkowski's
• NNReal/ENNReal are missing a lot of stuff that Reals have in this file, such as strict AM-GM
• EReal has nothing in this file, but should probably have AM-GM / HM-GM / Young's / Hölder's / Minkowski's

Figure out what the discrepancies are and fill them in.

Also in Analysis/MeanInequalitiesPow.lean, add strict versions of {Real,NNReal,ENNReal}.add_rpow_le_rpow_add for 0 < a 0 < b 1 < p.