New theorems in this update:
- ivthicc: The intermediate value theorem, in the form "$[f(m),f(n)]\subseteq\operatorname{ran}f$ whenever $m,n\in[a,b]$ and $f:[a,b]\to\Bbb R$ is continuous"; this is a bit more convenient to use than ivth, which explicitly states that $f(a)<u<f(b)$ and $a<b$, so you need to go through some case analysis with increasing/decreasing combinations to use this directly.
- divcn: In a curious oversight, we have continuity of addition, subtraction, and multiplication, but not division. This derives that $f:\Bbb C\times\Bbb C^*\to\Bbb C$ defined by $f(x,y)=\frac xy$ is jointly continuous (in the product topology). (Note that $0$ is excluded from the domain.)
- bndth: The Boundedness Theorem, topological version. A continuous function $f:X\to\Bbb R$, where $X$ is compact, is bounded above.
- evth: The Extreme Value Theorem, topological version. A continuous function $f:X\to\Bbb R$, where $X$ is compact and nonempty, attains its maximum value somewhere on the domain. (Curiously, most books neglect to mention that $X$ has to be nonempty, but it's clearly necessary; the topology $J=\{\emptyset\}$ is compact and has empty base set, and the empty function from $X=\emptyset$ to $\Bbb R$ is continuous, yet it clearly can't attain its maximum because there are no points in the base set.)
- evth2: A continuous function $f:X\to\Bbb R$, $X$ compact, attains its minimum.
- evthicc: Specialize evth and evth2 to the case when $X=[a,b]$ is a closed interval of $\Bbb R$.
- volsup*: The Lebesgue volume function preserves the limit of an increasing sequence of measurable sets.
- df-ditg: Define the directed integral. This is basically the difference between $\int_{[a,b]}f(x)\,dx$ and $\int_a^bf(x)\,dx$ - the second is defined regardless of the order of $a,b$, and negates under a swap of upper and lower limit. It is literally defined as $\int_a^bf(x)\,dx=\int_{(a,b)}f(x)\,dx$ if $a\le b$ and $\int_a^bf(x)\,dx=-\int_{(b,a)}f(x)\,dx$ otherwise. The usage of open intervals is in anticipation of such integrals as $f(x)=\int_0^x\log|t|\,dt$, which would not make sense under a closed interval because $\log 0$ is undefined. As it is, this would be a total function on $\Bbb R$. (The integral at $x=0$ is $0$ regardless of the function being integrated.)
- mbfmulc2re: The product of a measurable function $f:A\to\Bbb C$ and a real constant is a measurable function (the old mbfmulc2 only allowed $f:A\to\Bbb R$).
- mbfposb: A function $f:A\to\Bbb R$ is measurable if and only if the positive and negative parts $f^+=\max(0,f)$, $f^-=(-f)^+$ are measurable.
- mbfadd: The sum of measurable functions is measurable. (This is a nice argument by the decomposition $\{f+g>y\}=\bigcup_{r\in\Bbb Q}\{f>r\}\cap\{g>y-r\}$.)
- itg10a, itg1ge0a, itg1lea: These are "approximate" versions of the analogous theorems itg10, itg1ge0, itg1le which relax their conditions to only hold on a set of full measure. (For example, the integral of a function that is zero for almost all $x$ is zero, where "almost all" means that the measure of the complement is zero.)
- itg1climres*: The simple function integral preserves limiting operations on the base set.
- mbfi1fseq: A ridiculously complicated proof that there is an increasing sequence of simple functions that converge pointwise to any positive measurable function. The proof uses the sequence $$g_n(x)=\begin{cases} \max(2^{-n}\lfloor 2^nf(x)\rfloor,n) & -n\le x\le n \\ 0 & o.w. \end{cases}$$ and verifying that the preimage of each point is a measurable set (by describing it explicitly in terms of preimages of $f$) is a study in case analysis.
- itg2const, itgconst: Integral of a constant function.
- itg2seq: A nice result, although now mostly precluded by mbfi1fseq and itg2i1fseq which give more detailed information on the sequence. For any nonnegative function $f$, there is a sequence of simple functions less than $f$ whose integrals converge to $\int f$.
- itg2split, itgsplit: Unlike the analogous theorem for sums, we don't use itg2add to prove this, and instead prove it "directly" - the upshot of this is that we can work with extended real functions (for which addition is not defined), and also we don't need the countable choice baggage carried along with itg2add. If $A,B$ are almost disjoint measurable sets and $f$ is integrable on $A$ and $B$, then $\int_{A\cup B}f(x)\,dx=\int_A f(x)\,dx+\int_B f(x)\,dx$.
- ditgsplit: The best argument in favor of the definition df-ditg is that the path addition rule $\int_a^cf=\int_a^bf+\int_b^cf$ holds regardless of the relative ordering of $a,b,c$, unlike the analogous theorem for integrals of closed intervals, $\int_{[a,c]}f=\int_{[a,b]}f+\int_{[b,c]}f$, which only holds for $a\le b\le c$.
- mbfmono*, itg2mono*: The Monotone Convergence Theorem for integrals. This and the other starred* entries in the list are explained in much more detail in my previous blog entry.
- itg2i1fseq: Completing the work of mbfi1fseq, here we show that given an increasing sequence of simple functions that converge pointwise to the positive measurable function $f$, the integrals of the simple functions also converge to the integral of $f$. (Combining these two gives an alternative proof of itg2seq.)
- itg2add, itgadd: The main theorem of this update, which is not too complicated but carries some high-powered prerequisites above: If $f,g$ are integrable on $A$, then $$\int_A(f+g)\,dx=\int_Af\,dx+\int_Ag\,dx.$$
No comments:
Post a Comment