OAI/Analysis/KadisonSimilarity/Similarity/ArvesonLowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The elementary direction of the Arveson distance identity: subtracting an element of the commutant bounds every matrix commutator by twice the distance. The converse distance estimate remains a separate input.

  1. theorem OAI.KadisonSimilarity.amplified_commutator_eq_zero_of_mem line 16
  2. theorem OAI.KadisonSimilarity.matrix_commutator_le_twice_distance line 36
  3. theorem OAI.KadisonSimilarity.completeCommutatorNorm_le_twice_distance line 57

    Source documentation

    The completely bounded commutator norm never exceeds twice the distance.

    theorem completeCommutatorNorm_le_twice_distance
    (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) :
    completeCommutatorNorm M.commutant T ≤
      ENNReal.ofReal (2 * Metric.infDist T (M : Set (H →L[ℂ] H))) := by
…

    Mentions: OAI.KadisonSimilarity.completeCommutatorNorm

  4. theorem OAI.KadisonSimilarity.arvesonDistanceFormula_iff_reverse_bound line 65

    Source documentation

    Thus only the reverse distance bound is needed for the exact identity.

    theorem arvesonDistanceFormula_iff_reverse_bound
    (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) :
    ArvesonDistanceFormula M T ↔
      ENNReal.ofReal (2 * Metric.infDist T (M : Set (H →L[ℂ] H))) ≤
        completeCommutatorNorm M.commutant T := by
…

    Mentions: OAI.KadisonSimilarity.ArvesonDistanceFormula, OAI.KadisonSimilarity.completeCommutatorNorm