OAI/Analysis/KadisonKastler/DirectIntegralUnitary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds and adjoints for assembled measurable unitaries

The assembly is the actual multiplication operator on L²(X,H). An almost-everywhere fiber bound gives the same operator-norm bound.

  1. theorem OAI.KadisonKastler.regularUnitaryField_star_apply_ae line 20
  2. theorem OAI.KadisonKastler.norm_regularUnitaryField_sub_one_le line 43