OAI/Analysis/FactorGeneration/AmplificationEncoding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

One arbitrary operator and a pair of self-adjoint operators generate the same weakly closed star algebra.

  1. theorem OAI.Generator.realPart_mem line 18
  2. theorem OAI.Generator.imaginaryPart_mem line 23
  3. theorem OAI.Generator.mem_iff_parts_mem line 28
  4. theorem OAI.Generator.wstar_singleton_eq_parts line 35
  5. theorem OAI.Generator.realPart_pack line 52
  6. theorem OAI.Generator.imaginaryPart_pack line 57
  7. theorem OAI.Generator.wstar_pack line 62
  8. theorem OAI.Generator.singlyGenerated_iff_two_selfAdjoint line 67

    Source documentation

    Exact equivalence in thm:main, without proving either side for II1 factors.

    theorem singlyGenerated_iff_two_selfAdjoint (S : StarSubalgebra ℂ Op) :
    SinglyGenerated S ↔ ∃ a ∈ S, ∃ b ∈ S,
      IsSelfAdjoint a ∧ IsSelfAdjoint b ∧ wstar {a, b} = S := by
…

    Mentions: OAI.Generator.wstar

  9. def OAI.Generator.MatrixUnitSystem.concreteCoefficientHom line 90
  10. theorem OAI.Generator.MatrixUnitSystem.coefficient_corner line 93
  11. theorem OAI.Generator.MatrixUnitSystem.coefficient_diagonal line 100
  12. theorem OAI.Generator.MatrixUnitSystem.two_generators_of_four_commutant_generators line 110