OAI/Analysis/Quasitrace/Extension.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Matrix order and the normalization of genuine corner extensions.

  1. theorem OAI.Kaplansky.corner_add line 17
  2. theorem OAI.Kaplansky.corner_sub line 21
  3. theorem OAI.Kaplansky.corner_smul line 25
  4. theorem OAI.Kaplansky.corner_zero line 29
  5. theorem OAI.Kaplansky.diagonal_add line 34
  6. theorem OAI.Kaplansky.diagonal_sub line 39
  7. theorem OAI.Kaplansky.diagonal_one line 44
  8. theorem OAI.Kaplansky.corner_nonneg line 48
  9. theorem OAI.Kaplansky.diagonal_nonneg line 53
  10. theorem OAI.Kaplansky.diagonal_positiveContraction line 57
  11. theorem OAI.Kaplansky.corner_positive_equal line 73
  12. theorem OAI.Kaplansky.map_positive_diagonal line 78
  13. theorem OAI.Kaplansky.corner_normalization line 84
  14. theorem OAI.Kaplansky.corner_scalar_sub line 91

    Source documentation

    Scalar translation uses the corner identity, not the ambient unit.

    theorem corner_scalar_sub (τ : OneQuasitrace (CStarMatrix n n A)) (k : n)
    (c : ℝ) {a : A} (ha : IsSelfAdjoint a) :
    τ (corner k ((c : ℂ) • (1 : A) - a)) =
      (c : ℂ) * τ (corner k (1 : A)) - τ (corner k a) := by
…

    Mentions: OAI.Kaplansky.OneQuasitrace, OAI.Kaplansky.corner

  15. theorem OAI.Kaplansky.corner_scalar_upper_bound line 106
  16. theorem OAI.Kaplansky.upperLeft_eq_corner line 129
  17. theorem OAI.Kaplansky.extension_value_two line 134
  18. theorem OAI.Kaplansky.extension_not_normalized line 146

    Source documentation

    A direct check that the target's matrix extension is not accidentally required to be normalized.

    theorem extension_not_normalized (τ : OneQuasitrace A) (hτ : τ.Normalized)
    (σ : OneQuasitrace (CStarMatrix (Fin 2) (Fin 2) A))
    (hσ : ∀ a, σ (upperLeft a) = τ a) : ¬ σ.Normalized := by
…

    Mentions: OAI.Kaplansky.OneQuasitrace, OAI.Kaplansky.upperLeft