theorem L2norm_sq_eq {T : ℝ} [hT : Fact (0 < T)] (f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }) : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂AddCircle.haarAddCircle

theorem fourierCoeff_eq_innerProduct {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ 2)] {f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }} {n : ℤ} : fourierCoeff (↑↑f) n = ⟪fourierLp 2 n, f⟫_ℂ

def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }) : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ p AddCircle.haarAddCircle }

Equations

• partialFourierSumLp p N f = ∑ n ∈ Finset.Icc (-Int.ofNat N) ↑N, fourierCoeff (↑↑f) n • fourierLp p n

theorem partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ 2)] {f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }} {N : ℕ} : ‖partialFourierSumLp 2 N f‖ ^ 2 = ∑ n ∈ Finset.Icc (-Int.ofNat N) ↑N, ‖fourierCoeff (↑↑f) n‖ ^ 2

theorem spectral_projection_bound_sq {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }) : ‖partialFourierSumLp 2 N f‖ ^ 2 ≤ ‖f‖ ^ 2

theorem spectral_projection_bound_sq_integral {N : ℕ} {T : ℝ} [hT : Fact (0 < T)] (f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }) : ∫ (t : AddCircle T), ‖↑↑(partialFourierSumLp 2 N f) t‖ ^ 2 ∂AddCircle.haarAddCircle ≤ ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle

theorem spectral_projection_bound {N : ℕ} {T : ℝ} [hT : Fact (0 < T)] (f : { x : AddCircle T →ₘ[AddCircle.haarAddCircle] ℂ // x ∈ MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle }) : ‖partialFourierSumLp 2 N f‖ ≤ ‖f‖