OAI/Analysis/FactorGeneration/OperatorLimits.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Operator-norm completeness of the manuscript's concrete algebra, derived from its actual double-commutant property. No quotient completeness is assumed.

  1. theorem OAI.Generator.Tracial.base_norm_closed line 22
  2. instance OAI.Generator.Tracial.baseCompleteSpace line 28
  3. instance OAI.Generator.Tracial.baseNormedAlgebraRat line 31
  4. theorem OAI.Generator.Tracial.exists_weak_vector_ultralimit line 42
  5. theorem OAI.Generator.Tracial.exists_weak_operator_ultralimit line 71
  6. theorem OAI.Generator.Tracial.weak_operator_limit_mem line 93

    Source documentation

    The double-commutant property retains the weak limit in the actual algebra.

    theorem weak_operator_limit_mem (M : VonNeumannAlgebra H)
    {ι : Type*} {l : Filter ι} [l.NeBot] (a : ι → M.toStarSubalgebra)
    (T : H →L[ℂ] H)
    (ht : ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i : H →L[ℂ] H) x)) l
      (𝓝 (inner ℂ y (T x)))) : T ∈ M := by
…
  7. def OAI.Generator.Tracial.weakOperatorBall line 116
  8. theorem OAI.Generator.Tracial.weakOperatorBall_isCompact line 119
  9. theorem OAI.Generator.Tracial.weakOperatorBall_isClosed line 151
  10. theorem OAI.Generator.weakOperator_nonneg_isClosed line 159
  11. theorem OAI.Generator.weakOperator_lowerBound_isClosed line 178
  12. theorem OAI.Generator.weakOperator_upperBound_isClosed line 187