OAI/Analysis/FactorGeneration/MatrixEncoding.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Algebraic encoding of four corner operators by two self-adjoint matrices.

  1. def OAI.Generator.MatrixEncoding.E11 line 16
  2. def OAI.Generator.MatrixEncoding.E12 line 17
  3. def OAI.Generator.MatrixEncoding.E21 line 18
  4. def OAI.Generator.MatrixEncoding.E22 line 19
  5. def OAI.Generator.MatrixEncoding.corner line 20
  6. def OAI.Generator.MatrixEncoding.encodeA line 21
  7. def OAI.Generator.MatrixEncoding.encodeB line 22
  8. theorem OAI.Generator.MatrixEncoding.encodeA_selfAdjoint line 24
  9. theorem OAI.Generator.MatrixEncoding.encodeB_selfAdjoint line 33
  10. theorem OAI.Generator.MatrixEncoding.complement line 42
  11. theorem OAI.Generator.MatrixEncoding.star_E12 line 46
  12. theorem OAI.Generator.MatrixEncoding.cut_offDiagonal line 51
  13. theorem OAI.Generator.MatrixEncoding.cut_a₁ line 57
  14. theorem OAI.Generator.MatrixEncoding.cut_a₂ line 63
  15. theorem OAI.Generator.MatrixEncoding.cut_a₃ line 70
  16. theorem OAI.Generator.MatrixEncoding.cut_a₄ line 76
  17. theorem OAI.Generator.MatrixEncoding.matrix_reconstruction line 82
  18. theorem OAI.Generator.MatrixEncoding.matrix_units_mem line 91
  19. theorem OAI.Generator.MatrixEncoding.encoded_corners_mem line 99
  20. theorem OAI.Generator.MatrixEncoding.corner_algebraMap line 110
  21. theorem OAI.Generator.MatrixEncoding.encoded_corners_mem_scalar line 117

    Source documentation

    The source's shift C 1_N needs no extra corner-membership hypothesis.

    theorem encoded_corners_mem_scalar (NQ : StarSubalgebra 𝕜 Mat)
    {a₁ a₂ a₃ a₄ : R} (C : 𝕜)
    (hE : (E11 : Mat) ∈ NQ) (hA : encodeA a₁ a₂ (algebraMap 𝕜 R C) ∈ NQ)
    (hB : encodeB a₃ a₄ ∈ NQ) :
    corner a₁ ∈ NQ ∧ corner a₂ ∈ NQ ∧ corner a₃ ∈ NQ ∧ corner a₄ ∈ NQ := by
…

    Mentions: OAI.Generator.MatrixEncoding.E11, OAI.Generator.MatrixEncoding.encodeA, OAI.Generator.MatrixEncoding.encodeB, OAI.Generator.MatrixEncoding.corner

  22. theorem OAI.Generator.MatrixEncoding.eq_top_of_corner_and_units line 126
  23. theorem OAI.Generator.MatrixEncoding.E22_idempotent line 140
  24. theorem OAI.Generator.MatrixEncoding.E22_commute_encodeA line 145
  25. theorem OAI.Generator.MatrixEncoding.encodeA_scalar_shift line 151
  26. theorem OAI.Generator.MatrixEncoding.scalar_shift_selfAdjoint line 157