OAI/Analysis/KadisonKastler/NestAveraging.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Averaging operators preserving a projection nest

This is the algebraic averaging step after the nest distance estimate. The projections may be indexed by any type; completeness of the nest is needed by the distance theorem, not by these preservation calculations.

  1. def OAI.KadisonKastler.PreservesProjectionNest line 20
  2. theorem OAI.KadisonKastler.preservesProjectionNest_conjugate line 23
  3. theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_zero_block line 37
  4. theorem OAI.KadisonKastler.ScalarInvariantMean.operatorMean_preservesProjectionNest line 49
  5. theorem OAI.KadisonKastler.ScalarInvariantMean.averageConjugation_preservesProjectionNest line 56

    Source documentation

    Permuting the nest makes its algebra invariant under averaging.

    theorem ScalarInvariantMean.averageConjugation_preservesProjectionNest
    (m : ScalarInvariantMean G) (P : ι → H →L[ℂ] H)
    (U : G →* unitary (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : PreservesProjectionNest P T)
    (hP : ∀ g i, ∃ j, P i = unitaryConj (U g) (P j)) :
    PreservesProjectionNest P (m.averageConjugation U T) := by
…

    Mentions: OAI.KadisonKastler.ScalarInvariantMean, OAI.KadisonKastler.PreservesProjectionNest, OAI.KadisonKastler.unitaryConj

  6. theorem OAI.KadisonKastler.ScalarInvariantMean.norm_averageConjugation_sub_fixed_le line 67

    Source documentation

    Averaging near a fixed target costs no additional error.

    theorem ScalarInvariantMean.norm_averageConjugation_sub_fixed_le
    (m : ScalarInvariantMean G) (U : G →* unitary (H →L[ℂ] H))
    (T A : H →L[ℂ] H) (hA : ∀ g, unitaryConj (U g) A = A) :
    ‖m.averageConjugation U T - A‖ ≤ ‖T - A‖ := by
…

    Mentions: OAI.KadisonKastler.ScalarInvariantMean, OAI.KadisonKastler.unitaryConj