theorem L2norm_sq_eq {T : ℝ} [hT : Fact (0 < T)] (f : ↥(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 : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)} {n : ℤ} : fourierCoeff (↑↑f) n = inner (fourierLp 2 n) f

def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : ↥(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 : ↥(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 : ↥(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 : ↥(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 : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : ‖partialFourierSumLp 2 N f‖ ≤ ‖f‖