FourierLaplace.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Fourier transform of the two-sided exponential

This scalar calculation is the first half of the Cauchy-kernel character formula needed for Poisson demodulation. It uses the existing half-line exponential integrals and no additional published-input hypothesis.

def OAI.KadisonKastler.laplaceKernel line 21
Source documentation
The integrable two-sided exponential, with complex values.
```
def laplaceKernel (a t : ℝ) : ℂ := Complex.exp (-((a : ℂ) * ((|t| : ℝ) : ℂ)))
```
def OAI.KadisonKastler.laplaceFourierIntegrand line 23
theorem OAI.KadisonKastler.laplaceFourierIntegrand_nonpos line 26
theorem OAI.KadisonKastler.laplaceFourierIntegrand_nonneg line 35
theorem OAI.KadisonKastler.laplaceFourierIntegrand_integrableOn_left line 44
theorem OAI.KadisonKastler.laplaceFourierIntegrand_integrableOn_right line 53

theorem OAI.KadisonKastler.fourier_laplaceKernel_resolvents line 63

Source documentation

The transform is the sum of the two elementary half-line resolvents.

theorem fourier_laplaceKernel_resolvents {a : ℝ} (ha : 0 < a) (ξ : ℝ) :
    𝓕 (laplaceKernel a) ξ =
      ((a : ℂ) - (2 * Real.pi * ξ : ℝ) * Complex.I)⁻¹ -
        (-(a : ℂ) - (2 * Real.pi * ξ : ℝ) * Complex.I)⁻¹ := by
…

Mentions: OAI.KadisonKastler.laplaceKernel

theorem OAI.KadisonKastler.integrable_laplaceKernel line 99
Source documentation
Integrability of the two-sided exponential, obtained from the same half-line estimates used in its transform calculation.
```
theorem integrable_laplaceKernel {a : ℝ} (ha : 0 < a) : Integrable (laplaceKernel a) := by
…
```
Mentions: OAI.KadisonKastler.laplaceKernel
theorem OAI.KadisonKastler.continuous_laplaceKernel line 109
theorem OAI.KadisonKastler.complex_resolvent_pair line 113
theorem OAI.KadisonKastler.fourier_laplaceKernel line 142
Source documentation
The scalar rational form of the Fourier transform.
```
theorem fourier_laplaceKernel {a : ℝ} (ha : 0 < a) (ξ : ℝ) :
    𝓕 (laplaceKernel a) ξ = ((2 * a / (a ^ 2 + (2 * Real.pi * ξ) ^ 2) : ℝ) : ℂ) := by
…
```
Mentions: OAI.KadisonKastler.laplaceKernel