Aloïs Brunel Homepage

Coq


Here are different things I have formalized in Coq.

COMPLEX ANALYSIS

Winding numbers theory

Here is a formalization of the winding number theory and proofs of various complex analysis theorems using it.

Basics

The formalization consists of:

  • A definition of metric spaces and their main properties

  • A definition of euclidean spaces

  • Basics of complex analysis: continuity and differentiation, exponential and logarithm, curve integral

  • A definition of the winding number of a continuous lace thanks to the path lifting property.

  • In the cas of C1 functions, an alternative definition making use of the curve integral

  • The proof of homotopy invariance of the winding numbers

Main results

Classical proof (crucially relying on the notion of winding number) of the following theorems have also been formalized:

 

Classical realizability

Coming soon...

Powered by CoMFoRT !