[Merged by Bors] - refactor: Let positivity handle ENNReal-valued ofNat

[YaelDillies]

The meta code was looking for StrictOrderedSemiring instead of the weaker OrderedSemiring + Nontrivial, which is enough.

From LeanAPAP

---

[github-actions]

PR summary 8d8c7cc2c8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## 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.

[Ruben-VandeVelde]

I might add a test for \le or \ne as well, but I'll leave it to you whether that's useful

[YaelDillies]

No indeed, positivity already takes care of that

[hrmacbeth]

Rather than having a special ENNReal-ofNat positivity extension, I think we should fix the existing positivity extension for numerals to handle this use case. Note that currently

import Mathlib

example : 0 < (2:ENNReal) := by positivity -- fails
example : 0 ≤ (2:ENNReal) := by positivity -- works

The reason is that in the tactic code proving ≤ requires OrderedSemiring (which holds for ENNReal) but proving < requires StrictOrderedSemiring (which does not hold for ENNReal).

@YaelDillies I am sure you are very capable of finding or inventing a typeclass which (i) holds for ENNReal and (ii) implies that positive numerals are positive.

[YaelDillies]

Well, that was easy. For some reason I remembered that Nat.cast_pos had to use StrictOrderedSemiring, but clearly I was wrong and short-memoried since no one else than me generalised Nat.cast_pos back in leanprover-community/mathlib3#16172.

[hrmacbeth]

Could you please add a test like this?

example : (0 : ℝ≥0∞) < 3 - 2 := by positivity

(since the norm_num positivity extension should handle that too.)

[YaelDillies]

It doesn't work. I suspect it's because norm_num doesn't know about truncated subtraction.

Is your "should" meant as in "it should work" or as in "you should make it work"? I think it's pretty out of scope for this PR regardless of your answer.

In fact, my motivation here is to have positivity prove that the L2 norm of a nonzero function is positive, and there I really don't have any truncated subtraction

[hrmacbeth]

I was operating under the mistaken assumption that norm_num reduces (2:ENNReal) - 1 to 1. (It does for Nat but apparently not here.). No action required!

[hrmacbeth]

bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

I will try to make the 3 - 2 example work in another PR. Let's keep this one simple.

bors merge

[YaelDillies]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style