PR summary 9f80e920c7

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ iInf_mul_iInf
+ le_iInf_mul_iInf

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

In le_iInf_mul_iInf and iInf_mul_le_mul_iInf, it seems that the hypotheses (hu_top : ∀ x, u x ≠ ⊤) and (hv_top : ∀ x, v x ≠ ⊤) could use existential quantifiers instead of universal quantifiers. Basically, the idea is that you want to avoid e.g. f infinite everywhere and g converging to 0, in which case H is vacuous but the conclusion is too strong. But existential quantifiers are enough to guarantee that neither f nor g are infinite everywhere.

Is this something you could prove instead?

On a side note: some time ago, we added things like EReal.add_iInf_le_iInf_add. Given that (EReal, +) is isomorphic to (ENNReal, *) through the exponential, you may easily get some similar statements.

Edit: I think this suggestion is worth considering. On the dependent PR, you are proving limsup_mul_le', which is a multiplicative version of EReal.limsup_add_le_add_limsup. You might avoid a lot of work and prove a more general statement that way.

It would also be useful to keep similar names for such statements.

Is this something you could prove instead?

This version is sufficient for my use case, but if you have formalized the more general version I would have no problem changing it.

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Thanks! 🎉
bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style