Seminar: Konstruktive Analysis
Zeit und Ort
Mo 14-16, B252; Beginn Montag, 12. Oktober 2026. Bitte melden Sie sich im LSF an.
Inhalt
In dem Seminar soll (reelle und komplexe) Analysis auf konstruktiver Basis (TCF) behandelt werden. Die Beweise sollen auch in formalisierter Form geführt werden, unter Verwendung des Beweisassistenten Minlog.
Vorausgesetzt werden Grundkenntnisse in Mathematischer Logik. Ferner wird
vorausgesetzt, daß die Teilnehmer das
Tutorium
des Beweisassistenten
Minlog
durchgearbeitet haben.
Nach erfolgreichem Besuch des Seminars ist es möglich, eine
Bachelor- oder Masterarbeit zu einem Thema aus diesem Umkreis zu schreiben.
Vorträge
Die Vortragsthemen werden zu Beginn des Seminars in Absprache mit den Teilnehmern festgelegt. Es soll jeweils eine Übersicht über wichtige Definitionen und Theoreme gegeben werden, und an einer oder mehreren Stellen der Beweis am Rechner geführt werden. Ausserdem soll eine Textfassung der behandelten Gegenstände angefertigt werden. In der folgenden Liste beziehen sich die Seitenzahlen auf constr23.pdf.
- Number systems.
nat.scm pos.scm int.scm rat.scm
Equality, compatibility.
Helmut Schwichtenberg, 19. Oktober - Dyadic rational numbers. libdy.scm. Denominator is a power of 2. They suffice to represent reals.
- Real numbers. rea.scm. Cauchy sequences, equality, bound, non-negative, positive, arith functions. p. 2-9.
- Completeness of real numbers. rea.scm rseq.scm. Completeness, convergence, series, comparison and ratio test. p. 11-13, 19-21.
- Coding pairs of natural numbers. natpair.scm rseq.scm. Cauchy product, root coding, quadratic Gauss coding. p. 23,24.
- Sums, permutations, reordering. rsum.scm. Binomial coefficients.
- The exponential function. eser.scm. Estimate of the rest, functional equation, >=0, >0, e^x. p. 24,25.
- The exponential function for complex numbers.
cpx.scm.
p. 25-28. Katharina Wendler. - Sine, cosine, pi.
pi.scm.
p. 87-90. Noah Wedlich.
Literatur
Allgemein
- Bishop/Bridges, Constructive Analysis. Springer 1985.
- A. Bauer, Five stages of accepting constructive mathematics (Bull AMS, 2016)
- Handbook of Constructive Mathematics. Cambridge UP, 2023
Speziell
Minlog
Über Minlog kann man
sich in den mitgelieferten
Dateien tutor.pdf
und ref.pdf
informieren. Eine ausführliche Einführung (von Franziskus
Wiesnet) ist
hier.
Sehr hilfreich ist auch eine Serie von
Videos, die auch von Franziskus Wiesnet angefertigt wurden.
Falls git auf Ihrem Rechner installiert ist, können
Sie die jeweils aktuelle Version von Minlog erhalten durch
Ausführen von
git clone http://www.math.lmu.de/~minlogit/git/minlog.git.
Bitte arbeiten Sie mit dem dev-Zweig (durch Ausführen von git
checkout dev). Eine konkrete Einführung (von Nils Köpp und
Valentin Herrmann) ist
ueb00.scm.
Minlog ist auf den CIP-Rechnern des Mathematischen Instituts
installiert. Wenn man "minlog-dev" in der Konsole eines CIP-Rechners
eingibt wird der dev-Zweig aufgerufen.
Minlog Web (von
Valentin Herrmann) erlaubt das Arbeiten mit Minlog ohne das System zu
installieren.
Sprechstunde
- Helmut Schwichtenberg, Mi 13-14, B434.
Studienordnungen
Formal handelt es sich um zwei Seminare (ein Masterseminar und ein Bachelorseminar), die im gleichen Hörsaal zur gleichen Zeit stattfinden. Die verschiedenen Vortragsthemen sind jeweils entweder nur einschlägig für Bachelor- oder nur einschlägig für Master-Studenten. Das Masterseminar ist unter WP12 in der Masterstudienordnung Mathematik aufgelistet, und das Bachelorseminar in der Bachelorstudienordnung Mathematik unter WP8.
Letzte Änderung
15. Oktober 2026