A certified proof of the Cartan fixed point theorems

DOI10.1007/S10817-010-9198-6MaRDI QIDQ438546zbMATH OpenOpenAlexFDO

Authors Gianni Ciolli, Graziano Gentili, Marco Maggesi

Publication date 31 July 2012

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-010-9198-6

zbMATH Keywords

Cartan fixed point theoremscomplex analysisformal proofHOL-light

Mathematics Subject Classification ID

Maximum principle, Schwarz's lemma, Lindelöf principle, analogues and generalizations; subordination (30C80) Holomorphic functions of several complex variables (32A99)

Review text

The paper consists of two big parts, the first is a crash course in complex analysis, the second reports on the formalization of some of the proofs in the mechanized reasoning system HOL-light. In the first part, the authors introduce holomorphic functions and some of their surprising properties (when compared to their real counterparts), e.g., the identity principle. First the one-dimensional case and then some higher-dimensional theorems are introduced. With these preliminaries the first and second theorem of Cartan are introduced -- that under certain weak conditions a holomorphic higher-dimensional map must be the identity map or it must be linear, respectively. Furthermore the proofs of these theorems are sketched. In addition, a theorem on an involution and a relationship of holomorphic automorphisms and Möbius transformations is given. In the second part of the paper the HOL-light system and its extensive library on real and complex numbers are introduced. In order to prove Cartan's theorems, important properties such as the rule on the derivative of composed functions are introduced. The paper concludes with remarks on the de Bruijn factor (how much longer the formal proofs are compared to paper proofs), and the procedural (what is done to produce a proofs) versus declarative (how does the proof look like) style of proofs in formal systems.

Recommendations

• The HOL Light theory of Euclidean space
• Theorem Proving in Higher Order Logics
• A formalization of metric spaces in HOL Light
• A generalization of Cartan's theorem to proper holomorphic mappings
• Remarks to Cartan's second main theorem for holomorphic curves into \(\mathbb {P}^N(\mathbb {C})\)

Cites work

• A Declarative Language for the Coq Proof Assistant
• A new approach to Cullen-regular functions of a quaternionic variable
• A new theory of regular functions of a quaternionic variable
• Die Funktionentheorie der Differentialgleichungen \(\Delta u=0\) und \(\Delta\Delta u=0\) mit vier reellen Variablen
• Extension results for slice regular functions of a quaternionic variable
• Formal proof
• Formal proof - the four color theorem
• Formal proof -- theory and practice
• scientific article; zbMATH DE number 3699581 (Why is no real title available?)
• scientific article; zbMATH DE number 3779725 (Why is no real title available?)
• scientific article; zbMATH DE number 45113 (Why is no real title available?)
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• scientific article; zbMATH DE number 5486212 (Why is no real title available?)
• Power series and analyticity over the quaternions
• Quaternionic analysis
• Recent Developments for Regular Functions of a Hypercomplex Variable
• Reelle Transformationsgruppen und invariante Metriken auf komplexen Räumen
• Rigidity of Holomorphic Mappings and a New Schwarz Lemma at the Boundary
• Sur les fonctions de plusieurs variables complexes. L'itération des transformations intérieures d'un domaine borné
• Theorem Proving in Higher Order Logics

Cited in

(3)

• Formalizing basic quaternionic analysis
• The HOL Light theory of Euclidean space
• The Cartan Fixed Point Theorems

Describes a project that uses

Uses Software

• Isabelle/Isar
• HOL Light
• Coq

This page was built for publication: A certified proof of the Cartan fixed point theorems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438546)