Note that almost all of these theorems were necessary in order to complete the proof; it is an interesting exercise to see how some of these seemingly unrelated theorems in totally different fields are used in the final proof of the FTC. (To track the usage of a theorem, use the "This theorem is referenced by:" list at the end of the proof page.)
- fofinf1o: Complementary to f1finf1o, this shows that a surjection from a finite set to another of the same size is a bijection (f1finf1o shows the same assuming an injection).
- wlogle: Inspired by a similar theorem in HOL Light (another formalization language), we show that if a predicate satisfies $\varphi(x,y)\leftrightarrow \varphi(y,x)$, i.e. it is symmetric under interchange of $x,y$, then "without loss of generality" we can assume that $x\le y$ in a proof that $\forall x,y:\varphi(x,y)$.
- ifle: A nice property of the conditional operator ${\rm if}(\varphi,x,y)$ (read "if $\varphi$ then $x$, else $y$", or in piecewise notation as $\begin{cases}x&\varphi\\y&\lnot\varphi\end{cases}$) is that it can transform an implication into an inequality. To be precise, if $y\le x$, then $\varphi\to\psi$ implies ${\rm if}(\varphi,x,y)\le{\rm if}(\psi,x,y)$ (and the converse is also true if $x<y$).
- cnrecnv, cnrehmeo: The canonical map $\Bbb R^2\to\Bbb C$ is the function $\langle x,y\rangle\mapsto x+iy$. We already know from cnref1o that this map is invertible; here we show that the inverse is $z\mapsto\langle\Re\,z,\Im\,z\rangle$. Since all the functions involved here are known to be continuous, this allows us to deduce that the map is a homeomorphism, and so $\Bbb R^2$ under the product topology is homeomorphic to $\Bbb C$ under the metric topology.
- max0add: The identity $f^++f^-=|f|$, where $f^+=\max(f,0)$ and $f^-=\max(-f,0)$ are the positive and negative part functions. See also max0sub which shows $f^+-f^-=f$.
- txbas2: If $B$ and $C$ are topology bases, then $\{u\times v\,|\,u\in B,v\in C\}$ is also a basis for a topology, where $u\times v$ is the cartesian product of sets. This generalizes txbas which assumes that $B$ and $C$ are topologies.
- txbasval: The topological product $\scr B\times\scr C$ is defined as the topology generated by the basis discussed in the last bullet, but it is only defined on topologies, not topological bases. Here we show that if $B$ is a basis for $\scr B$ and $C$ is a basis for $\scr C$, then $\{u\times v\,|\,u\in B,v\in C\}$ is a basis for $\scr B\times\scr C$. Note the difference from the definition, which defines $\scr B\times\scr C$ as the topology generated by $\{u\times v\,|\,u\in{\scr B},v\in{\scr C}\}$ - we see that it is sufficient to consider rectangles of basis elements and not topology elements.
- iccntr: The interior of the closed interval $[x,y]$ is the open interval $(x,y)$, in the standard topology on the reals.
- volsup2*, volcn*, volivth*: The intermediate value theorem for Lebesgue measure: Given a measurable set $A$, there is a measurable subset of $A$ of any measure $0\le x\le\operatorname{vol}(A)$.
- I changed the token for the set of all (Lebesgue) integrable functions from the made-up $f\in{\rm Itgbl}$ to $f\in L^1$, since the latter actually seems to be in use and so may be more understandable to the lay-mathematician.
- mbfimaopn, mbfimaopn2: The preimage of an open set under a measurable function is measurable. Note in particular that these are open sets in the complex topology, not the real topology; the proof essentially proceeds by showing that open rectangles with rational coordinates form a countable basis for the topology on $\Bbb C$.
- cncombf: The composition $g\circ f$ is measurable if $f$ is measurable and $g$ is continuous. This could be generalized to $g$ Borel-measurable, but I don't feel like defining the Borel
- itg2gt0*, itggt0*: If $\operatorname{vol}(A)>0$ and $f>0$ on $A$, then $\int_A f>0$. This is a nice proof that is discussed in a previous post.
- itg2cn, itgcn: Absolute continuity of the Lebesgue integral. If $f$ is integrable, then for any $\varepsilon>0$ there is a $\delta>0$ such that for any measurable set $A$ with $\operatorname{vol}(A)<\delta$, $\int_A|f|<\varepsilon$. Note that no assumptions on $f$ other than integrability are needed.
- itgeqa: If two functions are equal almost everywhere, then they have the same integrable and one is integrable iff the other is.
- itgss3: If $A\subseteq B$ and $B\setminus A$ is a nullset, then $f$ is integrable on $A$ iff it is integrable on $B$ and the integrals are the same.
- iblsub, itgsub: If $f,g$ are integrable, then $f-g$ is integrable and $\int(f-g)=\int f-\int g$.
- itgfsum: If $f_1,f_2,\dots f_n$ are integrable, then $\sum_{k=1}^nf_k$ is integrable and $\int_A\sum_{k=1}^nf_k=\sum_{k=1}^n\int_Af_k$.
- iblabs, iblabsr: If $f$ is a measurable function, then $f$ is integrable iff $|f|$ is integrable.
- iblmulc2, itgmulc2: If $f$ is integrable and $c\in\Bbb C$, then $c\cdot f$ is integrable and $\int_Ac\cdot f=c\int_Af$.
- itgabs: If $f$ is integrable, then $|\int_Af|\le\int_A|f|$. This is another nice proof that works on arbitrary complex functions $f$.
- dvcj: The derivative $(f(x)^*)'$ is $f'(x)^*$, where ${}^*$ denotes the conjugate function. This does not follow from dvcof (the chain rule) because ${}^*$ is not differentiable as a complex function and is just the identity as a real function.
- dvfre: The derivative of a real function is a real function.
- dvmptid, dvmptc, dvmptadd, $\dots$, dvmptco: These theorems are nothing new in terms of actual content, in the sense that we already have formulas for the derivative of a sum, product, etc.; rather these are designed to be easy to use in proofs so that one can quickly differentiate a function given by a formula, in a sense providing an "algorithm" for differentiation. Supported here are the rules: $$c'=0\quad x'=1\quad (f+g)'=f'+g'\quad (fg)'=f'g+g'f\quad (cf)'=cf'\quad (-f)'=-f'$$ $$(f-g)'=f'-g'\quad (f^*)'=f'^*\quad (\Re\,f)'=\Re\,f'\quad (\Im\,f)'=\Im\,f'$$ Also the chain rule $(f(g(x)))'=f'(g(x))g'(x)$ as well as restriction theorems: if $f:X\to\Bbb C$ is differentiable on $X$ and $Z\subseteq X$, $Y=Z^\circ$ is the interior of $Z$, then $(f\upharpoonright Z)'=f'\upharpoonright Y$.
- rolle: Rolle's theorem. If $f:[a,b]\to\Bbb R$ is continuous on $[a,b]$, differentiable on $(a,b)$, and $a<b$ and $f(a)=f(b)$, then there is an $x\in(a,b)$ such that $f'(x)=0$.
- mvth: The Mean Value Theorem. If $f:[a,b]\to\Bbb R$ is continuous on $[a,b]$, differentiable on $(a,b)$, and $a<b$, then there is an $x\in(a,b)$ such that $f'(x)=\frac{f(b)-f(a)}{b-a}$.
- dveq0: If $f:[a,b]\to\Bbb R$ is continuous on $[a,b]$ and differentiable with derivative $0$ on $(a,b)$, then $f$ is a constant function.
- ftc1a: Let $f:D\to\Bbb C$ be an integrable function, and $(a,b)\subseteq D\subseteq\Bbb R$ with $a\le b$. Define $G:[a,b]\to\Bbb C$ by $G(x)=\int_a^xf(t)\,dt$. Then $G$ is a continuous function on $[a,b]$.
- ftc1: Now assume that $f$ is also continuous at some $c\in(a,b)$. Then $G$ is differentiable at $c$, and $G'(c)=f(c)$.
- ftc1cn: Simplifying the assumptions, if $f:(a,b)\to\Bbb C$ is continuous and integrable, then $G'=f$.
- ftc2: Let $f:[a,b]\to\Bbb C$ be a function differentiable on $(a,b)$ such that $f'$ is integrable and continuous. Then $\int_a^bf'=f(b)-f(a)$.
This will be theorem #15 of 100 at Formalizing 100 Theorems; as of now there are thus 35 theorems formalized in Metamath. You can see the others at the metamath 100 page.
* These theorems were discussed with natural-language proofs in integral of a positive function.
No comments:
Post a Comment