theorem TruncatedFourierInversion.tendsto_eLpNorm_indicator_compl_Icc {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : Filter.Tendsto (fun (N : ℕ) => MeasureTheory.eLpNorm ((Set.Icc (-↑N) ↑N)ᶜ.indicator g) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

theorem TruncatedFourierInversion.truncated_fourier_hat_memLp (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (N : ℝ) : MeasureTheory.MemLp ((Set.Icc (-N) N).indicator ↑↑(FourierTransform.fourier f)) 2 MeasureTheory.volume

theorem TruncatedFourierInversion.truncated_fourier_inversion_L2 (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Filter.Tendsto (fun (N : ℕ) => ‖f - FourierTransformInv.fourierInv (MeasureTheory.MemLp.toLp ((Set.Icc (-↑N) ↑N).indicator ↑↑(FourierTransform.fourier f)) ⋯)‖) Filter.atTop (nhds 0)