theorem
L2norm_sq_eq
{T : ℝ}
[hT : Fact (0 < T)]
(f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle))
:
theorem
fourierCoeff_eq_innerProduct
{T : ℝ}
[hT : Fact (0 < T)]
[h2 : Fact (1 ≤ 2)]
{f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)}
{n : ℤ}
:
theorem
partialFourierSumL2_norm
{T : ℝ}
[hT : Fact (0 < T)]
[h2 : Fact (1 ≤ 2)]
{f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)}
{N : ℕ}
:
theorem
spectral_projection_bound_sq
{T : ℝ}
[hT : Fact (0 < T)]
(N : ℕ)
(f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle))
:
theorem
spectral_projection_bound_sq_integral
{N : ℕ}
{T : ℝ}
[hT : Fact (0 < T)]
(f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle))
:
theorem
spectral_projection_bound_lp
{N : ℕ}
{T : ℝ}
[hT : Fact (0 < T)]
(f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle))
: