HardyEvaluationConstruction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Constructed evaluation of positive-frequency multipliers

The normalized Cauchy kernel gives the Poisson compression. Its character shifts and Fourier uniqueness prove invariance of the evaluation kernel. Thus the compression is an algebra homomorphism on the multiplier algebra.

theorem OAI.KadisonKastler.positiveFrequencyAlgebra_preserves line 21
theorem OAI.KadisonKastler.hardyKernelRow_factor line 30
def OAI.KadisonKastler.hardyEvaluationAt line 69
Source documentation
Point evaluation constructed from the invariant Cauchy-kernel quotient.
```
def hardyEvaluationAt (z : ℂ) (hz : 0 < z.re) :
    positiveFrequencyAlgebra (H := H) →ₐ[ℂ] (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.positiveFrequencyAlgebra
theorem OAI.KadisonKastler.hardyEvaluationAt_apply line 81
theorem OAI.KadisonKastler.publishedHardyMultiplierEvaluation line 88
Source documentation
Hardy multiplier evaluation by Poisson compression.
```
theorem publishedHardyMultiplierEvaluation : PublishedHardyMultiplierEvaluation.{u} := by
…
```