FiniteAverageRepresentation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Transporting finite averages between represented algebras

def OAI.KadisonKastler.FiniteInnerAverage.pullback line 20
Source documentation
Pull each finite averaging unitary back to the original representation.
```
def pullback (A : FiniteInnerAverage N) (e : Algebra M ≃⋆ₐ[ℂ] Algebra N) :
    FiniteInnerAverage M where
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.FiniteInnerAverage.pullback_algebraApply line 27

theorem OAI.KadisonKastler.FiniteInnerAverage.pullback_norm_error line 47

Source documentation

Isometric algebra transport preserves the scalar approximation error.

theorem pullback_norm_error (A : FiniteInnerAverage N)
    (e : Algebra M ≃⋆ₐ[ℂ] Algebra N) (he : ∀ x : Algebra M, ‖e x‖ = ‖x‖)
    (x : Algebra M) (z : ℂ) :
    ‖(A.pullback e).apply x.val - z • (1 : H →L[ℂ] H)‖ =
      ‖A.apply (e x).val - z • (1 : K →L[ℂ] K)‖ := by
…

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