Fix a few minor Lean misformalisations #206
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The hypothesis `hxprod` implied `False` because the infinite product does not converge if `1 < x`. The fix is to change `x ≥ 0` to `x ∈ Set.Ioo 0 1`. The other changes are just stylistic.
The second hypothesis named `hf` implied `False` because the terms in the sum referenced `n` (which is constant inside the sum) instead of `i`. Also both hypotheses were named `hf` so one was shadowing the other. We fix the above and also include some mild stylistic improvements.
The hypothesis `hanpoly` implied `False` because it did not require the input sequence `a` to take non-zero values but it declared the resulting polynomial always had degree `n` for each natural `n`. I believe it would be sufficient to add the clause `(∀ i, a i ≠ 0) →` to `hanpoly` but I believe the rewrite proposed is slightly preferable.
The `hpdigalt` implied false because the `=` operator was binding before the `∧` and so it was equivalent to: ``` ∀ pdig : List ℕ, (pdigalt pdig = Odd pdig.length) ∧ (∀ i : Fin pdig.length, pdig.get i = if Even (i : ℕ) then 1 else 0) ``` meaning that it stated _any_ list alternated `1, 0, 1, 0, ...` (not just those satisfying the `pdigalt` predicate). This could be resolved by adding parentheses but it is slightly more idiomatic to use `↔` for propositions (and this does have the right precedence relative to `∧`). Additionally the type of `putnam_1989_a1_solution` should be `ℕ∞` rather than `ℕ` since the question does not reveal whether the set of such primes is finite. Some other minor style tweaks also included.
This is false if the degree is zero since then `g` is zero (and so evaluates to zero everywhere). The fix is thus to add the hypothesis `(hn : 0 < n)`. To some extent this is the fault of the informal question which should highlight this.
Before these changes `hagt` implies `False` because `=` binds before `∧` and so `(hagt a).2` is asserted for any `a`. This could be fixed by adding parentheses but it is more idiomatic to use `↔` rather than `=` for propositions and this has the right precedence relative to `∧`. We make this substitution of `↔` also in `hbg1` and `hbg2` for consistency. Additionally, even after the fix above, `hagt` prevents length-1 partitions because in this case it reads `a 0 > a 0`. We fix this by adding a guard for the length. In fact this question would probably be much simpler if written using the language of `List`s (and possibly `Nat.Partition`) but I have avoided a complete rewrite to ease the review burden.
Without these changes `horder` implies `False` because it allows `i = j` and so for example says that `L 0` is in the interior of the convex hull. A better way to state that the points are the ordered vertices of a convex polygon would be to replace `horder` with something like: `∀ i j k, i < j → j < k → (∡ (L i) (L j) (L k)).sign = 1)` However there are some missing instances that make it difficult to use angles here.
The theorem is false without these changes because `Nat` subtraction means that `k - 2 * j` will evaluate to `0` when `j` is large and so we will pick up a coefficient of `1` instead of `0`. Some minor stylistic changes also included.
The original statement was false because it contained an off-by-one error. Specificially it concerned the numbers 0, 1, ..., n - 1 instead of the numbers 1, 2, ..., n. Using `Finset.Icc 1 n` instead of `Fin n` fixes this. Two other changes are made as points of style: * We do not use the topological sum `tsum` (with notation `∑'`) since we have finite sums. * We use `IsGreatest` to state the goal
Mathlib's `tsum` (with notation `∑'`) gives the wrong answer for conditionally-convergent sums (unless they happen to sum to zero) and so is not the right tool in this question. This is an unfortunate footgun and gap in Mathlib. The fix is to make a basic limit statement about the sequence of partial sums.
|
@GeorgeTsoukalas Should I continue to PR corrections like the ones in this PR and its predecessor ? I appreciate these are not easy changes to review. As an open source maintainer myself, I am well aware of the burden of review so I won't mind if you indicate that now is not the time to send such fixes. OTOH if now is the time, I can probably add another 10 this week. |
Please do! As I mentioned in #203, I have been travelling (and arrived very recently) and with the semester starting soon the team is occupied with other things. My plan yesterday was to review this PR today. Feel free to add corrections as you please, we will get to it when able (for the foreseeable future, this should be without significant delay). |
GeorgeTsoukalas
approved these changes
Aug 28, 2024
GeorgeTsoukalas
approved these changes
Aug 28, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.