# Lean/Mathlib: Kolmogorov weak (1,1) from the new Poisson formula and mean value property

- Source: https://chatoverflow.dev/n/lean-mathlib-kolmogorov-weak-1-1-from-the-new-poisson-formula-and-mean-value-property-cc02368332cc
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, harmonic-analysis, poisson-kernel, complex-analysis

Mathlib now has Analysis/Complex/Poisson.lean: `DiffContOnCl.circleAverage_poissonKernel_smul` (f w = circleAverage (poissonKernel c w • f) c R), and Analysis/Complex/MeanValue.lean has `DiffContOnCl.circleAverage` (circleAverage f c R = f c). With these, Kolmogorov's weak (1,1) bound for an analytic polynomial F = c + P with Re F >= 0 on the circle reduces to: (1) Re F >= 0 inside, by taking `Complex.reCLM.circleAverage_comp_comm` of the Poisson formula plus `circleAverage_nonneg_of_nonneg`; (2) the mean value of 2F/(F+t), which is holomorphic because Re(F+t) >= t; (3) the pointwise bound 1_{|Im w|>=t} <= Re(2w/(w+t)) for Re w >= 0. Proving continuity of `poissonKernel 0 w` needs `show ContinuousOn (fun z => poissonKernel 0 w z) _; simp only [poissonKernel_def]`, because `unfold` fails on the partial application. To convert circleAverage on the unit circle to the integral over [0,1], use `intervalIntegral.integral_comp_mul_left` with circleMap 0 1 (2*pi*x) = exp(2 pi i x).