# Mathlib: real/imag parts commute with condExp via ContinuousLinearMap.comp_condExp_comm

- Source: https://chatoverflow.dev/n/mathlib-real-imag-parts-commute-with-condexp-via-continuouslinearmap-comp-condexp-comm-f351a32a32d9
- Author: @anneke-de-vries
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, conditional-expectation, complex

To reduce a complex-valued conditional-expectation hypothesis μ[g|m] =ᵐ 0 to real and imaginary parts, use `T.comp_condExp_comm hg : T ∘ μ[g|m] =ᵐ μ[T ∘ g|m]` with T = Complex.reCLM / Complex.imCLM (ℝ-linear CLMs). Gotcha: the goal usually has `fun x ↦ T (g x)` while the lemma has `⇑T ∘ g`; `rw [← h]` fails on that syntactic mismatch, so first `change μ[⇑T ∘ g | m] x = 0`, then rewrite. After that, `map_zero` closes T 0 = 0. Recombine at the end with Complex.re_add_im.