Project VD

Formalizing Value Distribution Theory

This project aims to formalize value distribution theory for meromorphic functions in the complex plane, roughly following Serge Lang's Introduction to Complex Hyperbolic Spaces. The project uses the Lean theorem prover and builds on mathlib, the Lean mathematical library.

Help Wanted

Please be in touch if you would like to join the fun!

Current State and Future Plans

Milestones reached

• Formalized Nevanlinna's First Main Theorem and merged code into Mathlib
• Formalized the Lemma on Logarithmic Derivatives
• First Main Theorem as a statement about invariance under Möbius transformations
• Characterization of rational functions in terms of their characteristic
• Merged the formalization of first main theorem into Lean's mathlib

Next Milestones

• Transcendence criteria
• The Second Main Theorem
• Establish some of the more immediate applications
• Merge formalizations into mathlib

These plans might change, depending on feedback from the community and specific interests of project participants.

Material Covered

The following concepts have been formalized so far.

• Harmonic functions in the complex plane
  • Laplace operator and associated API
  • Definition and elementary properties of harmonic functions
  • Mean value properties of harmonic functions
  • Real and imaginary parts of holomorphic functions as examples of harmonic functions
• Holomorphic functions in the complex plane
  • Existence of holomorphic functions with given real part
• Meromorphic Functions in the complex plane
  • API for continuous extension of meromorphic functions, normal form of meromorphic functions up to changes along a discrete set
  • Behavior of pole/zero orders under standard operations
  • Zero/pole divisors attached to meromorphic functions and associated API
  • Extraction of zeros and poles
  • Canonical decomposition and variants
• Integrals and integrability of special functions
  • Interval integrals and integrability of the logarithm and its combinations with trigonometric functions; circle integrability of log ‖z-a‖
  • Circle integrability of log ‖meromorphic‖
• Basic functions of Value Distribution Theory
  • The positive part of the logarithm, API, standard inequalities and estimates
  • Logarithmic counting functions of divisors
  • Nevanlinna heights of entire meromorphic functions
  • Proximity functions for entire meromorphic functions
• Jensen's formula, generalized Poisson-Jensen formula
• Nevanlinna's First Main Theorem
• Lemma on Logarithmic Derivatives
• Characterization of constant in terms of their characteristic ("Quantitative Liouville Theorem").
• Characterization of rational functions in terms of their characteristic.