OAI/Analysis/KadisonKastler/NestMultiplierApproximation.lean

Actual measurable multipliers from a nest approximation

The published distance formula first supplies a nest-preserving operator. The proved invariant mean retains that property and its error bound. Published diagonal decomposition then gives an actual measurable field, and uniqueness of fields transfers the approximation estimate pointwise almost everywhere. No analytic extension theorem is assumed here.