Fix a misformalization of putnam_2022_b1 #227
Conversation
This falsely stated that exp had a finite polynomial expansion. This also cleans up the spelling of "with integer coefficients".
| (Pconst : P.coeff 0 = 0) | ||
| (Pdegree : P.degree = n) | ||
| (Podd : Odd (P.coeff 1)) | ||
| (hB : ∀ x : ℝ, HasSum (fun i => b i * x ^ i) (Real.exp (aeval x P))) : |
There was a problem hiding this comment.
I think there might be a preferred spelling of this with PowerSeries or FormalMultilinearSeries, but I couldn't work it out.
There was a problem hiding this comment.
@ocfnash, do you think HasSum or tsum is better here?
There was a problem hiding this comment.
I have a mild preference for HasSum here but either is fine.
|
I actually caught this one yesterday! See #225. Which spelling do you think is better? |
|
Ah, nice! I guess either spelling is probably fine, though |
|
Good point. I can remove that commit from my PR and merge this one instead, if you'd like. I tend to prefer the changes in here (and the comment you had about 'B' -> 'b' is already applied here). |
lean4/src/putnam_2022_b1.lean
Outdated
| (b : ℕ → ℝ) | ||
| (npos : n ≥ 1) | ||
| (Pconst : P.coeff 0 = 0) | ||
| (Pdegree : P.degree = n) |
There was a problem hiding this comment.
You could drop n entirely and this too:
| (Pdegree : P.degree = n) |
Even Lean agrees (warning ugly proof):
example (P : Polynomial ℤ) (h : Odd (P.coeff 1)) :
0 < P.degree := by
have h0 : ¬ Odd (0 : ℤ) := by simp [← Int.not_even_iff_odd, not_not]
have hP : 0 ≤ P.degree := by
rw [Polynomial.zero_le_degree_iff]
rintro rfl
rw [Polynomial.coeff_zero] at h
contradiction
suffices P.degree ≠ 0 from lt_of_le_of_ne hP this.symm
rintro contra
rw [Polynomial.eq_C_of_degree_eq_zero contra, Polynomial.coeff_C_succ] at h
contradictionThere was a problem hiding this comment.
Yes, I guess the question is whether including n makes this a more literal translation.
There was a problem hiding this comment.
I think it can be dropped, I would say the informal statement mostly uses it to describe the form of a polynomial which is unnecessary.
This falsely stated that exp had a finite polynomial expansion.
This also cleans up the spelling of "with integer coefficients".