Commit 2025-09-16 14:41 0521a543

feat: mean value theorem for harmonic functions (#29682) Building on #9598, prove that harmonic functions on disks in the complex plane are real parts of holomorphic functions. As a corollary, establish the mean value theorem for harmonic functions. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.