noncomputable def ApproxIdentityR.rescaledKernel (K : ℝ → ℝ) (ε x : ℝ) : ℝ

theorem ApproxIdentityR.approxIdentity_tendsto_Lp_norm (K : ℝ → ℝ) (p : ENNReal) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hK : MeasureTheory.Integrable K MeasureTheory.volume) (hK_int : ∫ (x : ℝ), K x = 1) (f : ℝ → ℂ) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : Filter.Tendsto (fun (ε : ℝ) => MeasureTheory.eLpNorm (fun (x : ℝ) => MeasureTheory.convolution (rescaledKernel K ε) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x - f x) p MeasureTheory.volume) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem ApproxIdentityR.approxIdentity_tendsto_L1_norm (K : ℝ → ℝ) (hK : MeasureTheory.Integrable K MeasureTheory.volume) (hK_int : ∫ (x : ℝ), K x = 1) (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Filter.Tendsto (fun (ε : ℝ) => MeasureTheory.eLpNorm (fun (x : ℝ) => MeasureTheory.convolution (rescaledKernel K ε) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x - f x) 1 MeasureTheory.volume) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

noncomputable def CesaroSummation.fejerKernelBase (x : ℝ) : ℝ

noncomputable def CesaroSummation.fejerKernel (N x : ℝ) : ℝ

theorem CesaroSummation.fejerKernelBase_nonneg (x : ℝ) : 0 ≤ fejerKernelBase x

theorem CesaroSummation.sin_sq_half_le (x : ℝ) : Real.sin (x / 2) ^ 2 * (1 + x ^ 2) ≤ 2 * x ^ 2

theorem CesaroSummation.fejerKernelBase_le_bound (x : ℝ) : fejerKernelBase x ≤ 4 / Real.pi * (1 + x ^ 2)⁻¹

theorem CesaroSummation.fejerKernelBase_measurable : Measurable fejerKernelBase

theorem CesaroSummation.fejerKernelBase_integrable : MeasureTheory.Integrable fejerKernelBase MeasureTheory.volume

theorem CesaroSummation.hasDerivAt_antideriv_cexp (a : ℂ) (ha : a ≠ 0) (t : ℝ) : HasDerivAt (fun (x : ℝ) => (1 - ↑x) * Complex.exp (a * ↑x) / a + Complex.exp (a * ↑x) / a ^ 2) ((1 - ↑t) * Complex.exp (a * ↑t)) t

theorem CesaroSummation.integral_one_sub_mul_cexp (a : ℂ) (ha : a ≠ 0) : ∫ (ξ : ℝ) in 0..1, (1 - ↑ξ) * Complex.exp (a * ↑ξ) = (Complex.exp a - 1 - a) / a ^ 2

theorem CesaroSummation.integral_tri_cexp (a : ℂ) (ha : a ≠ 0) : ∫ (ξ : ℝ) in -1..1, ↑(1 - |ξ|) * Complex.exp (a * ↑ξ) = (Complex.exp a + Complex.exp (-a) - 2) / a ^ 2

theorem CesaroSummation.fourier_tri_ae_eq (w : ℝ) : ∫ (ξ : ℝ) in -1..1, ↑(1 - |ξ|) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑w * ↑ξ) = ↑(2 * Real.pi * fejerKernelBase (2 * Real.pi * w))

theorem CesaroSummation.fejerKernelBase_integral : ∫ (x : ℝ), fejerKernelBase x = 1

theorem CesaroSummation.tendsto_inv_atTop_nhdsWithin_Ioi : Filter.Tendsto (fun (N : ℝ) => N⁻¹) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

theorem CesaroSummation.cesaro_L1_convergence (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Filter.Tendsto (fun (N : ℝ) => MeasureTheory.eLpNorm (fun (x : ℝ) => MeasureTheory.convolution (ApproxIdentityR.rescaledKernel fejerKernelBase N⁻¹) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x - f x) 1 MeasureTheory.volume) Filter.atTop (nhds 0)

noncomputable def SchwartzFourierInversion.bookFourier (f : ℝ → ℂ) (ξ : ℝ) : ℂ

noncomputable def SchwartzFourierInversion.bookFourierInv (g : ℝ → ℂ) (x : ℝ) : ℂ

theorem SchwartzFourierInversion.fourier_inversion (f : SchwartzMap ℝ ℂ) : FourierTransformInv.fourierInv (FourierTransform.fourier f) = f

theorem SchwartzFourierInversion.fourierInv_eq_fourier_neg (f : SchwartzMap ℝ ℂ) (x : ℝ) : (FourierTransformInv.fourierInv f) x = (FourierTransform.fourier f) (-x)

theorem SchwartzFourierInversion.real_inner_eq_mul (v w : ℝ) : inner ℝ v w = v * w

theorem SchwartzFourierInversion.fourierChar_inner_eq_exp (v ξ : ℝ) : ↑(Real.fourierChar (-inner ℝ v (ξ / (2 * Real.pi)))) = Complex.exp (-(Complex.I * ↑v * ↑ξ))

theorem SchwartzFourierInversion.bookFourier_eq_fourier_rescale (f : SchwartzMap ℝ ℂ) (ξ : ℝ) : bookFourier (⇑f) ξ = (FourierTransform.fourier f) (ξ / (2 * Real.pi))

theorem SchwartzFourierInversion.plancherel_schwartz_book (f : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), ‖bookFourier (⇑f) ξ‖ ^ 2 = 2 * Real.pi * ∫ (x : ℝ), ‖f x‖ ^ 2

theorem TempDistFourierInversion.fourier_fourierInv_tempered (T : TemperedDistribution ℝ ℂ) : FourierTransform.fourier (FourierTransformInv.fourierInv T) = T

theorem TempDistFourierInversion.fourierInv_fourier_tempered (T : TemperedDistribution ℝ ℂ) : FourierTransformInv.fourierInv (FourierTransform.fourier T) = T

theorem L2FourierExtension.fourier_schwartz_approx_tendsto (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (fj : ℕ → SchwartzMap ℝ ℂ) (hfj : Filter.Tendsto (fun (j : ℕ) => (fj j).toLp 2 MeasureTheory.volume) Filter.atTop (nhds f)) : Filter.Tendsto (fun (j : ℕ) => FourierTransform.fourier ((fj j).toLp 2 MeasureTheory.volume)) Filter.atTop (nhds (FourierTransform.fourier f))

theorem L2FourierExtension.fourier_L2_linear_isometry_equiv : ∃ (e : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), (∀ (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), e f = FourierTransform.fourier f) ∧ ∀ (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), e.symm f = FourierTransformInv.fourierInv f

theorem L2FourierExtension.plancherel_L2 (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖FourierTransform.fourier f‖ = ‖f‖

theorem L2FourierExtension.fourier_inversion_L2' (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : FourierTransform.fourier (FourierTransformInv.fourierInv f) = f

theorem L2FourierExtension.fourier_L2_injective (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hf : FourierTransform.fourier f = 0) : f = 0

theorem L2FourierExtension.fourier_L2_injective' : Function.Injective FourierTransform.fourier

noncomputable def FourierInversionL2.bookInverseFourier (f : ℝ → ℂ) (x : ℝ) : ℂ

theorem FourierInversionL2.fourier_isometry_L2 (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖FourierTransform.fourier f‖ = ‖f‖

theorem FourierInversionL2.fourier_L2_equiv : ∃ (e : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), (∀ (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), e f = FourierTransform.fourier f) ∧ (∀ (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), e.symm f = FourierTransformInv.fourierInv f) ∧ ∀ (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), ‖e f‖ = ‖f‖

theorem InverseFourierL1L2Agreement.neg_innerₗ_flip : (-innerₗ ℝ).flip = -innerₗ ℝ

theorem InverseFourierL1L2Agreement.inverseFourier_L2_agrees_L1 (h : ℝ → ℂ) (hh₁ : MeasureTheory.Integrable h MeasureTheory.volume) (hh₂ : MeasureTheory.MemLp h 2 MeasureTheory.volume) : ↑↑(FourierTransformInv.fourierInv (MeasureTheory.MemLp.toLp h hh₂)) =ᵐ[MeasureTheory.volume] FourierTransformInv.fourierInv h

theorem InverseFourierL1L2Agreement.inverseFourier_L2_agrees_L1_book (h : ℝ → ℂ) (hh₁ : MeasureTheory.Integrable h MeasureTheory.volume) (hh₂ : MeasureTheory.MemLp h 2 MeasureTheory.volume) : ∀ᵐ (x : ℝ), ↑↑(FourierTransformInv.fourierInv (MeasureTheory.MemLp.toLp h hh₂)) x = FourierInversionL2.bookInverseFourier h x

noncomputable def FourierInjectiveL1.cesaroMean (f : ℝ → ℂ) (N x : ℝ) : ℂ

theorem FourierInjectiveL1.mathlib_fourier_eq_zero_of_bookFourier_eq_zero (f : ℝ → ℂ) (hhat : ∀ (ξ : ℝ), SchwartzFourierInversion.bookFourier f ξ = 0) (w : ℝ) : FourierTransform.fourier f w = 0

theorem FourierInjectiveL1.integral_smul_eq_zero_of_bookFourier_eq_zero (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hhat : ∀ (ξ : ℝ), SchwartzFourierInversion.bookFourier f ξ = 0) (g : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) (hg_cs : HasCompactSupport g) : ∫ (x : ℝ), g x • f x = 0

theorem FourierInjectiveL1.fourier_injective_L1 (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hhat : ∀ (ξ : ℝ), SchwartzFourierInversion.bookFourier f ξ = 0) : f =ᵐ[MeasureTheory.volume] 0

theorem L2L1FourierAgree.fourier_L2_eq_L1 (f : ℝ → ℂ) (hf1 : MeasureTheory.MemLp f 1 MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ↑↑(FourierTransform.fourier (MeasureTheory.MemLp.toLp f hf2)) =ᵐ[MeasureTheory.volume] FourierTransform.fourier f