Moving my theorems to the main body - principal objections, too long, fruit of the poison tree.

69 views
Skip to first unread message

tbrend...@gmail.com

unread,
Jul 28, 2021, 8:23:11 AM7/28/21
to Metamath
I've heard others say some of my theorems should be moved to the main body, in particular the area of a circle.  As I have it currently, the area of a circle is based on a strange variant of the Fundamental Theorem of Calculus, based on a notion of the integral that is, frankly, not the integral at all, since it's based on a measure that's a submeasure.  It could, of course, very easily be rewritten to rely on the principle of countable choice.  Moreover, some of my theorems dodging this principle are strictly as good (bddibl and cniccibl) or better (itg2add), even if they are fruit of a poison tree.

And then there are less controversial ones, like the Poincare-Miranda theorem, or the Heine-Cantor theorem, or pi being strictly greater than 3.  And there are those I'm not sure the main body has a place for, like the half-angle theorem.

savask

unread,
Jul 29, 2021, 2:54:10 AM7/29/21
to Metamath
In my opinion, current area of circle proof shouldn't be moved to the main part yet, but not only because it's a "fruit of the poison tree", but also since of the ongoing formalization of measure theory in set.mm. As far as I understand, Glauco Siliprandi's mathbox already contains the formalization of the n-dimensional Lebesgue measure on RR ^m X, as well as theorems about volumes of n-dimensional cubes, etc. It seems that this is more or less enough to reduce the computation of the area to essentially the same integral which was computed in areacirc.

As for the other results, like Heine-Cantor theorem and especially Brouwer fixed point theorem for the unit cube, they certainly deserve being moved to the main part. Since there are no sections in your mathbox, these theorems do not appear in the table of contents and remain a bit obscure. Half-angle theorems probably can be moved to the section "The exponential, sine and cosine functions" of "Elementary trigonometry"; there's already a group of statements about addition/subtraction formulae for trigonometric functions.

среда, 28 июля 2021 г. в 19:23:11 UTC+7, tbrend...@gmail.com:
Reply all
Reply to author
Forward
0 new messages