CutoffInversion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The same concrete smoothing used for the proved endpoint error is the inverse Fourier integral of its compactly supported frequency multiplier.

theorem OAI.CubicFirstMoment.continuous_fourier_of_integrable line 18
theorem OAI.CubicFirstMoment.integrable_concrete_intervalSmoothing line 23
theorem OAI.CubicFirstMoment.continuous_concrete_intervalSmoothing line 29
theorem OAI.CubicFirstMoment.integrable_fourier_intervalSmoothing line 43
theorem OAI.CubicFirstMoment.concrete_interval_fourier_integral line 58
Source documentation
The inverse integral has support only in the prescribed frequency band, by fourier_intervalSmoothing_zero.
```
theorem concrete_interval_fourier_integral {T : ℝ} (hT : 0 < T) (a b s : ℝ) :
    intervalSmoothing (scaledKernel truncationKernel T) a b s =
      ∫ ξ : ℝ, Complex.exp ((2 * Real.pi * ξ * s : ℝ) * Complex.I) *
        (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