Formalization of the Sequential Banach-Alaoglu theorem
Loading...
URL
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu |
Bachelor's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
2024-11-15
Department
Major/Subject
Matematiikka ja systeemitieteet
Mcode
SCI3029
Degree programme
Teknistieteellinen kandidaattiohjelma
Language
en
Pages
33
Series
Abstract
Computer formalization of mathematics refers to expressing mathematical concepts, theorems and proofs in a formal language the computer can understand. Formalization is carried out using proof assistants, which provide feedback and enable writing formal mathematical statements and the verification of the correctness of their proofs. Many proof assistants use type-theoretic foundations instead of the familiar set theory. In type theory, each term is assigned a unique type to ensure that operations are performed only with compatible types. In this thesis, we formalize the sequential Banach-Alaoglu theorem. The formalization is carried out using the Lean4 interactive proof assistant, and built on top of Mathlib, the library of formalized mathematics in Lean.The Banach-Alaoglu theorem states that the closed unit ball is compact in the weak* topology of the dual space of a normed space. The Sequential Banach-Alaoglu theorem considers sequential compactness instead of compactness. We introduce relevant mathematical definitions and the results to be formalized, along with their proofs. Furthermore, we illustrate how these concepts are translated into formal language and give a brief introduction to formalization. Selected details of the formalized proofs and the process of formalization are described.Matematiikan tietokoneformalisointi tarkoittaa matemaattisten käsitteiden, tulosten ja todistusten kääntämistä formaalille tietokonekielelle. Formalisoinnissa käytetään todistusassistenttia, joka mahdollistaa formaalien matemaattisten väitteiden kirjoittamisen, ja niiden todistusten oikeellisuuden tarkistamisen. Joukko-opin sijaan monet todistusassistentit perustuvat tyyppiteoriaan, jossa jokaisella termillä on yksikäsitteinen tyyppi, mikä varmistaa että matemaattiset operaatiot suoritetaan ainoastaan yhteensopivien tyyppien välillä. Tässä kandidaatintyössä formalisoidaan jonoittainen Banach-Alaoglu-lause ja annetaan lyhyt johdanto formalisoinnin perusteisiin. Formalisoinnissa käytetään interaktiivista Lean4-todistusassistenttia, sekä Leanilla formalisoitujen tulosten kirjastoa Mathlibia. Banach-Alaoglu-lauseen mukaan suljettu yksikkökuula on kompakti normiavaruuden duaalin heikko-*-topologiassa. Jonoittaisessa Banach-Alaoglu-lauseessa tarkastellaan jonokompaktiutta kompaktiuden sijaan. Työssä esitellään oleelliset matemaattiset määritelmät ja tulokset todistuksineen, sekä havainnollistetaan, miten nämä tulokset käännetään formaalille kielelle todistusassistentin avulla. Formalisoiduista todistuksista ja formalisointiprosessista esitellään tärkeimmät yksityiskohdat.Description
Supervisor
Kytölä, KalleThesis advisor
Kytölä, KalleKeywords
formalization, type theory, Lean, Banach-Alaoglu theorem, weak* topology