invpoly.ses sorry

Stream: condensed mathematics

[Kevin Buzzard]

I have been working on a plan to remove the sorry in invpoly.ses; however my plan involves using results in laurent_measures.ses2. I've added import laurent_measures.ses2 to invpoly.ses and it worked, which was a good start. However the running assumptions in invpoly.ses are 0<p<=1 so the results in laurent_measures.ses2 do not apply, as they need p<1 (or equivalently 1/2<r). master compiles right now. But I changed line 20 in invpoly.ses to ... [fact (p<1)] and this breaks the build; I get errors in laurent_measures.ext (which Adam is in the process of editing right now). I tried changing p<=1 to p<1 in that file too (but I'm unclear about whether the p there is my p or p') and got a bunch of errors which look fixable but I need to go and cook dinner right now so this issue is currently unresolved; I'll come back to it in a couple of hours if nobody fixed it before then. I'm hoping this issue isn't serious!

[Kevin Buzzard]

I need a (finite) bound for a function in the proof of short_exact in invpoly/ses.lean and the bound I worked out on paper involves (2 - r⁻¹)⁻¹ which isn't much of a bound if p=1 and thus r=1/2.

[Kevin Buzzard]

I am assuming that the answer is "oh we just need to change a bunch of <= to < and everything will be fine", this feels mathematically like it's what's going to happen, and this is just some random noise because we didn't ever need p<1 until this point in the argument so people just went with p<=1.

[Kevin Buzzard]

https://github.com/leanprover-community/lean-liquid/blob/786e35176a114db02d442dc5cdf7925edd78baff/src/invpoly/ses.lean#L141-L144

[Kevin Buzzard]

OK I've fixed it, problem solved. At least I hope it is -- master compiles with the change. In laurent_measures.ext I now see that the thing which is needed is p' < 1 and we have this because the assumptions are p' < p and p <= 1, so in particular we can leave p<=1 in that file. Sorry for the noise! I just didn't have time to think about it earlier and was slightly worried that this would cause problems.

[Kevin Buzzard]

here are the changes. I think the sorry in invpoly/ses.lean is not fillable unless p < 1 (which it now is) but in the application in laurent_measures/ext.lean we apply it to p' not p, and p' < 1 is deducible from the running hypotheses in that file so no more hypotheses need to be changed.

[Johan Commelin]

Yeah, I think we got p and p' confused again. Sorry for that. And thanks for fixing this.