sInf (Real.toEReal ' ' ...)

Stream: Is there code for X?

[Michael Stoll]

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]

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]

With corollaries for sInf in a ConditionallyCompleteLattice.

[Michael Stoll]

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]

Sounds good! The sooner the better, I'd say

[Michael Stoll]

Does it make sense to PR stuff right now, with the cache not working?

[Yaël Dillies]

If it's working on your end, then luckily you will get green CI on the first go.

[Yaël Dillies]

You can also base yourself off v2024

[Michael Stoll]

How do I upgrade my current master to precisely this version? (I.e., what's the command syntax for git?)

[Yaël Dillies]

git checkout v2024 should do

[Kevin Buzzard]

That doesn't do what Michael asked though

[Michael Stoll]

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]

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]

you may need to git pull first

[Mario Carneiro]

to move master to that commit, checkout master and then (with a clean working directory) git reset v2024 --hard

[Michael Stoll]

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]

I seem to have ended up with a branch called v2024, which is probably not what I should have done.

[Mario Carneiro]

If you are on a branch then you probably want to rebase onto v2024 instead

[Mario Carneiro]

git rebase v2024

[Mario Carneiro]

from your branch

[Mario Carneiro]

and probably delete the v2024 branch

[Michael Stoll]

I switched back to master and deleted the v2024 branch. Do I now do git reset v2024 or something?

[Mario Carneiro]

yes, git reset v2024 --hard from the master branch

[Mario Carneiro]

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]

but it's equivalent to git reset v2024 and then just discard all changes in the working directory

[Michael Stoll]

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]

what does lake exe cache get do?

[Michael Stoll]

produces thousands of lines The requested URL returned error: 403.

[Mario Carneiro]

It is supposed to work on that version, but since about 2024-01-02T05:07:00-05:00 it's been reporting 403 for everyone

[Michael Stoll]

#9404 for the interval lemmas.

[Michael Stoll]

BTW, should the interval lemmas be tagged simp?

[Michael Stoll]

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?