Pi irrational #1351
Pi irrational #1351
Conversation
affeldt-aist
added
the
enhancement ✨
affeldt-aist
force-pushed
the
pi_irrational
branch
from
2053c7f
to
fe8a6a5
Compare
There was a problem hiding this comment.
Overall a nice milestone that we can do this in ~600 lines now. Sadly at least 50% of that seems to be about measurable/differentiable/integrable stuff that ought to be automated. But it's a nice application nonetheless.
Moving some of the files around as you mentioned in your comments is probably good. Especially the polynomial stuff will be nice to have independently. And the filename thing should be an easy fix. Otherwise I don't see any blockers
| End derive_horner. | ||
|
|
||
| Local Open Scope classical_set_scope. | ||
|
|
There was a problem hiding this comment.
Is there a reason we don't have just continuous (horner p))? Seems like that would imply all of this, but I am quite unfamiliar with mathcomps polynomials so I expect i am missing something.
| Local Notation "f ^` ()" := (derive1 f) : classical_set_scope. | ||
|
|
||
| (* connect MathComp's polynomials with analysis *) | ||
| Section derive_horner. |
There was a problem hiding this comment.
All this stuff about polynomials and derivates is great. It should definitely live in a more accesible place. We'll want it for the full strength Taylor's theorem, for example
| by rewrite -mulrDl hornerD. | ||
| Qed. | ||
|
|
||
| Definition intfsin n := \int[mu]_(x in `[0, pi]) (fsin n x). |
There was a problem hiding this comment.
I suppose most of these should be Local Definition, and Local Lemma if anything. No reason for these to leak outside the file if it can be helped.
| Let abx x : 0 < x < pirat -> 0 < a na - b nb * x. | ||
| Proof. | ||
| move=> /andP[x0]; rewrite subr_gt0. | ||
| rewrite /pirat /exercise6.pirat ltr_pdivlMr 1?mulrC//. |
There was a problem hiding this comment.
The explicit dependency on the filename is a little jarring. I would prefer at most one of the following to be true, ideally neither
- The file is called exercise6 without any context
- The text of the filename explicitly appears in the proof script.
Motivation for this change
@LaurenceRideau
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers