Commit 2024-10-21 08:28 1404d2bd

feat(ENNReal): liminf/limsup/iInf/iSup and multiplication (#17656) This PR adds a few lemmas about multiplication and liminf/limsup/iInf/iSup: mul_iInf_le_iInf_mul, iSup_mul_le_mul_iSup, mul_liminf_le_liminf_mul and three avatars of the latter. The strategy adopted is the same as for similar lemmas in EReal (EReal.add_iInf_le_iInf_add...): we suffer to prove the key result mul_le_of_forall_mul_le, and everything is deduced from there. Note that ENNReal.mul_le_of_forall_mul_le could be deduced much faster from EReal.add_le_of_forall_add_le using the exp (both as an order isomorphism and as a "group" morphism). However, I wanted to avoid importing special functions, which unfortunately leads to a much longer and painful proof. This also generalizes some lemmas in #15373 : limsup_mul_le' therein can be replaced by limsup_mul_le_mul_limsup with some easy plug-and-play; if _root_.Real.limsup_mul_le is still needed, I can write another PR to deal with it (most of the work is already done anyways -- I think I can prove mul_le_of_forall_mul_le in NNReal, and leverage it to simplify the proof in ENNReal).