OAI/Analysis/FiniteFactor/OperatorUltraweak.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.ultraweakTopology line 12

   Source documentation

   The actual ultraweak topology, generated by absolutely summable vector functionals. No continuity of a chosen trace is built into this definition.

   @[instance_reducible] def ultraweakTopology : TopologicalSpace (H →L[ℂ] H) :=
   …

2. theorem OAI.FiniteFactor.vectorFunctional_ultraweak_continuous line 19