Commit 2024-11-01 11:23 7a8a81c7

feat: liminf and limsup add/mul lemmas in Real (#18365) Lemmas such as limsup u f + liminf v f ≤ limsup (u + v) f (and its multiplicative avatars) in (basically) reals. These lemmas had already been done in EReal/ENNReal. The strategy is the same; using reals brings some complexity with the gestion of IsBoundedUnder/IsCoboundedUnder properties. Summary of the modifications:

• In Mathlib/Algebra/Order/Group/DenselyOrdered.lean: proof of le_mul_of_forall_lt and mul_le_of_forall_lt, as well as their additive versions, which are key for the final results on (R, +).
• In Mathlib/Algebra/Order/Field/Basic.lean: proof of le_mul_of_forall_lt' and mul_le_of_forall_lt_of_nonneg, which are key for the final results on (R+, *).
• In Mathlib/Order/LiminfLimsup.lean: four lemmas from IsCobounded.frequently_le to IsCobounded.of_frequently_le are moved to the beginning of the file, so they can be used within. Four new elementary lemmas about IsBoundedUnder which I found quite practical. Four new lemmas about boundedness/coboundedness of sums and products.
• In Mathlib/Topology/Algebra/Order/LiminfLimsup.lean: eight new lemmas about addition/multiplication and limsup/liminfs.