Hi Benoit Il giorno domenica 15 dicembre 2019 22:02:33 UTC+1, Benoit ha scritto:
> First, I re-ask my previous question: is there a particular reason you chose sine and cosine over the exponential function ? the proofs that I followed stated the coefficients in terms of sine and cosine. Some of them, then, proved some intermediate results using the complex exponential form (it simplified some integral calculation), some other sources instead kept using sine and cosine everywhere. When I had a choice between two alternative such proofs, I followed the sine/cosine approach. As I side note, I could be wrong, but I believe that the sine / cosine statement is more familiar and accessible to a wider audience. > ~ eliood , ~ eliocd , ~ elicod , ~ eliccd : it looks to me that they could be strengthened by assuming only that A, B, C are extended reals. For instance, in the proof of eliood, use elioo1 instead of elioo2, and similarly in the proof of eliccd, use elicc1 instead of elicc2. elioo1 and elioo2 are "different" theorems, and I'm sure there are pros and cons in both. But I see that elioo2 has (roughly) ten times the number of references than elioo1 does and I guess that's an indication that elioo2 turns out to be handy more often than elioo1. It maybe I chose eliood in such form, because I noticed it was required more often in that form. Of course, it may be useful to also introduce an elioo1d alternative that takes the elioo1 "approach". > ~ evthiccabs : I'm surprised that the proof is so long, given evthicc. Have you used MM>minimize * on you theorems? unfortunately I miss some of the features of metamath.exe , because I use mmj2 only (but I'm really intrigued by Thierry's plugin for Eclipse, I hope I will soon have time to take a closer look at it). If I'm not mistaken, Normann periodically runs a "minimize" on the all set.mm, and that will help. As a general note, given the current tools, it looks like there is a trade off between productivity and proof optimization, I'll try to explain with an example: I always proof backward; assume I have proven a statement in the form |- ( ps <-> ( ch /\ th ) ) and I want to prove |- ( ph -> ps ) The "optimized" way would be to use sylanbrc and for some time I tried to remember all such labels, but unfortunately we don't have intellisense yet, and... it was hard. So I decided to always go with sylibr that I can remember and covers a large number of "upstream" statements. But I have to pay with an additional jca and that will introduce an additional line. I hope that, in the future, we will have a minimizer that can (after the fact) revert non optimal sylibr into sylanbrc . HTH Glauco -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0565e681-45a8-4e2e-8127-0b5ac419ea0d%40googlegroups.com.
