Work at SourceForge, help us to make it a better place! We have an immediate need for a Support Technician in our San Francisco or Denver office.

Close

[7860bc]: thys / Integration / document / root.tex Maximize Restore History

Download this file

root.tex    91 lines (71 with data), 2.0 kB

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
\documentclass[11pt,a4paper]{report}
% further packages required for unusual symbols (see also isabellesym.sty)
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{wasysym}
\usepackage{eufrak}
\usepackage{textcomp}
%\usepackage{apalike}
%\usepackage{times}
\usepackage{isabelle,isabellesym}
% this should be the last package used
\usepackage{pdfsetup}
% proper setup for best-style documents
\urlstyle{rm}
\isabellestyle{it}
\hyphenation{Isabelle}
\renewcommand{\isamarkupheader}[1] {\markright{THEORY~\isabellecontext}}
\date{15th May 2003}
\parindent 0pt\parskip 0.5ex
\begin{document}
\title{Formalizing Integration Theory, with an Application to
Probabilistic Algorithms}
\author{Stefan Richter\\
LuFG Theoretische Informatik\\
RWTH Aachen\\
Ahornstraße 55\\
52056 Aachen\\
FRG\\
\url{richter@informatik.rwth-aachen.de}}
\date{\today}
\maketitle
\pagestyle{headings}
\tableofcontents
% include generated text of all theories
% \input{session}
\newpage
\pagestyle{headings}
\input{intro}
\input{Sigma_Algebra}
\subsection{Monotone convergence}
\label{sec:monconv}
\input{MonConv}
\subsection{Measure spaces}
\label{sec:measure-spaces}
\input{Measure}
\newpage
\section{Real-valued random variables}
\label{sec:realrandvar}
\input{RealRandVar}
\chapter{Integration}
\label{cha:integration}
The chapter at hand assumes a central position in the present paper. The Lebesgue
integral is defined and its characteristics are shown in
\ref{sec:stepwise-approach}. To illustrate the problems arising in
doing so, we first look at implementation alternatives that did not
work out.
\section{Two approaches that failed}
\label{sec:two-approaches-that}
\input{Failure}
\section{The three-step approach}
\label{sec:stepwise-approach}
\input{Integral}
\input{outro}
\begin{flushleft}
\bibliographystyle{plain}
\bibliography{root}
\end{flushleft}
\end{document}