Revision #1236 → #1829 · back to history
0b4f9a896074| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Definition","snippet":"The Fourier series of a complex-valued"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n=-\\infty }^{\\infty }c_{n}e^{i2\\pi {\\tfrac {n}{P}}x},}"},{"type":"math_alttext","value":"{\\displaystyle c_{n}={\\frac {1}{P}}\\int _{0}^{P}s(x)\\ e^{-i2\\pi {\\tfrac {n}{P}}x}\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle s(x)=\\sum _{n=-\\infty }^{\\infty }c_{n}e^{i2\\pi {\\tfrac {n}{P}}x}.}"}] | — |
9232fb6168bd| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Example","snippet":"Consider a sawtooth function"},{"type":"math_alttext","value":"{\\displaystyle s(x)=s(x+2\\pi k)={\\frac {x}{\\pi }},\\quad \\mathrm {for} -\\pi <x<\\pi ,{\\text{ and }}k\\in \\mathbb {Z} .}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}a_{0}&=0.\\\\a_{n}&={\\frac {1}{\\pi }}\\int _{-\\pi }^{\\pi }s(x)\\cos(nx)\\,dx=0,\\quad n\\geq 1.\\\\b_{n}&={\\frac {1}{\\pi }}\\int _{-\\pi }^{\\pi }s(x)\\sin(nx)\\,dx\\\\&=-{\\frac {2}{\\pi n}}\\cos(n\\pi )+{\\frac {2}{\\pi ^{2}n^{2}}}\\sin(n\\pi )\\\\&={\\frac {2\\,(-1)^{n+1}}{\\pi n}},\\quad n\\geq 1.\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}s(x)&=a_{0}+\\sum _{n=1}^{\\infty }\\left[a_{n}\\cos \\left(nx\\right)+b_{n}\\sin \\left(nx\\right)\\right]\\\\[4pt]&={\\frac {2}{\\pi }}\\sum _{n=1}^{\\infty }{\\frac {(-1)^{n+1}}{n}}\\sin(nx),\\quad \\mathrm {for} \\ (x-\\pi )\\ {\\text{is not a multiple of}}\\ 2\\pi .\\end{aligned}}}"}] | — |
eafee939ed8c1b0e3e96f61d| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Parseval's theorem","snippet":"periodic over an interval of length"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{P}}\\int _{P}|s(x)|^{2}\\,dx=\\sum _{n=-\\infty }^{\\infty }{\\Bigl |}S[n]{\\Bigr |}^{2}.}"}] | — |
3ece3568eb0b| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Convolution theorems","snippet":"discrete convolution of the"},{"type":"math_alttext","value":"{\\displaystyle h_{P}(x)\\triangleq s_{P}(x)\\cdot r_{P}(x)}"},{"type":"math_alttext","value":"{\\displaystyle H[n]=\\{S*R\\}[n].}"}] | — |
f5c80da46d36| Field | From #1236 | To #1829 |
|---|---|---|
| note | Mathlib has Fourier-transform convolution theorems (`Real.fourier_bilin_convolution_eq`) but no analogue for Fourier coefficients on `AddCircle T`. | Mathlib has Fourier-transform convolution theorems but no analogue for Fourier coefficients on `AddCircle T`. |
8888f184ca42| Field | From #1236 | To #1829 |
|---|---|---|
| note | No occurrence of Peter–Weyl was found in Mathlib. | No occurrence of Peter–Weyl was found in Mathlib (loogle confirms no decl name contains `PeterWeyl`). |
34150020f29e| Field | From #1236 | To #1829 |
|---|---|---|
| mathlib.module | Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality | Mathlib.Topology.Algebra.PontryaginDual |
| note | Mathlib handles the finite-abelian case via `PontryaginDuality`, but no general LCA-group Fourier transform is defined. | Mathlib defines `PontryaginDual` and develops the finite-abelian case in `Mathlib.Analysis.Fourier.FiniteAbelian`, but no general LCA-group Fourier transform is defined. |
b764d8363cd7| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Fourier-Stieltjes series","snippet":"the Fourier-Stieltjes series can be defined as the Fourier series whose coefficients are given by"},{"type":"math_alttext","value":"{\\displaystyle c_{n}={\\hat {\\mu }}(n)={\\frac {1}{P}}\\int _{0}^{P}\\ e^{-i2\\pi {\\tfrac {n}{P}}x}\\,d\\mu (x),\\quad \\forall n\\in \\mathbb {Z} ,}"}] | — |
5bd3a99f2f7f| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Fourier-Stieltjes series","snippet":"is a function of bounded variation"},{"type":"math_alttext","value":"{\\displaystyle c_{n}={\\frac {1}{P}}\\int _{0}^{P}\\ e^{-i2\\pi {\\tfrac {n}{P}}x}\\,dF(x),\\quad \\forall n\\in \\mathbb {Z} ,}"}] | — |
7b2efd74369d| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Fourier series on a square","snippet":"We can also define the Fourier series for functions of two variables"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}f(x,y)&=\\sum _{j,k\\in \\mathbb {Z} }c_{j,k}e^{ijx}e^{iky},\\\\[5pt]c_{j,k}&={\\frac {1}{4\\pi ^{2}}}\\int _{-\\pi }^{\\pi }\\int _{-\\pi }^{\\pi }f(x,y)e^{-ijx}e^{-iky}\\,dx\\,dy.\\end{aligned}}}"}] | — |
| mathlib.match_kind | generalization | exact |
| note | `AddCircleMulti` defines multivariate Fourier monomials `mFourier` and coefficients on `UnitAddTorus d`, generalizing the 2D-square case. | Verified via decl_exists: `UnitAddTorus.mFourierCoeff` does exist in `Mathlib.Analysis.Fourier.AddCircleMulti`, giving multivariate Fourier coefficients (covers the two-variable / unit-square case). |
| provenance | ai | ai-moderated |
612634fba63e| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Fourier series of a Bravais-lattice-periodic function","snippet":"A three-dimensional Bravais lattice is defined as the set of vectors"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {R} =n_{1}\\mathbf {a} _{1}+n_{2}\\mathbf {a} _{2}+n_{3}\\mathbf {a} _{3}}"}] | — |
| note | No definition of a Bravais lattice was found in Mathlib. | No definition of a Bravais lattice was found in Mathlib (loogle confirms no decl name contains `Bravais`). |
2e3c2253bc5d| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Fourier series of a Bravais-lattice-periodic function","snippet":"The Fourier series for"},{"type":"math_alttext","value":"{\\displaystyle g(x_{1},x_{2},x_{3})=\\sum _{m_{1},m_{2},m_{3}\\in \\mathbb {Z} }\\,c(m_{1},m_{2},m_{3})\\,e^{i2\\pi \\left({\\tfrac {m_{1}}{a_{1}}}x_{1}+{\\tfrac {m_{2}}{a_{2}}}x_{2}+{\\tfrac {m_{3}}{a_{3}}}x_{3}\\right)}.}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {a} _{i}\\cdot \\mathbf {b_{j}} =2\\pi \\delta _{ij},}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {Q} \\cdot \\mathbf {r} =\\left(m_{1}\\mathbf {b} _{1}+m_{2}\\mathbf {b} _{2}+m_{3}\\mathbf {b} _{3}\\right)\\cdot \\left(x_{1}{\\frac {\\mathbf {a} _{1}}{a_{1}}}+x_{2}{\\frac {\\mathbf {a} _{2}}{a_{2}}}+x_{3}{\\frac {\\mathbf {a} _{3}}{a_{3}}}\\right)=2\\pi \\left(x_{1}{\\frac {m_{1}}{a_{1}}}+x_{2}{\\frac {m_{2}}{a_{2}}}+x_{3}{\\frac {m_{3}}{a_{3}}}\\right),}"},{"type":"math_alttext","value":"{\\displaystyle f(\\mathbf {r} )=\\sum _{\\mathbf {Q} }c(\\mathbf {Q} )\\,e^{i\\mathbf {Q} \\cdot \\mathbf {r} },}"},{"type":"math_alttext","value":"{\\displaystyle c(\\mathbf {Q} )={\\frac {1}{a_{3}}}\\int _{0}^{a_{3}}dx_{3}\\,{\\frac {1}{a_{2}}}\\int _{0}^{a_{2}}dx_{2}\\,{\\frac {1}{a_{1}}}\\int _{0}^{a_{1}}dx_{1}\\,f\\left(x_{1}{\\frac {\\mathbf {a} _{1}}{a_{1}}}+x_{2}{\\frac {\\mathbf {a} _{2}}{a_{2}}}+x_{3}{\\frac {\\mathbf {a} _{3}}{a_{3}}}\\right)e^{-i\\mathbf {Q} \\cdot \\mathbf {r} }.}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {r} =x_{1}{\\frac {\\mathbf {a} _{1}}{a_{1}}}+x_{2}{\\frac {\\mathbf {a} _{2}}{a_{2}}}+x_{3}{\\frac {\\mathbf {a} _{3}}{a_{3}}},}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}x\\\\y\\\\z\\end{bmatrix}}=\\mathbf {J} {\\begin{bmatrix}x_{1}\\\\x_{2}\\\\x_{3}\\end{bmatrix}}={\\begin{bmatrix}{\\frac {\\mathbf {a} _{1}}{a_{1}}},{\\frac {\\mathbf {a} _{2}}{a_{2}}},{\\frac {\\mathbf {a} _{3}}{a_{3}}}\\end{bmatrix}}{\\begin{bmatrix}x_{1}\\\\x_{2}\\\\x_{3}\\end{bmatrix}}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {J} ={\\begin{bmatrix}{\\dfrac {\\partial x}{\\partial x_{1}}}&{\\dfrac {\\partial x}{\\partial x_{2}}}&{\\dfrac {\\partial x}{\\partial x_{3}}}\\\\[12pt]{\\dfrac {\\partial y}{\\partial x_{1}}}&{\\dfrac {\\partial y}{\\partial x_{2}}}&{\\dfrac {\\partial y}{\\partial x_{3}}}\\\\[12pt]{\\dfrac {\\partial z}{\\partial x_{1}}}&{\\dfrac {\\partial z}{\\partial x_{2}}}&{\\dfrac {\\partial z}{\\partial x_{3}}}\\end{bmatrix}}\\,.}"}] | — |
e33cfc42c620| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Hilbert space","snippet":"the space of square-integrable functions"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle ={\\frac {1}{2\\pi }}\\int _{-\\pi }^{\\pi }f(x){\\overline {g(x)}}\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle f(x)=\\sum _{n=-\\infty }^{\\infty }c_{n}e^{inx},}"},{"type":"math_alttext","value":"{\\displaystyle f=\\sum _{n=-\\infty }^{\\infty }\\langle f,e_{n}\\rangle \\,e_{n}.}"}] | — |
c07f083d3f4a| Field | From #1236 | To #1829 |
|---|---|---|
| anchors | [{"section":"Hilbert space","snippet":"the sines and cosines form an orthogonal set"},{"type":"math_alttext","value":"{\\displaystyle \\int _{-\\pi }^{\\pi }\\cos(mx)\\,\\cos(nx)\\,dx={\\frac {1}{2}}\\int _{-\\pi }^{\\pi }\\cos((n-m)x)+\\cos((n+m)x)\\,dx=\\pi \\delta _{mn},\\quad m,n\\geq 1,}"},{"type":"math_alttext","value":"{\\displaystyle \\int _{-\\pi }^{\\pi }\\sin(mx)\\,\\sin(nx)\\,dx={\\frac {1}{2}}\\int _{-\\pi }^{\\pi }\\cos((n-m)x)-\\cos((n+m)x)\\,dx=\\pi \\delta _{mn},\\quad m,n\\geq 1}"},{"type":"math_alttext","value":"{\\displaystyle \\int _{-\\pi }^{\\pi }\\cos(mx)\\,\\sin(nx)\\,dx={\\frac {1}{2}}\\int _{-\\pi }^{\\pi }\\sin((n+m)x)+\\sin((n-m)x)\\,dx=0;}"},{"type":"math_alttext","value":"{\\displaystyle \\left\\{{\\frac {1}{\\sqrt {2}}},{\\frac {\\cos x}{\\sqrt {2}}},{\\frac {\\sin x}{\\sqrt {2}}},\\dots ,{\\frac {\\cos(nx)}{\\sqrt {2}}},{\\frac {\\sin(nx)}{\\sqrt {2}}},\\dots \\right\\},}"}] | — |
| mathlib.decl | orthonormal_fourier | fourierBasis |
| note | Mathlib proves orthonormality of complex exponentials (`orthonormal_fourier`) and that they form a Hilbert basis, but not the real sin/cos version explicitly. | Mathlib proves the complex-exponential Fourier basis is a Hilbert basis (orthonormality via `fourierBasis`), but the real sin/cos orthonormal basis is not packaged as a named lemma. |
| provenance | ai | ai-moderated |
1f2bab3c744342e9e7776043ca0f90ade0f8| Field | From #1236 | To #1829 |
|---|---|---|
| mathlib.module | Mathlib.Analysis.InnerProductSpace.L2Space | Mathlib.Analysis.InnerProductSpace.l2Space |
2aa4c91a25eb| Field | From #1236 | To #1829 |
|---|---|---|
| note | Carleson's theorem on a.e. convergence of L² Fourier series is not present in Mathlib. | Carleson's theorem on a.e. convergence of L² Fourier series is not present in Mathlib (loogle confirms no decl name contains `Carleson`). |
a237cb58b7d6