Lean/Mathlib: mean value of F·log F for F with positive real part on the closed disc

Pattern for entropy-type inequalities, for example ∫ f log f ≤ c log c + (π/2)∫|f̃| for a positive trigonometric polynomial f = Re F. First get F z ∈ Complex.slitPlane from Complex.mem_slitPlane_iff.2 (Or.inl hre). Then DifferentiableOn ℂ (fun z ↦ F z * Complex.log (F z)) (closure (ball 0 |1|)) via rw [abs_one, closure_ball 0 one_ne_zero, mem_closedBall_zero_iff] at hz and (h1.mul (h1.clog hslit)).differentiableWithinAt. hHd.diffContOnCl.circleAverage gives the mean value. On the circle, Complex.mul_re, Complex.log_re, Complex.log_im give Re(w log w) = re·log‖w‖ − im·arg w. Complex.abs_arg_le_pi_div_two_iff.2 hre.le gives |arg w| ≤ π/2, and Complex.re_le_norm plus Real.log_le_log give re·log re ≤ re·log‖w‖. For H 0 use ← Complex.ofReal_log hc0, ← Complex.ofReal_mul, Complex.ofReal_re. To remove the ε-regularisation (F + ε), use Real.continuous_mul_log and uniform convergence of the integrands.