-
Notifications
You must be signed in to change notification settings - Fork 11
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix a few minor Lean misformalisations #229
Conversation
The informal solution provided at: https://kskedlaya.org/putnam-archive/2022s.pdf contains some typos. The condition: $$ b < \ln(1 - r_{-})^2 - |a|r_{-} $$ should be: $$ b < \ln(1 + r_{-}^2) - ar_{-} $$ Similarly for the $r_{+}$ case. The argument given in the PDF correctly derives that for $0 < a < 1$ one should have: $$ b < g(r_{-}) $$ where $g(x) = \ln(1 + x ^ 2) - ax$ (and similarly for the $r_{+}$ case. However there are some typos when transcribing this to the headline solution (given higher up).
Nice catch for noticing a mistake. I think the case for the |
Sorry I meant to get back to you about this: will do so tomorrow. |
In fact I believe all is well, though I nearly went mad trying to understand why your plot made things look wrong. I somehow FINALLY realised that in this desmos site, |
In the meantime, I have added three more problems where we have identified misformalisations to this PR. As always, thanks for review and maintenance. |
Whoops! Sorry for causing confusion, I was trying to avoid it with the graph but had the opposite effect. I am now confident in the change. |
This was disprovable because the integral was using the two-dimensional measure from the plane in the integral on the one-dimensional set that is the circle (and thus was always zero). We could fix this by supplying the one-dimensional Hausdorff measure but this is too heavy-weight given that we can just parameterise and use the interval integral. A second error was the inclusion of the typeclasses `[AddCommGroup V] [Module ℝ V]`. The subset already has this algebraic structure and by supplying these there is ambiguity of which structure applies, as well as the fact that these are arbitrary typeclasses with no relation to the ambient structure on `MvPolynomial (Fin 2) ℝ`.
f5290ac
to
76e3114
Compare
This was disprovable because of division-by-zero silliness. The fix is to restate the problem in the language of rational functions.
This was disprovable because `y` could fail to be differentiable at `1`. E.g., one could define `y` such that: `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` for `x ≥ 1` and `y x = 0` for `x < 1`. This will satisfy the RHS of the iff in the goal but not the left. I see two obvious ways to resolve the issue: 1. Demand that `y` is C^n on `[1, ∞)` 2. Require that `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` holds on a neighbourhood of `[1, ∞)` The informal statement is very vague so I have somewhat arbitrarily opted for the first of these resolutions. This was previously "fixed" in 7a92152 but unfortunately an error remained.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Everything looks good to me, thanks for the contribution!
No description provided.