[Merged by Bors] - feat: Miscellaneous small ENNReal lemmas.#13938
[Merged by Bors] - feat: Miscellaneous small ENNReal lemmas.#13938
Conversation
PR summary 326e10bcf0Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| rfl | ||
|
|
||
| /-- If `xs : ι → ℝ≥0∞` is bounded, then we have `liminf (toNNReal ∘ xs) = toNNReal (liminf xs)`. -/ | ||
| lemma liminf_toNNReal_eq {b : ℝ≥0∞} (b_ne_top : b ≠ ∞) |
There was a problem hiding this comment.
Isn't it enough to assume the weaker condition that xs i is eventually not equal to ∞? If the liminf is infinity in this case, it means that the sequence is tending to infinity, so the liminf in NNReal is probably zero (what other choice of junk value could we have? I haven't checked).
There was a problem hiding this comment.
True. The existing lemma Monotone.map_liminf_of_continuousAt used here had suboptimal assumptions, so it looks like the right course is to generalize that first. I made PR #14591 for the generalization. With it, I will return and generalize this lemma (and liminf_toReal_eq above, which inherited a similar suboptimal assumption).
Actually, I belatedly realized that your observation was stronger than the general generalization it made me think of. In the ENNReal case the junk value choice should allow for an even weaker assumption than coboundedness. I will therefore think about fixing the ENNReal-lemmas independently of the generalization in the other PR, which I nevertheless still think is fixing suboptimal generality elsewhere. [UPDATE: The requested generalization ended up depending on the other PR's generalization in any case.]
There was a problem hiding this comment.
I moved the generalization of this lemma and the ones below to #15115. (Unfortunately I missed that these are not completely independent: the new PR still depends on one lemma in the current simple PR. I still think the division makes the PRs clearer that way.)
…map limsup lemmas
…nificantly changed.
Mathlib/Data/ENNReal/Basic.lean
Outdated
| @[simp] theorem toReal_nonneg {a : ℝ≥0∞} : 0 ≤ a.toReal := a.toNNReal.2 | ||
|
|
||
| @[simp] theorem toNNReal_toReal_eq (z : ℝ≥0∞) : z.toReal.toNNReal = z.toNNReal := by | ||
| ext; simp only [Real.coe_toNNReal', ge_iff_le, toReal_nonneg, max_eq_left]; rfl |
There was a problem hiding this comment.
Why do you need the rfl here? Missing lemmas?
There was a problem hiding this comment.
The goal after this simp only [...], before rfl, was essentially the following lemma, which is true by rfl but indeed seemed to be missing. However, creating it and making it a @[simp] lemma causes a loop in a simp later, so maybe there is a reason... On the other hand, the RHS below should definitely in my opinion be the simp normal form of this expression!
theorem coe_toNNReal_eq_toReal (z : ℝ≥0∞) : (z.toNNReal : ℝ) = z.toReal := rfl
I added it now without @[simp] tag, and providing this to simp now avoids the last rfl.
j-loreaux
left a comment
There was a problem hiding this comment.
Assuming the norm_cast suggestion works and you implement the other suggestions:
bors d+
|
✌️ kkytola can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
…ommunity/mathlib4 into kkytola/misc_ENNReal_lemmas
|
bors r+ |
`ENNReal.*`: `.toNNReal_toReal_eq`, `.sub_add_eq_add_sub`, `.zpow_neg`, `.zpow_sub`, `.tendsto_pow_atTop_nhds_top` + instance `MeasurableSMul₂ ℝ≥0 ℝ≥0∞` Co-authored-by: kkytola <“kalle.kytola@aalto.fi”> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
`ENNReal.*`: `.toNNReal_toReal_eq`, `.sub_add_eq_add_sub`, `.zpow_neg`, `.zpow_sub`, `.tendsto_pow_atTop_nhds_top` + instance `MeasurableSMul₂ ℝ≥0 ℝ≥0∞` Co-authored-by: kkytola <“kalle.kytola@aalto.fi”> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
`ENNReal.*`: `.toNNReal_toReal_eq`, `.sub_add_eq_add_sub`, `.zpow_neg`, `.zpow_sub`, `.tendsto_pow_atTop_nhds_top` + instance `MeasurableSMul₂ ℝ≥0 ℝ≥0∞` Co-authored-by: kkytola <“kalle.kytola@aalto.fi”> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
`ENNReal.*`: `.toNNReal_toReal_eq`, `.sub_add_eq_add_sub`, `.zpow_neg`, `.zpow_sub`, `.tendsto_pow_atTop_nhds_top` + instance `MeasurableSMul₂ ℝ≥0 ℝ≥0∞` Co-authored-by: kkytola <“kalle.kytola@aalto.fi”> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
ENNReal.*:.toNNReal_toReal_eq,.sub_add_eq_add_sub,.zpow_neg,.zpow_sub,.tendsto_pow_atTop_nhds_top+ instanceMeasurableSMul₂ ℝ≥0 ℝ≥0∞