CauchyFourier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KadisonKastler.fourier_laplaceKernel_cauchy line 17
Source documentation
In mathlib's Fourier convention the transform of the two-sided exponential is exactly the normalized Cauchy density.
```
theorem fourier_laplaceKernel_cauchy {γ : NNReal} (hγ : 0 < γ) (ξ : ℝ) :
    𝓕 (laplaceKernel (2 * Real.pi * γ)) ξ = (cauchyPDFReal 0 γ ξ : ℂ) := by
…
```
Mentions: OAI.KadisonKastler.laplaceKernel
theorem OAI.KadisonKastler.fourierInv_cauchyPDFReal line 32
Source documentation
The inverse transform of the Cauchy density is the two-sided exponential. All integrability hypotheses follow from proved library results and the explicit transform above.
```
theorem fourierInv_cauchyPDFReal {γ : NNReal} (hγ : 0 < γ) (t : ℝ) :
    𝓕⁻ (fun x : ℝ => (cauchyPDFReal 0 γ x : ℂ)) t =
      laplaceKernel (2 * Real.pi * γ) t := by
…
```
Mentions: OAI.KadisonKastler.laplaceKernel