FourierCutoff.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A concrete Fourier cutoff kernel

The fixed cutoff is a smooth bump, one near zero and supported in [-1,1]. Its inverse Fourier transform is a normalized Schwartz kernel. Mathlib uses exp(2π i x ξ); this frequency variable differs by 2π from the height variable in the manuscript.

def OAI.CubicFirstMoment.frequencyBump line 21
def OAI.CubicFirstMoment.frequencyCutoff line 27
theorem OAI.CubicFirstMoment.frequencyCutoff_apply line 32
theorem OAI.CubicFirstMoment.frequencyCutoff_one line 34
theorem OAI.CubicFirstMoment.frequencyCutoff_zero line 39
def OAI.CubicFirstMoment.truncationKernel line 44
theorem OAI.CubicFirstMoment.fourier_truncationKernel line 47
Source documentation
Inversion identifies the Fourier transform with the actual compact cutoff.
```
theorem fourier_truncationKernel : 𝓕 truncationKernel = frequencyCutoff :=
…
```
Mentions: OAI.CubicFirstMoment.truncationKernel, OAI.CubicFirstMoment.frequencyCutoff
theorem OAI.CubicFirstMoment.integral_truncationKernel line 51
Source documentation
Normalization follows from the value of the Fourier transform at zero.
```
theorem integral_truncationKernel : (∫ y, truncationKernel y) = 1 := by
…
```
Mentions: OAI.CubicFirstMoment.truncationKernel
theorem OAI.CubicFirstMoment.fourier_interval_error line 58
Source documentation
The chosen Fourier kernel gives the uniform two-endpoint approximation.
```
theorem fourier_interval_error {T : ℝ} (hT : 0 < T) (a b s : ℝ) :
    ‖(intervalStep a b s : ℂ) - intervalSmoothing (scaledKernel truncationKernel T) a b s‖ ≤
      kernelMoment truncationKernel 1 / (1 + T*|s-a|)^2 +
        kernelMoment truncationKernel 1 / (1 + T*|s-b|)^2 :=
…
```
Mentions: OAI.CubicFirstMoment.intervalStep, OAI.CubicFirstMoment.intervalSmoothing, OAI.CubicFirstMoment.scaledKernel, OAI.CubicFirstMoment.truncationKernel, OAI.CubicFirstMoment.kernelMoment