@[reducible, inline]

noncomputable abbrev TorusConvolution.mulℂ : ℂ →L[ℂ] ℂ →L[ℂ] ℂ

theorem TorusConvolution.eLpNorm_convolution_le {T : ℝ} [hT : Fact (0 < T)] {f g : AddCircle T → ℂ} (hf : MeasureTheory.Integrable f AddCircle.haarAddCircle) (hg : MeasureTheory.Integrable g AddCircle.haarAddCircle) : MeasureTheory.eLpNorm (MeasureTheory.convolution f g mulℂ AddCircle.haarAddCircle) 1 AddCircle.haarAddCircle ≤ MeasureTheory.eLpNorm f 1 AddCircle.haarAddCircle * MeasureTheory.eLpNorm g 1 AddCircle.haarAddCircle

noncomputable def ApproximateIdentity.periodicConvolution (f K : ℝ → ℝ) (x : ℝ) : ℝ

theorem ApproximateIdentity.periodic_continuous_uniformContinuous {f : ℝ → ℝ} {p : ℝ} (hp : 0 < p) (hf : Continuous f) (hper : Function.Periodic f p) : UniformContinuous f

theorem ApproximateIdentity.convolution_sub_eq (f K : ℝ → ℝ) (x : ℝ) (hK : IntervalIntegrable K MeasureTheory.volume (-Real.pi) Real.pi) (hfK : IntervalIntegrable (fun (y : ℝ) => f (x - y) * K y) MeasureTheory.volume (-Real.pi) Real.pi) (hnorm : 1 / (2 * Real.pi) * ∫ (y : ℝ) in -Real.pi..Real.pi, K y = 1) : periodicConvolution f K x - f x = 1 / (2 * Real.pi) * ∫ (y : ℝ) in -Real.pi..Real.pi, (f (x - y) - f x) * K y

theorem ApproximateIdentity.integral_subinterval_le_of_nonneg (g : ℝ → ℝ) (a b c d : ℝ) (hab : a ≤ b) (hbc : b ≤ c) (hcd : c ≤ d) (hg_intble : IntervalIntegrable g MeasureTheory.volume a d) (hg_nonneg : ∀ x ∈ Set.Icc a d, 0 ≤ g x) : ∫ (x : ℝ) in b..c, g x ≤ ∫ (x : ℝ) in a..d, g x

theorem ApproximateIdentity.approximate_identity_lemma (f : ℝ → ℝ) (K : ℕ → ℝ → ℝ) (hf_cont : Continuous f) (hf_periodic : Function.Periodic f (2 * Real.pi)) (hK_intble : ∀ (N : ℕ), IntervalIntegrable (K N) MeasureTheory.volume (-Real.pi) Real.pi) (hfK_intble : ∀ (N : ℕ) (x : ℝ), IntervalIntegrable (fun (y : ℝ) => f (x - y) * K N y) MeasureTheory.volume (-Real.pi) Real.pi) (habs_K_intble : ∀ (N : ℕ), IntervalIntegrable (fun (y : ℝ) => |K N y|) MeasureTheory.volume (-Real.pi) Real.pi) (hdiff_K_intble : ∀ (N : ℕ) (x : ℝ), IntervalIntegrable (fun (y : ℝ) => |f (x - y) - f x| * |K N y|) MeasureTheory.volume (-Real.pi) Real.pi) (h_normalize : ∀ (N : ℕ), 1 / (2 * Real.pi) * ∫ (x : ℝ) in -Real.pi..Real.pi, K N x = 1) (h_bound : ∃ (M : ℝ), ∀ (N : ℕ), ∫ (x : ℝ) in -Real.pi..Real.pi, |K N x| ≤ M) (h_concentrate : ∀ (δ : ℝ), 0 < δ → δ ≤ Real.pi → Filter.Tendsto (fun (N : ℕ) => (∫ (x : ℝ) in -Real.pi..-δ, |K N x|) + ∫ (x : ℝ) in δ..Real.pi, |K N x|) Filter.atTop (nhds 0)) (ε : ℝ) : ε > 0 → ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (x : ℝ), |f x - periodicConvolution f (K N) x| ≤ ε

theorem TrigPolyDensity.trigPoly_dense_in_continuous {T : ℝ} [hT : Fact (0 < T)] : Dense ↑(Submodule.span ℂ (Set.range fourier))

theorem TrigPolyDensity.trigPoly_approx_sup_norm {T : ℝ} [hT : Fact (0 < T)] (f : C(AddCircle T, ℂ)) {ε : ℝ} (hε : 0 < ε) : ∃ p ∈ ↑(Submodule.span ℂ (Set.range fourier)), ‖f - p‖ < ε

noncomputable def FejerL1Density.periodicL1Norm (f : ℝ → ℝ) : ℝ

noncomputable def FejerL1Density.periodicConvolution (f K : ℝ → ℝ) (x : ℝ) : ℝ

noncomputable def FejerL1Density.fejerKernel (N : ℕ) (x : ℝ) : ℝ

noncomputable def FejerL1Density.fejerMean (f : ℝ → ℝ) (N : ℕ) : ℝ → ℝ

def FejerL1Density.IsTrigPolynomial (p : ℝ → ℝ) : Prop

theorem FejerL1Density.periodicL1Norm_nonneg (f : ℝ → ℝ) : 0 ≤ periodicL1Norm f

theorem FejerL1Density.periodicL1Norm_sub_comm (f g : ℝ → ℝ) : (periodicL1Norm fun (x : ℝ) => f x - g x) = periodicL1Norm fun (x : ℝ) => g x - f x

theorem FejerL1Density.abs_sin_mul_le (n : ℕ) (θ : ℝ) : |Real.sin (↑n * θ)| ≤ ↑n * |Real.sin θ|

theorem FejerL1Density.fejerKernel_measurable (N : ℕ) : Measurable (fejerKernel N)

theorem FejerL1Density.fejerKernel_nonneg_aux (N : ℕ) (x : ℝ) : 0 ≤ fejerKernel N x

theorem FejerL1Density.fejerKernel_le_N (N : ℕ) (x : ℝ) : fejerKernel N x ≤ ↑N

theorem FejerL1Density.fejerKernel_intervalIntegrable (N : ℕ) : IntervalIntegrable (fejerKernel N) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.integral_cos_nat_mul_eq_zero (k : ℕ) (hk : k ≠ 0) : ∫ (x : ℝ) in -Real.pi..Real.pi, Real.cos (↑k * x) = 0

theorem FejerL1Density.integral_const_mul_cos_eq_zero (c : ℝ) (k : ℕ) : ∫ (x : ℝ) in -Real.pi..Real.pi, c * Real.cos ((↑k + 1) * x) = 0

theorem FejerL1Density.two_sin_half_mul_cos (k : ℕ) (x : ℝ) : 2 * Real.sin (x / 2) * Real.cos (↑k * x) = Real.sin ((2 * ↑k + 1) * (x / 2)) - Real.sin ((2 * ↑k - 1) * (x / 2))

theorem FejerL1Density.dirichlet_identity (n : ℕ) (x : ℝ) : Real.sin ((2 * ↑n + 1) * (x / 2)) = Real.sin (x / 2) + 2 * Real.sin (x / 2) * ∑ k ∈ Finset.range n, Real.cos ((↑k + 1) * x)

theorem FejerL1Density.fejer_telescope (N : ℕ) (x : ℝ) : ∑ n ∈ Finset.range N, Real.sin ((2 * ↑n + 1) * (x / 2)) * Real.sin (x / 2) = Real.sin (↑N * x / 2) ^ 2

theorem FejerL1Density.sin_half_ne_zero_of_ne_zero {x : ℝ} (hx : x ∈ Set.Ioc (-Real.pi) Real.pi) (hx0 : x ≠ 0) : Real.sin (x / 2) ≠ 0

theorem FejerL1Density.integral_dirichlet_sum (n : ℕ) : ∫ (x : ℝ) in -Real.pi..Real.pi, 1 + 2 * ∑ k ∈ Finset.range n, Real.cos ((↑k + 1) * x) = 2 * Real.pi

theorem FejerL1Density.integral_fejer_sum_all (N : ℕ) : ∫ (x : ℝ) in -Real.pi..Real.pi, ∑ n ∈ Finset.range N, (1 + 2 * ∑ k ∈ Finset.range n, Real.cos ((↑k + 1) * x)) = ↑N * (2 * Real.pi)

theorem FejerL1Density.fejerKernel_normalize (N : ℕ) (hN : N ≠ 0) : 1 / (2 * Real.pi) * ∫ (x : ℝ) in -Real.pi..Real.pi, fejerKernel N x = 1

instance FejerL1Density.instFactLtRealOfNatHMulPi_atlas : Fact (0 < 2 * Real.pi)

theorem FejerL1Density.continuous_periodic_dense_L1 (f : ℝ → ℝ) (hf_periodic : Function.Periodic f (2 * Real.pi)) (hf_intble : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (ε : ℝ) : ε > 0 → ∃ (g : ℝ → ℝ), Continuous g ∧ Function.Periodic g (2 * Real.pi) ∧ (periodicL1Norm fun (x : ℝ) => f x - g x) ≤ ε

theorem FejerL1Density.periodic_integral_translate_abs (h : ℝ → ℝ) (hper : Function.Periodic h (2 * Real.pi)) (y : ℝ) : ∫ (x : ℝ) in -Real.pi..Real.pi, |h (x - y)| = ∫ (x : ℝ) in -Real.pi..Real.pi, |h x|

theorem FejerL1Density.fubini_conv_eq (h : ℝ → ℝ) (N : ℕ) (hh_per : Function.Periodic h (2 * Real.pi)) (hint : MeasureTheory.Integrable (Function.uncurry fun (x y : ℝ) => |h (x - y)| * fejerKernel N y) ((MeasureTheory.volume.restrict (Set.Ioc (-Real.pi) Real.pi)).prod (MeasureTheory.volume.restrict (Set.Ioc (-Real.pi) Real.pi)))) : ∫ (x : ℝ) (y : ℝ) in Set.Ioc (-Real.pi) Real.pi, |h (x - y)| * fejerKernel N y = (∫ (x : ℝ) in Set.Ioc (-Real.pi) Real.pi, |h x|) * ∫ (y : ℝ) in Set.Ioc (-Real.pi) Real.pi, fejerKernel N y

theorem FejerL1Density.young_fejerKernel (h : ℝ → ℝ) (N : ℕ) (hh : IntervalIntegrable h MeasureTheory.volume (-Real.pi) Real.pi) (hh_per : Function.Periodic h (2 * Real.pi)) : periodicL1Norm (periodicConvolution h (fejerKernel N)) ≤ periodicL1Norm h

theorem FejerL1Density.fejer_uniform_convergence (g : ℝ → ℝ) (hg_cont : Continuous g) (hg_per : Function.Periodic g (2 * Real.pi)) (ε : ℝ) : ε > 0 → ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (x : ℝ), |g x - periodicConvolution g (fejerKernel N) x| ≤ ε

theorem FejerL1Density.convolution_linear (g h : ℝ → ℝ) (N : ℕ) (x : ℝ) (hg : IntervalIntegrable (fun (y : ℝ) => g (x - y) * fejerKernel N y) MeasureTheory.volume (-Real.pi) Real.pi) (hh : IntervalIntegrable (fun (y : ℝ) => h (x - y) * fejerKernel N y) MeasureTheory.volume (-Real.pi) Real.pi) : periodicConvolution (fun (y : ℝ) => g y - h y) (fejerKernel N) x = periodicConvolution g (fejerKernel N) x - periodicConvolution h (fejerKernel N) x

theorem FejerL1Density.conv_intble_of_continuous (g : ℝ → ℝ) (hg : Continuous g) (N : ℕ) (x : ℝ) : IntervalIntegrable (fun (y : ℝ) => g (x - y) * fejerKernel N y) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.conv_intble_of_periodic (f : ℝ → ℝ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf_intble : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (N : ℕ) (x : ℝ) : IntervalIntegrable (fun (y : ℝ) => f (x - y) * fejerKernel N y) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.trig_sum_extend (a b : ℕ → ℝ) (N M : ℕ) (hNM : N ≤ M) (x : ℝ) : ∑ n ∈ Finset.range (N + 1), (a n * Real.cos (↑n * x) + b n * Real.sin (↑n * x)) = ∑ n ∈ Finset.range (M + 1), ((if n ≤ N then a n else 0) * Real.cos (↑n * x) + (if n ≤ N then b n else 0) * Real.sin (↑n * x))

theorem FejerL1Density.isTrigPolynomial_add {p q : ℝ → ℝ} (hp : IsTrigPolynomial p) (hq : IsTrigPolynomial q) : IsTrigPolynomial fun (x : ℝ) => p x + q x

theorem FejerL1Density.isTrigPolynomial_smul (c : ℝ) {p : ℝ → ℝ} (hp : IsTrigPolynomial p) : IsTrigPolynomial fun (x : ℝ) => c * p x

theorem FejerL1Density.isTrigPolynomial_finset_sum {f : ℕ → ℝ → ℝ} {s : Finset ℕ} (hf : ∀ i ∈ s, IsTrigPolynomial (f i)) : IsTrigPolynomial fun (x : ℝ) => ∑ i ∈ s, f i x

theorem FejerL1Density.dirichlet_isTrigPolynomial (j : ℕ) : IsTrigPolynomial fun (x : ℝ) => 1 + 2 * ∑ k ∈ Finset.range j, Real.cos ((↑k + 1) * x)

theorem FejerL1Density.cos_eq_one_of_sin_half_eq_zero (x : ℝ) (h : Real.sin (x / 2) = 0) (n : ℕ) : Real.cos (↑n * x) = 1

theorem FejerL1Density.fejerKernel_eq_dirichlet_avg (N : ℕ) (hN : N ≠ 0) (x : ℝ) : fejerKernel N x = 1 / ↑N * ∑ j ∈ Finset.range N, (1 + 2 * ∑ k ∈ Finset.range j, Real.cos ((↑k + 1) * x))

theorem FejerL1Density.fejerKernel_isTrigPolynomial (N : ℕ) : IsTrigPolynomial (fejerKernel N)

theorem FejerL1Density.fxy_intervalIntegrable (f : ℝ → ℝ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf_intble : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (x : ℝ) : IntervalIntegrable (fun (y : ℝ) => f (x - y)) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.periodic_integral_shift (g : ℝ → ℝ) (hg : Function.Periodic g (2 * Real.pi)) (x : ℝ) : ∫ (y : ℝ) in -Real.pi..Real.pi, g (x - y) = ∫ (y : ℝ) in -Real.pi..Real.pi, g y

theorem FejerL1Density.single_term_convolution (f : ℝ → ℝ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf_intble : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (a b : ℝ) (n : ℕ) (x : ℝ) : ∫ (y : ℝ) in -Real.pi..Real.pi, f (x - y) * (a * Real.cos (↑n * y) + b * Real.sin (↑n * y)) = ((a * ∫ (t : ℝ) in -Real.pi..Real.pi, f t * Real.cos (↑n * t)) - b * ∫ (t : ℝ) in -Real.pi..Real.pi, f t * Real.sin (↑n * t)) * Real.cos (↑n * x) + ((a * ∫ (t : ℝ) in -Real.pi..Real.pi, f t * Real.sin (↑n * t)) + b * ∫ (t : ℝ) in -Real.pi..Real.pi, f t * Real.cos (↑n * t)) * Real.sin (↑n * x)

theorem FejerL1Density.fejerMean_isTrigPolynomial (f : ℝ → ℝ) (N : ℕ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf_intble : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) : IsTrigPolynomial (fejerMean f N)

theorem FejerL1Density.intble_diff_abs (f g : ℝ → ℝ) (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (hg_cont : Continuous g) (_hg_per : Function.Periodic g (2 * Real.pi)) : IntervalIntegrable (fun (x : ℝ) => |f x - g x|) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.intble_cts_conv (g : ℝ → ℝ) (N : ℕ) (hg_cont : Continuous g) (hg_per : Function.Periodic g (2 * Real.pi)) : IntervalIntegrable (fun (x : ℝ) => |g x - periodicConvolution g (fejerKernel N) x|) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.periodicConv_intervalIntegrable (f : ℝ → ℝ) (N : ℕ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) : IntervalIntegrable (periodicConvolution f (fejerKernel N)) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.intble_result (f : ℝ → ℝ) (N : ℕ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) : IntervalIntegrable (fun (x : ℝ) => |f x - fejerMean f N x|) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.intble_conv_diff (f g : ℝ → ℝ) (N : ℕ) (hf_per : Function.Periodic f (2 * Real.pi)) (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (hg_cont : Continuous g) (hg_per : Function.Periodic g (2 * Real.pi)) : IntervalIntegrable (fun (x : ℝ) => |periodicConvolution g (fejerKernel N) x - periodicConvolution f (fejerKernel N) x|) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.intble_diff (f g : ℝ → ℝ) (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) (hg_cont : Continuous g) (_hg_per : Function.Periodic g (2 * Real.pi)) : IntervalIntegrable (fun (x : ℝ) => g x - f x) MeasureTheory.volume (-Real.pi) Real.pi

theorem FejerL1Density.fejer_L1_convergence (f : ℝ → ℝ) (hf_periodic : Function.Periodic f (2 * Real.pi)) (hf_intble : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi) : Filter.Tendsto (fun (N : ℕ) => periodicL1Norm fun (x : ℝ) => f x - fejerMean f N x) Filter.atTop (nhds 0)