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

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).