61 lines
2.6 KiB
Markdown
61 lines
2.6 KiB
Markdown
# Project VD
|
|
|
|
### Formalizing Value Distribution Theory
|
|
|
|
This project aims to formalize value distribution theory for meromorphic
|
|
functions in the complex plane, roughly following the sections on Nevanlinna
|
|
Theory in Serge Lang's "Introduction to Complex Hyperbolic Spaces". The project
|
|
uses the lean4 computer language and builds on the lean mathematical library.
|
|
|
|
We are looking for collaborators. Please be in touch if you would like to join
|
|
the fun!
|
|
|
|
## State of Affairs and Future Plans
|
|
|
|
With the formalization of "Nevanlinna's First Main Theorem", the project has
|
|
recently reached its first milestone. The current code has "proof of concept"
|
|
quality: It compiles fine but needs refactoring and documentation. The next
|
|
goals are as follows.
|
|
|
|
- Clean up the existing codebase and feed intermediate results into the lean
|
|
mathematical library
|
|
- Formalize the Theorem on Logarithmic Differentials
|
|
- Formalize the Second Main Theorem of value distribution theory
|
|
- Establish some of the more immediate applications
|
|
|
|
These plans might change, depending on feedback from the community and specific
|
|
interests of project participants.
|
|
|
|
## Material Covered
|
|
|
|
We touched on the following subjects.
|
|
|
|
- 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 primitives [duplication of work already under review at
|
|
mathlib]
|
|
- 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
|
|
- 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
|
|
- The First Main Theorem
|