Theorems · Definition · harmonic analysis
fourierCoeff
- #76 of the 100 theorems: Fourier Series
{T : ℝ} →
[hT : Fact (0 < T)] → {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (AddCircle T → E) → ℤ → EThe n-th Fourier coefficient of a function AddCircle T → E, for E a complete normed
ℂ-vector space, defined as the integral over AddCircle T of fourier (-n) t • f t.
- Defined in
- Mathlib.Analysis.Fourier.AddCircle
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 250 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Complexstatement and proof · cited by 5,565
- Factstatement and proof · cited by 2,726
- MeasureTheory.integralproof · cited by 1,779
- AddCirclestatement and proof · cited by 189
- fourierproof · cited by 62
- AddCircle.haarAddCircleproof · cited by 28
Cited by27
Results whose statement or proof uses this declaration.
- fourierCoeffOnproof · cited by 13
- fourierCoeff_eq_intervalIntegralstatement and proof · cited by 4
- fourierCoeff.const_smulstatement · cited by 3
- Polynomial.fourierCoeff_toAddCirclestatement and proof · cited by 3
- fourierCoeff_toLpstatement · cited by 2
- hasSum_sq_fourierCoeffstatement · cited by 2
- fourierCoeff.addstatement · cited by 2
- has_pointwise_sum_fourier_series_of_summablestatement and proof · cited by 2
- fourierCoeff_congr_aestatement · cited by 2
- Polynomial.sum_sq_norm_coeff_eq_circleAverageproof · cited by 1
- hasSum_one_div_pow_mul_fourier_mul_bernoulliFunproof · cited by 1
- Real.tsum_eq_tsum_fourierproof · cited by 1