Fix a few minor Lean misformalisations #210

This was disprovable because the key predicate did not quantify over all groups (and the goal was false even for the trivial group).

The original form was disprovable because of quantifier confusion (e.g., taking `x` and `y` to be non-zero and constant gave a contradiction).

This was disprovable because the argument `ha : SDiff (Finset a)` allowed the user to fill in any function for the set difference function. So for example by providing a dummy set difference function that just always returned the empty set, the goal was false. Presumably this error arose because the original formaliser found that they could not use the existing set difference function out of the box. The right fix is either to put `open Classical` before the proof or to add the typeclass argument `[DecidableEq a]`. In the end I have provided rewrite since the original formalisation is a bit more complicated than it needs to be.

This was disprovable because it did not restrict `x` and `y` to the positive quadrant. The informal statement is quite sloppy in this same sense (presumably because non-integral powers of negative reals are not defined). I have also proposed changing the implementation of "tangent to the curve" since a priori a line could intersect a degree `m` curve in up to `m` points so the naive set-counting definition is arguably too strong.

This was disprovable because the hypothesis `apos : a > 0` means that `0 ≤ a n` for all `n` and there exists some `n` such that `0 < a n`. (So the sequence: 1, 0, 0, 0, 0, ... was admissible and provided a counter example to the statement.)

This was previously "fixed" in c75c0b0 but unfortunately an error remained.

This was disprovable because of a minor Mathlib footgun: namely the limsup of a real-valued function which is not bounded above is zero.

This was disprovable because the zero function was excluded from the solution set. The fix is to replace `a > 0` with `a ≥ 0` in the solution. Other changes are just style. There is incidentally a sharper version of this question which requires establishing which solutions correspond to functions with finite / infinite domain. However this is not actually asked.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix a few minor Lean misformalisations #210

Fix a few minor Lean misformalisations #210

Commits on Sep 9, 2024