HardyCauchyKernel.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The one-sided exponential and its Cauchy transform

These are the concrete kernels for evaluating a positive-frequency multiplier. All transforms here are computed from the half-line exponential integral.

def OAI.KadisonKastler.positiveLaplaceKernel line 21
Source documentation
The exponentially decreasing kernel on the positive frequency half-line.
```
def positiveLaplaceKernel (z : ℂ) : ℝ → ℂ :=
…
```
theorem OAI.KadisonKastler.integrable_positiveLaplaceKernel line 24
theorem OAI.KadisonKastler.positiveLaplaceKernel_memLp line 29
theorem OAI.KadisonKastler.fourier_positiveLaplaceKernel line 45
theorem OAI.KadisonKastler.cauchyResolvent_norm_sq line 69
Source documentation
The squared norm of the Cauchy kernel is a multiple of a probability Poisson kernel. This also supplies its square integrability.
```
theorem cauchyResolvent_norm_sq {z : ℂ} (hz : 0 < z.re) (s : ℝ) :
    ‖(z + (2 * Real.pi * s : ℝ) * Complex.I)⁻¹‖ ^ 2 =
      realPoissonKernel (-z.im / (2 * Real.pi)) (z.re / (2 * Real.pi)) s /
        (2 * z.re) := by
…
```
Mentions: OAI.KadisonKastler.realPoissonKernel
theorem OAI.KadisonKastler.cauchyResolvent_memLp line 81
theorem OAI.KadisonKastler.fourier_positiveLaplaceKernel_toLp line 100
Source documentation
The integral computation also holds for the actual unitary L² transform.
```
theorem fourier_positiveLaplaceKernel_toLp {z : ℂ} (hz : 0 < z.re) :
    𝓕 ((positiveLaplaceKernel_memLp hz).toLp (positiveLaplaceKernel z)) =
      (cauchyResolvent_memLp hz).toLp
        (fun s : ℝ => (z + (2 * Real.pi * s : ℝ) * Complex.I)⁻¹) := by
…
```
Mentions: OAI.KadisonKastler.positiveLaplaceKernel_memLp, OAI.KadisonKastler.positiveLaplaceKernel, OAI.KadisonKastler.cauchyResolvent_memLp