A certified proof of the Cartan fixed point theorems

DOI10.1007/S10817-010-9198-6MaRDI QIDQ438546zbMATHOpenAlexFDO

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

formal proofcomplex analysisCartan fixed point theoremsHOL-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)

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

• 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?)
• 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
• 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

(2)

• Formalizing basic quaternionic analysis
• The HOL Light theory of Euclidean space

Describes a project that uses

Uses Software

• Coq
• Isabelle/Isar
• HOL Light

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)