Mario's posts

Post has attachment

**Dirichlet's theorem**

There have been some calls for an informal exposition of the recent formal proof of Dirichlet's theorem: Theorem 9.4.1 ( dirith , Dirichlet's theorem): If $N\in\Bbb N$ and $(A,N)=1$, then there are infinitely many primes $p$ such that $N\mid p-A$. If you ha...

Post has attachment

**Mathbox update: Functions of Number Theory**

I should probably apologize for having nothing but mathbox updates on this blog of late, but this is the only type of post I release regularly, in conjunction with the actual theorems being uploaded to the Metamath site. (I try to make up for it by making f...

Post has attachment

**Mathbox update: Fundamental Theorem of Algebra**

The main theorems in this short update are Van der Waerden's theorem (already discussed in a previous post ) and the Fundamental Theorem of Algebra. This last one is one of the metamath 100, and the proof was surprisingly straightforward. The hardest part w...

Post has attachment

**Mathbox update: Ostrowski's theorem**

Hello all, This update has two main foci: the rounding off of the integration theorems with the integration by parts and integration by substitution formulas, and an unrelated work to formalize the concept of an absolute value over a ring (in the algebra se...

Post has attachment

**Mathbox update: The Fundamental Theorem of Calculus**

Today I just put the finishing touches on a proof of the Fundamental Theorem of Calculus, which is the first theorem from the Formalizing 100 Theorems list to be proven since the creation of this blog, and has been the main reason for my recent fixation on ...

Post has attachment

**Integral of a positive function is positive**

Here is a nice theorem that is not as simple as the statement would have you believe: Theorem ( itggt0 ): If $f$ is integrable and $A$ is a measurable set such that $0<\DeclareMathOperator{\vol}{vol}\vol(A)\le\infty$ and $f(x)>0$ for all $x\in A$, then $\in...

Post has attachment

**Van der Waerden's theorem**

To take a break from all this real analysis, I thought I'd change gears and formalize a gem of number theory, which goes by the name of Van der Waerden's theorem . The proof is not yet complete, so instead I'll just lay out the high-level strategy of the pr...

Post has attachment

**Mathbox update: More integrals**

This is the first post on this blog in the mathbox-update category, so allow me to explain what this is. I periodically release my latest work in Metamath to the database, and in this post I go over the highlights and additions to be found in the release, l...

Wait while more posts are being loaded