FourierIntegralL2.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Agreement of the integral and Hilbert-space Fourier transforms

The reproducing kernels used by Hardy evaluation are integrable square-integrable functions, rather than Schwartz functions. This bridge identifies their explicit integral transforms with the existing unitary Fourier transform.

theorem OAI.KadisonKastler.fourier_toLp_of_integrable line 21
Source documentation
An integrable scalar function whose Fourier transform is square integrable has the same transform in the concrete L² Fourier representation.
```
theorem fourier_toLp_of_integrable {f : ℝ → ℂ} (hf : Integrable f)
    (hf2 : MemLp f 2) (hF2 : MemLp (𝓕 f) 2) :
    𝓕 (hf2.toLp f) = hF2.toLp (𝓕 f) := by
…
```
theorem OAI.KadisonKastler.fourierInv_toLp_of_integrable line 48
Source documentation
An integrable scalar function whose Fourier transform is square integrable has the same transform in the concrete L² Fourier representation.
```
theorem fourierInv_toLp_of_integrable {f : ℝ → ℂ} (hf : Integrable f)
    (hf2 : MemLp f 2) (hF2 : MemLp (𝓕⁻ f) 2) :
    𝓕⁻ (hf2.toLp f) = hF2.toLp (𝓕⁻ f) := by
…
```