mathlib

d9eed422 - feat(analysis/liouville/inequalities_and_series): two useful inequalities for Liouville (#8001)

feat(analysis/liouville/inequalities_and_series): two useful inequalities for Liouville (#8001) This PR ~~creates a file with~~ proves two very specific inequalities. They will be useful for the Liouville PR, showing that transcendental Liouville numbers exist. After the initial code review, I scattered an initial segment of this PR into mathlib. What is left might only be useful in the context of proving the transcendence of Liouville's constants. ~~Given the shortness of this file, I may move it into the main `liouville_constant`, after PR #8020 is merged.~~