FourierSmoothing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Frequency support of the concrete interval smoothing

The convolution has Fourier transform equal to the interval transform times the actual compactly supported cutoff. This connects the physical endpoint bounds with truncation in the height variable.

theorem OAI.CubicFirstMoment.fourier_scaledKernel line 21
Source documentation
Dilation of the kernel dilates its Fourier support by exactly the same factor.
```
theorem fourier_scaledKernel (k : ℝ → ℂ) {T : ℝ} (hT : 0 < T) (ξ : ℝ) :
    𝓕 (scaledKernel k T) ξ = 𝓕 k (ξ/T) := by
…
```
Mentions: OAI.CubicFirstMoment.scaledKernel
theorem OAI.CubicFirstMoment.integrable_intervalStep line 35
theorem OAI.CubicFirstMoment.intervalSmoothing_eq_convolution line 47
theorem OAI.CubicFirstMoment.fourier_intervalSmoothing line 56
Source documentation
The exact Fourier multiplier of the interval approximation.
```
theorem fourier_intervalSmoothing {T : ℝ} (hT : 0 < T) (a b ξ : ℝ) :
    𝓕 (intervalSmoothing (scaledKernel truncationKernel T) a b) ξ =
      frequencyCutoff (ξ/T) * 𝓕 (fun x => (intervalStep a b x : ℂ)) ξ := by
…
```
Mentions: OAI.CubicFirstMoment.intervalSmoothing, OAI.CubicFirstMoment.scaledKernel, OAI.CubicFirstMoment.truncationKernel, OAI.CubicFirstMoment.frequencyCutoff, OAI.CubicFirstMoment.intervalStep
theorem OAI.CubicFirstMoment.fourier_intervalSmoothing_zero line 67
Source documentation
No frequencies beyond the prescribed truncation height survive.
```
theorem fourier_intervalSmoothing_zero {T : ℝ} (hT : 0 < T) (a b ξ : ℝ)
    (hξ : T ≤ |ξ|) :
    𝓕 (intervalSmoothing (scaledKernel truncationKernel T) a b) ξ = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.intervalSmoothing, OAI.CubicFirstMoment.scaledKernel, OAI.CubicFirstMoment.truncationKernel