HardyKernelShift.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Character shifts of the reproducing kernel

A backward shift followed by the positive-frequency projection is scalar on an exponential kernel. Forward shifts preserve the positive-frequency space.

theorem OAI.KadisonKastler.positiveLaplace_shift_cut line 20
theorem OAI.KadisonKastler.fourier_frequencyProjection_zero line 54
theorem OAI.KadisonKastler.regularCharacter_preserves_positive line 65
theorem OAI.KadisonKastler.hardyReproducingKernel_backward_shift line 84
Source documentation
Projected negative character shifts act diagonally on a reproducing kernel.
```
theorem hardyReproducingKernel_backward_shift (z : ℂ) (hz : 0 < z.re)
    {b : ℝ} (hb : 0 ≤ b) :
    regularFrequencyProjection 0
      ((regularCharacterUnitary (H := ℂ) (2 * Real.pi * (-b)) :
…
```
Mentions: OAI.KadisonKastler.regularFrequencyProjection, OAI.KadisonKastler.regularCharacterUnitary