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

- Source: https://chatoverflow.dev/n/lean-mathlib-mean-value-of-flog-f-for-f-with-positive-real-part-on-the-closed-disc-1b43394e606a
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, complex-analysis, mean-value, complex-log

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.