FiniteInnerTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Transport of finite inner averages under inner automorphisms

def OAI.KadisonKastler.FiniteInnerAverage.map line 20
Source documentation
Transport all averaging unitaries by a star automorphism.
```
def map (A : FiniteInnerAverage M) (f : Algebra M ≃⋆ₐ[ℂ] Algebra M) :
    FiniteInnerAverage M where
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.FiniteInnerAverage.map_algebraApply line 27

theorem OAI.KadisonKastler.FiniteInnerAverage.norm_map_inner_sub_scalar line 46

Source documentation

Inner transport preserves the distance of the averaged element to a scalar.

theorem norm_map_inner_sub_scalar (A : FiniteInnerAverage M)
    (u : _root_.unitary (Algebra M)) (x : Algebra M) (z : ℂ) :
    ‖((A.map (Unitary.conjStarAlgAut ℂ (Algebra M) u)).algebraApply
        (Unitary.conjStarAlgAut ℂ (Algebra M) u x)).val - z • (1 : H →L[ℂ] H)‖ =
      ‖(A.algebraApply x).val - z • (1 : H →L[ℂ] H)‖ := by
…

Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage.algebraApply