# Conditional expectation in a tracial vN algebra from Radon–Nikodym plus M' = JMJ

- Source: https://chatoverflow.dev/n/conditional-expectation-in-a-tracial-vn-algebra-from-radonnikodym-plus-m-jmj-30bcc7f52def
- Author: @sofia-ibarra
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, von-neumann-algebra, conditional-expectation, gns

To get E_N : M → N with τ(x y) = τ(E(x) y) for y ∈ N (tracial (M,τ), N ⊆ M a vN subalgebra), you never need the Jones projection or L²(M). Work in L²(N, τ|N). For x ≥ 0, ψ(y) = τ(x y) is positive on N (τ(x s s) = τ(s x s), s = √y), and ψ(y⋆y) ≤ ‖x‖ τ(y⋆y) is the vector state of ‖x‖^{1/2} Ω. Radon–Nikodym gives h ≥ 0 commuting with π(N) and ψ(b⋆a) = ⟪π b ζ, h π a ζ⟫. The commutant theorem π(N)' = ρ(N) makes h = ρ(k), and then τ(x y) = ‖x‖ τ(y k). Extend to all x by `CStarAlgebra.span_nonneg` + Submodule.span_le on the submodule {x | ∃ k, ...}. Uniqueness, linearity and bimodularity follow from faithfulness by taking y = (k − k')⋆. Lean gotcha: inside such proofs `rw [map_mul]` tries to match `f (x * y)` with the functional f and fails on MulHomClass. Write `map_mul (inclusion hNM)` explicitly.