Zulip Chat Archive
Stream: Is there code for X?
Topic: sInf (Real.toEReal ' ' ...)
Michael Stoll (Jan 01 2024 at 22:43):
How do I prove the following in a simple way?
import Mathlib.Data.Real.EReal
example: sInf (Real.toEReal '' {x | 1 < x}) = 1 := sorry
Yury G. Kudryashov (Jan 01 2024 at 22:57):
I think that you will need to prove
-- Not sure if true with weaker TC assumptions
lemma IsGLB.image {α β : Type*} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {x : α}
(hsx : IsGLB s x) (hf : Monotone f) (hf' : OrdConnected (range f)) : IsGLB (f '' s) (f x)
Yury G. Kudryashov (Jan 01 2024 at 22:58):
With corollaries for sInf
in a ConditionallyCompleteLattice
.
Michael Stoll (Jan 02 2024 at 13:06):
I have solved my problem as follows.
import Mathlib.Data.Real.EReal
lemma EReal.Ioi_ofReal {x : ℝ} : Real.toEReal '' Set.Ioi x = Set.Ioo ↑x ⊤ := by
refine (Set.image_comp WithBot.some WithTop.some _).trans ?_
rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]
rfl
example: sInf (Real.toEReal '' {x | 1 < x}) = 1 := by
simpa only [Set.Ioi_def, EReal.Ioi_ofReal, EReal.coe_one] using csInf_Ioo <| EReal.coe_lt_top _
I think I will (eventually) add EReal.Ioi_ofReal
together with the seven other similar lemmas to one of the preparatory PRs for the extension of the L-series material. (Unless there are objections...)
Ruben Van de Velde (Jan 02 2024 at 13:07):
Sounds good! The sooner the better, I'd say
Michael Stoll (Jan 02 2024 at 13:07):
Does it make sense to PR stuff right now, with the cache not working?
Yaël Dillies (Jan 02 2024 at 13:09):
If it's working on your end, then luckily you will get green CI on the first go.
Yaël Dillies (Jan 02 2024 at 13:09):
You can also base yourself off v2024
Michael Stoll (Jan 02 2024 at 13:10):
How do I upgrade my current master
to precisely this version? (I.e., what's the command syntax for git
?)
Yaël Dillies (Jan 02 2024 at 13:11):
git checkout v2024
should do
Kevin Buzzard (Jan 02 2024 at 13:13):
That doesn't do what Michael asked though
Michael Stoll (Jan 02 2024 at 13:13):
This gives me an error (something like "path specification 'v2024' is not known to git" [paraphrasing and translating from the German locale...]).
Yaël Dillies (Jan 02 2024 at 13:14):
I don't know the git command but you can click on the branch name in the bottom left of vscode and find it there.
Mario Carneiro (Jan 02 2024 at 13:15):
you may need to git pull first
Mario Carneiro (Jan 02 2024 at 13:17):
to move master to that commit, checkout master and then (with a clean working directory) git reset v2024 --hard
Michael Stoll (Jan 02 2024 at 13:20):
I still have a branch (for the PR on bounds on the complex log, which is slowly rotting) in my mathlib
directory. If I do git reset v2024 --hard
there, will this be a problem?
Michael Stoll (Jan 02 2024 at 13:22):
I seem to have ended up with a branch called v2024
, which is probably not what I should have done.
Mario Carneiro (Jan 02 2024 at 13:25):
If you are on a branch then you probably want to rebase onto v2024
instead
Mario Carneiro (Jan 02 2024 at 13:25):
git rebase v2024
Mario Carneiro (Jan 02 2024 at 13:25):
from your branch
Mario Carneiro (Jan 02 2024 at 13:26):
and probably delete the v2024
branch
Michael Stoll (Jan 02 2024 at 13:28):
I switched back to master
and deleted the v2024
branch. Do I now do git reset v2024
or something?
Mario Carneiro (Jan 02 2024 at 13:37):
yes, git reset v2024 --hard
from the master branch
Mario Carneiro (Jan 02 2024 at 13:38):
if you don't use --hard
it will keep your working tree the same, meaning that you will end up with hundreds of dirty files from all the changes in master since v2024
Mario Carneiro (Jan 02 2024 at 13:39):
but it's equivalent to git reset v2024
and then just discard all changes in the working directory
Michael Stoll (Jan 02 2024 at 13:39):
Did this, but then lake exe cache get
does not work (which is unsurprising, I guess). And lake build
starts building a lot of stuff...
Mario Carneiro (Jan 02 2024 at 13:40):
what does lake exe cache get
do?
Michael Stoll (Jan 02 2024 at 13:40):
produces thousands of lines The requested URL returned error: 403
.
Mario Carneiro (Jan 02 2024 at 13:40):
It is supposed to work on that version, but since about it's been reporting 403 for everyone
Michael Stoll (Jan 02 2024 at 18:12):
#9404 for the interval lemmas.
Michael Stoll (Jan 02 2024 at 18:19):
BTW, should the interval lemmas be tagged simp
?
Michael Stoll (Jan 02 2024 at 18:23):
Now CI fails at the "get cache" stage and doesn't even try to build Mathlib after that (even though I branched off the v2024
Mathlib)...
So I assume it does not make much sense to PR stuff until the cache problem is solved?
Last updated: May 02 2025 at 03:31 UTC