About one third of the theorems is specific for the Dirichlet Kernel and the Fourier series results (if there is interest, I can write an overview of the main proof).
The other theorems are (mostly) general purpose statements, that will probably be useful for other users. As a general note, using deduction form it's "easy" to have hypothesis shorter than the main statement, and mmj2 autocomplete algorithm takes enormous advantage from this fact. Here is Mario's description "I consider theorems with no new variables, of any arity, but such that every hypothesis is shorter than the original theorem". So, whenever I saw that I needed a "basic" result over and over, I took the opportunity to increase the "library". ~ eliood is such an example: when mmj2 sees a statement that matches, essentially does the job for you (I always proof backward style, I'm not sure it would work as well proving forward). And also similar theorems where created ~ eliocd , ~ elicod , ~ eliccd. Here are the areas where most new theorems where developed. ORDERING ON REAL NUMBERS - REAL AND COMPLEX NUMBERS BASIC OPERATIONS I've tried to complete some of the list of results we have about commutativity/associativity and comparison, see ~ mul13d ~ subadd4b ~ xrlttri5d as examples. And there are also some non so trivial results, see ~ upbdrech2 and ~ ssfiunibd as examples. REAL INTERVALS Some are simple new autocomplete friendly library theorems ( ~ eliood family described above, as an example) , some are simple snippets I had to use over and over ( see ~ icogelb and similar theorems for all kinds of intervals, all kind of bounds and all kind of comparisons). There are many other theorems about intervals, involving difference, union, inclusion, relationships between bounds, and so on. Nothing fancy here, the only nontrivial result may be ~ evthiccabs (an application of the extreme value theorem, that I could have classified in another section). LIMITS A lot of theorems I had to write for the Fourier proof. Some are for limit of sequences, some are for infinite sums, some are for limit of functions, some are for limit points and some are for limsup. To get a taste of some of the results, you can take a look at ~ ellimciota (an explicit value for the limit, when the limit exists at a limit point), ~ climinf (a bounded monotonic non increasing sequence converges to the infimum of its range), ~ divlimc (and similar theorems for other bynary and unary operations), ~ limclner (the limit of the function exits only if the left and the right limits are equal) , ~ islpcn ~ lptre2pt (results about limit points) and ~ limcperiod (a result for limits of periodic functions). TRIGONOMETRY As the title says... you can take a look at ~ cosknegpi as an example. CONTINUOUS FUNCTIONS Some results here I had to use over and over, as an example ~ cncfmptssg is a generalization of other theorems and it allows to remember a single label to handle several cases (a minimizer "could" then jump in later to check if there is a shorter theorem, applying more specific cncfmpt* theorems). Other examples of "library" results are ~ divcncf (and similar theorems for other bynary, unary and nullary operations) , ~ cncfdmsn and ~ cncfcompt . Some other example of results that could be handy are ~ cncfuni ( a function is continuous if it's domain is the union of sets over which the function is continuous ) and ~ jumpncnp (Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point). Some other theorems refer to continuity for periodic functions, like ~ cncfshift or ~ cncfperiod . DERIVATIVES Some theorems are derivatives computed for specific functions (see ~ dvsinax as an example). Some theorems are useful to compute derivatives for generic functions in Map To form, for example ~ dvmptdiv (function-builder for derivative, quotient rule) and similar theorems for other bynary, unary and nullary operations. Similar results are available for functions built with the oF operator, see ~ dvsubf and ~ dvdivf (quotient rule for everywhere-differentiable functions). Some results are specific for periodic functions, see ~ fperdvper . Then there are a few results that allowed me to state the Fourier series convergence using only conditions on the derivative of the function (in "literature" I've always found the piecewise smooth function condition stated saying that the function and its derivative have to be piecewise continuous, but I've shown that the derivative of F being piecewise continuous implies that F itself is piecewise continuous too). The main results are ~ ioodvbdlimc1 (a real function with bounded derivative, has a limit at the lower bound of an open interval) and its symmetric ~ ioodvbdlimc2 . A related result that could be useful is ~ dvbdfbdioo (a function on an open interval, with bounded derivative, is bounded). INTEGRALS Some theorems are integrals computed for specific functions (see ~ itgcoscmulx as an example). Some theorems are of (I expect) general use, for example ~ vol0 ~ volge0 and ~ iblsplit (the union of two integrable functions is integrable). Some theorems are a bit more involved, like ~ ditgeqiooicc ( a function on an open interval, has the same directed integral as its extension on the closed interval; see the theorem to understand what "extension" means in this context ). Some results are for integrals of periodic functions, like ~ itgiccshift and ~ itgperiod . The most important result of this section, probably is ~ itgsubsticc ( integration by u-substitution ). I was not able to use ~ itgsubst "as is" I had to extend it (no other theorems refer to ~ itgsubst, if Mario had the time to try to use it to check if he actually meant to state it that way, or it has to be slightly changed to be more usable; it may very well have been just my fault). Then I used ~ itgsubsticc to prove ~ itgsbtaddcnst (an example of integral by substitution, I guess we don't have other examples of integrals by substitution in set.mm , since ~ itgsubst is not referenced elsewhere ). Please, feel free to ask about anything. 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/b7ec17fe-816d-47f7-8ff8-343931a3c923%40googlegroups.com.
