HardyCompression.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Algebra evaluation from an invariant reproducing-kernel quotient

The Hardy-space evaluation is a compression. Multiplicativity follows when its kernel is invariant and the operators preserve the positive-frequency space.

def OAI.KadisonKastler.hardyCompressionAlgHom line 24

Source documentation

The compression used for Hardy evaluation. The first identity preserves the positive-frequency space on the kernel vectors, and the second expresses invariance of the evaluation kernel inside that space.

def hardyCompressionAlgHom (A : Subalgebra ℂ (E →L[ℂ] E))
    (i : H →L[ℂ] E) (j : E →L[ℂ] H) (P : E →L[ℂ] E)
    (hji : j.comp i = ContinuousLinearMap.id ℂ H)
    (hleft : ∀ T : A, P.comp (T.val.comp i) = T.val.comp i)
    (hright : ∀ T : A,
      (j.comp T.val).comp P = ((j.comp T.val).comp i).comp j) :
    A →ₐ[ℂ] (H →L[ℂ] H) where
…

theorem OAI.KadisonKastler.hardyCompressionAlgHom_apply line 54