Revision #1237 → #1828 · back to history
modifiedFourier transform (integral definition)4471d8abf2f8
| Field | From #1237 | To #1828 |
|---|
| mathlib.decl | Real.fourierIntegral | Fourier.fourierIntegral |
| note | `Real.fourierIntegral` (specialization of `VectorFourier.fourierIntegral` with the standard additive character `𝐞`) defines the Fourier integral exactly as in the article. | `Fourier.fourierIntegral` (with the explicit unfolding `Real.fourierIntegral_eq`) defines the Fourier integral on ℝ via the standard additive character `Real.fourierChar`, exactly as in the article. |
modifiedFourier inversion theorem9924f548f253
| Field | From #1237 | To #1828 |
|---|
| note | `MeasureTheory.Integrable.fourierInv_fourier_eq` and `Continuous.fourierInv_fourier_eq` give the Fourier inversion formula on finite-dimensional real inner product spaces. | `MeasureTheory.Integrable.fourierInv_fourier_eq` gives the Fourier inversion formula on finite-dimensional real inner product spaces. |
modifiedFourier transform of the delta functionc35b2c3a228b
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Definition","snippet":"the Fourier transform of the delta function is the constant function"},{"type":"math_alttext","value":"{\\displaystyle f(x)\\ {\\stackrel {\\mathcal {F}}{\\longleftrightarrow }}\\ {\\widehat {f}}(\\xi ).}"},{"type":"math_alttext","value":"{\\displaystyle \\delta (x)\\ {\\stackrel {\\mathcal {F}}{\\longleftrightarrow }}\\ 1.}"}] | — |
| note | `TemperedDistribution.fourier_delta_zero` states `𝓕 (delta 0) = volume.toTemperedDistribution`, i.e. the Fourier transform of δ is the constant 1 distribution. | `TemperedDistribution.fourier_delta_zero` states `𝓕 (delta 0) = volume.toTemperedDistribution`, i.e. the Fourier transform of δ is the constant-1 distribution. |
modifiedAngular-frequency conventionac5f342614b6
| Field | From #1237 | To #1828 |
|---|
| note | Mathlib's Fourier transform uses the ordinary-frequency (2π) convention via `fourierChar`; no separate angular-frequency variant `𝓕(f)(ω) = ∫ f(x) e^{-iωx} dx` is defined. | Mathlib's Fourier transform uses the ordinary-frequency (2π) convention via `Real.fourierChar`; no separate angular-frequency variant `𝓕(f)(ω) = ∫ f(x) e^{-iωx} dx` is defined. |
modifiedLebesgue integrable function99debabd1c88
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Lebesgue integrable functions","snippet":"is called (Lebesgue) integrable if the Lebesgue integral of its absolute value is finite"},{"type":"math_alttext","value":"{\\displaystyle \\|f\\|_{1}=\\int _{\\mathbb {R} }|f(x)|\\,dx<\\infty .}"}] | — |
modifiedL^p space6cc48b00b91d
| Field | From #1237 | To #1828 |
|---|
| note | `MeasureTheory.Lp E p μ` (and `MeasureTheory.MemLp`) define the L^p spaces of measurable functions with finite p-seminorm. | `MeasureTheory.Lp E p μ` defines the L^p spaces of measurable functions with finite p-seminorm. |
modifiedFourier transform is a Banach-algebra homomorphismc103eb5edb40
| Field | From #1237 | To #1828 |
|---|
| note | The ingredients exist — linearity (`fourier_add`/`fourier_smul`), L¹-norm bound (`norm_fourierIntegral_le_integral_norm`), and convolution-to-multiplication (`Real.fourier_mul_convolution_eq`) — but Mathlib does not package the L¹ Fourier transform as a Banach-algebra homomorphism. | The ingredients exist — linearity, L¹-norm bound, and convolution-to-multiplication (`Real.fourier_mul_convolution_eq`) — but Mathlib does not package the L¹ Fourier transform as a Banach-algebra homomorphism. |
modifiedSymmetry of FT for real-valued functionsc911d40d6e79
| Field | From #1237 | To #1828 |
|---|
| note | Mathlib has no named lemma `𝓕(f)(-ξ) = conj(𝓕(f)(ξ))` for real-valued `f` (Hermitian symmetry); grep finds no such conjugation/negation symmetry result for the Fourier integral. | Mathlib has no named lemma `𝓕(f)(-ξ) = conj(𝓕(f)(ξ))` for real-valued `f` (Hermitian symmetry). |
modifiedFourier transform of a periodic functionccd3b1589a2f
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Fourier transform for periodic functions","snippet":"the Fourier transform is a Dirac comb function whose teeth are multiplied by the Fourier series coefficients"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f}}(\\xi )=\\sum _{n=-\\infty }^{\\infty }c_{n}\\cdot \\delta \\left(\\xi -{\\tfrac {n}{P}}\\right),}"}] | — |
modifiedPoisson summation formula for sampled FT67e92293c3d4
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Sampling the Fourier transform","snippet":"These samples can be deduced from one cycle of a periodic function"},{"type":"math_alttext","value":"{\\displaystyle f_{P}(x)\\triangleq \\sum _{n=-\\infty }^{\\infty }f(x+nP)={\\frac {1}{P}}\\sum _{k=-\\infty }^{\\infty }{\\widehat {f}}\\left({\\tfrac {k}{P}}\\right)e^{i2\\pi {\\frac {k}{P}}x},\\quad \\forall k\\in \\mathbb {Z} .}"}] | — |
| note | Classical Poisson summation `∑ f(n) = ∑ 𝓕(f)(n)` is in `Real.tsum_eq_tsum_fourier`, which is the underlying identity but not phrased in terms of FT samples vs. periodization. | Classical Poisson summation `∑ f(n) = ∑ 𝓕(f)(n)` is in `Real.tsum_eq_tsum_fourier`, the underlying identity but not phrased in terms of FT samples vs. periodization. |
modifiedTime-reversal property1470ff6ff665
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Time scaling","snippet":"leads to the time-reversal property"},{"type":"math_alttext","value":"{\\displaystyle f(ax)\\ \\ {\\stackrel {\\mathcal {F}}{\\Longleftrightarrow }}\\ \\ {\\frac {1}{|a|}}{\\widehat {f}}\\left({\\frac {\\xi }{a}}\\right);\\quad \\ a\\neq 0}"},{"type":"math_alttext","value":"{\\displaystyle f(-x)\\ \\ {\\stackrel {\\mathcal {F}}{\\Longleftrightarrow }}\\ \\ {\\widehat {f}}(-\\xi )}"}] | — |
| note | `Real.fourierInv_eq_fourier_comp_neg` (and `fourierInv_eq_fourier_neg`) encode `𝓕⁻¹ f (w) = 𝓕 f (-w)`, equivalent to the time-reversal property; no separate `𝓕(f∘neg) = 𝓕(f)∘neg` lemma was found. | `Real.fourierInv_eq_fourier_comp_neg` encodes `𝓕⁻¹ f = 𝓕 f ∘ neg`, equivalent to the time-reversal property; no separate `𝓕(f∘neg) = 𝓕(f)∘neg` lemma was found. |
modifiedFT of a real function is conjugate symmetric (Hermitian)5ce92dbf0bce
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Conjugation","snippet":"is conjugate symmetric ( a.k.a. Hermitian function )"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f}}(-\\xi )={\\bigl (}{\\widehat {f}}(\\xi ){\\bigr )}^{*}.}"}] | — |
modifiedZero-frequency component equals total mass / DC bias73766a0664ed
| Field | From #1237 | To #1828 |
|---|
| note | Although the statement is immediate from `fourierIntegral_def` (since `𝐞(0)=1`), there is no dedicated `fourierIntegral_zero_eq_integral` lemma in Mathlib. | Although the statement is immediate from the definition (since `Real.fourierChar 0 = 1`), there is no dedicated `fourierIntegral_zero_eq_integral` lemma in Mathlib. |
modifiedUniform continuity of FT of integrable function6b0008d92fd8
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Uniform continuity and the Riemann–Lebesgue lemma","snippet":"of any integrable function"},{"type":"math_alttext","value":"{\\displaystyle \\left\\|{\\widehat {f}}\\right\\|_{\\infty }\\leq \\left\\|f\\right\\|_{1}}"}] | — |
modifiedRiemann–Lebesgue lemma35cb599dea39
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Uniform continuity and the Riemann–Lebesgue lemma","snippet":"By the Riemann–Lebesgue lemma"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f}}(\\xi )\\to 0{\\text{ as }}|\\xi |\\to \\infty .}"}] | — |
| note | `Real.zero_at_infty_fourier` and `Real.zero_at_infty_vector_fourierIntegral` state that `𝓕 f → 0` at cocompact infinity for `f ∈ L¹`. | `Real.zero_at_infty_fourier` states that `𝓕 f → 0` at cocompact infinity for `f ∈ L¹`. |
modifiedInjectivity of FT on L^1(R)d47e84d1b039
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Uniform continuity and the Riemann–Lebesgue lemma","snippet":"the Fourier transform is injective on L 1 ( R )"},{"type":"math_alttext","value":"{\\displaystyle f(x)=\\int _{-\\infty }^{\\infty }{\\widehat {f}}(\\xi )e^{i2\\pi x\\xi }\\,d\\xi }"}] | — |
modifiedParseval's formula4bd2a36ad6ba
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Plancherel theorem and Parseval's theorem","snippet":"the Parseval formula follows"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle _{L^{2}}=\\int _{-\\infty }^{\\infty }f(x){\\overline {g(x)}}\\,dx=\\int _{-\\infty }^{\\infty }{\\widehat {f}}(\\xi ){\\overline {{\\widehat {g}}(\\xi )}}\\,d\\xi ,}"}] | — |
modifiedPlancherel theoremd45e7a58e9ea
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Plancherel theorem and Parseval's theorem","snippet":"The Plancherel theorem , which follows from the above, states that"},{"type":"math_alttext","value":"{\\displaystyle \\|f\\|_{L^{2}}^{2}=\\int _{-\\infty }^{\\infty }\\left|f(x)\\right|^{2}\\,dx=\\int _{-\\infty }^{\\infty }\\left|{\\widehat {f}}(\\xi )\\right|^{2}\\,d\\xi .}"}] | — |
| note | `MeasureTheory.Lp.fourierTransformₗᵢ` packages the Fourier transform on L² as a `LinearIsometryEquiv` (Plancherel), with the norm identity proved as `Lp.norm_fourier_eq`. | `MeasureTheory.Lp.fourierTransformₗᵢ` packages the Fourier transform on L² as a `LinearIsometryEquiv`, the formalization of the Plancherel theorem. |
modifiedConvolution theoremf580299fb312
| Field | From #1237 | To #1828 |
|---|
| note | `Real.fourier_mul_convolution_eq` (and the bilinear variant `fourier_bilin_convolution_eq`) prove `𝓕 (f ⋆ g) = 𝓕 f · 𝓕 g`. | `Real.fourier_mul_convolution_eq` proves `𝓕 (f ⋆ g) = 𝓕 f · 𝓕 g`. |
modifiedCross-correlation theorem944fc5a529db
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Cross-correlation theorem","snippet":"is the cross-correlation of"},{"type":"math_alttext","value":"{\\displaystyle h(x)=(f\\star g)(x)=\\int _{-\\infty }^{\\infty }{\\overline {f(y)}}g(x+y)\\,dy}"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {h}}(\\xi )={\\overline {{\\widehat {f}}(\\xi )}}\\,{\\widehat {g}}(\\xi ).}"}] | — |
modifiedFT of a derivative94ca1b65e6e6
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Differentiation","snippet":"Then the Fourier transform of the derivative is given by"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f'}}(\\xi )={\\mathcal {F}}\\left\\{{\\frac {d}{dx}}f(x)\\right\\}=i2\\pi \\xi {\\widehat {f}}(\\xi ).}"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f^{(n)}}}(\\xi )={\\mathcal {F}}\\left\\{{\\frac {d^{n}}{dx^{n}}}f(x)\\right\\}=(i2\\pi \\xi )^{n}{\\widehat {f}}(\\xi ).}"}] | — |
| note | `VectorFourier.fourierIntegral_fderiv` and `fourierIntegral_iteratedFDeriv` give the formula `𝓕(f') = 2πiξ · 𝓕 f` in the general vector-valued setting. | `VectorFourier.fourierIntegral_fderiv` gives the formula `𝓕(f') = 2πiξ · 𝓕 f` in the general vector-valued setting. |
modifiedEigenfunctions of the Fourier transform01fa2b067499
| Field | From #1237 | To #1828 |
|---|
| note | Mathlib proves that the Gaussian is fixed by the Fourier transform (`fourier_gaussian_pi`, `fourier_gaussian_innerProductSpace`) but does not develop a general theory of FT eigenfunctions. | Mathlib proves that the Gaussian is fixed by the Fourier transform (`fourier_gaussian_innerProductSpace`) but does not develop a general theory of FT eigenfunctions. |
modifiedFour-periodicity / Fourier inversion theoremc5518cfe2839
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Inversion and periodicity","snippet":"the various forms of the Fourier inversion theorem"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}{\\mathcal {F}}^{0}&=\\mathrm {id} ,\\\\{\\mathcal {F}}^{1}&={\\mathcal {F}},\\\\{\\mathcal {F}}^{2}&={\\mathcal {P}},\\\\{\\mathcal {F}}^{3}&={\\mathcal {F}}^{-1}={\\mathcal {P}}\\circ {\\mathcal {F}}={\\mathcal {F}}\\circ {\\mathcal {P}},\\\\{\\mathcal {F}}^{4}&=\\mathrm {id} \\end{aligned}}}"}] | — |
modifiedStone–von Neumann realization of FT as intertwiner1bf4c1e969ff
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Connection with the Heisenberg group","snippet":"According to the Stone–von Neumann theorem"},{"type":"math_alttext","value":"{\\displaystyle \\rho \\circ j=W\\rho W^{*}.}"}] | — |
| note | Neither the Heisenberg group nor the Stone–von Neumann theorem appear in Mathlib. | Neither the Heisenberg group nor the Stone–von Neumann theorem appears in Mathlib. |
modifiedPaley–Wiener theorema1b997905c4e
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Complex domain","snippet":"The Paley–Wiener theorem says that f is smooth"},{"type":"math_alttext","value":"{\\displaystyle \\left\\vert \\xi ^{n}{\\widehat {f}}(\\xi )\\right\\vert \\leq C_{n}e^{2\\pi a\\vert \\tau \\vert }}"}] | — |
modifiedRelation between FT and Laplace transformab4e357f848b
| Field | From #1237 | To #1828 |
|---|
| note | The Laplace transform is not defined in Mathlib (no `Laplace.?[Tt]ransform` matches), so a relation to it cannot be stated. | The Laplace transform is not defined in Mathlib, so a relation to it cannot be stated. |
modifiedComplex-line inversion for causal exponentially-bounded functions71523894c260
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Inversion","snippet":"Theorem: If f ( t ) = 0 for t < 0"},{"type":"math_alttext","value":"{\\displaystyle f(t)=\\int _{-\\infty }^{\\infty }{\\widehat {f}}(\\sigma +i\\tau )e^{i2\\pi (\\sigma +i\\tau )t}\\,d\\sigma ,}"}] | — |
modifiedMellin inversion formula for the Laplace transformf6bae1c67f4a
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Inversion","snippet":"This theorem implies the Mellin inversion formula for the Laplace transformation"},{"type":"math_alttext","value":"{\\displaystyle f(t)={\\frac {1}{i2\\pi }}\\int _{b-i\\infty }^{b+i\\infty }F(s)e^{st}\\,ds}"}] | — |
| note | Mathlib has `mellin_inversion` (`mellinInv_mellin_eq`) for the Mellin transform itself, but no derivation as an inversion formula for the (absent) Laplace transform. | Mathlib has `mellin_inversion` for the Mellin transform itself, but no derivation as an inversion formula for the (absent) Laplace transform. |
modifiedFourier transform on Euclidean space R^nb4481759ba44
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Fourier transform on Euclidean space","snippet":"The Fourier transform can be defined in any arbitrary number of dimensions"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f}}({\\boldsymbol {\\xi }})={\\mathcal {F}}(f)({\\boldsymbol {\\xi }})=\\int _{\\mathbb {R} ^{n}}f(\\mathbf {x} )e^{-i2\\pi {\\boldsymbol {\\xi }}\\cdot \\mathbf {x} }\\,d\\mathbf {x} }"}] | — |
modifiedUncertainty principlea370fdde3dbb
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Uncertainty principle","snippet":"The uncertainty principle states that"},{"type":"math_alttext","value":"{\\displaystyle D_{0}(f)D_{0}({\\widehat {f}})\\geq {\\frac {1}{16\\pi ^{2}}}.}"}] | — |
modifiedHirschman uncertainty principle314178965231
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Uncertainty principle","snippet":"A stronger uncertainty principle is the Hirschman uncertainty principle"},{"type":"math_alttext","value":"{\\displaystyle H\\left(\\left|f\\right|^{2}\\right)+H\\left(\\left|{\\widehat {f}}\\right|^{2}\\right)\\geq \\log \\left({\\frac {e}{2}}\\right)}"},{"type":"math_alttext","value":"{\\displaystyle H(p)=-\\int _{-\\infty }^{\\infty }p(x)\\log {\\bigl (}p(x){\\bigr )}\\,dx}"}] | — |
modifiedFourier integral expansion (sine/cosine form)4df5170df257
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Sine and cosine transforms","snippet":"This is called an expansion as a trigonometric integral"},{"type":"math_alttext","value":"{\\displaystyle a(\\lambda )=2\\int _{-\\infty }^{\\infty }f(t)\\cos(2\\pi \\lambda t)\\,dt}"},{"type":"math_alttext","value":"{\\displaystyle b(\\lambda )=2\\int _{-\\infty }^{\\infty }f(t)\\sin(2\\pi \\lambda t)\\,dt.}"}] | — |
| note | No sine / cosine transform definitions are present (grep `(F|f)ourier(S|s)ine` / `(C|c)osine` returns nothing). | No sine / cosine transform definitions are present in Mathlib. |
modifiedFefferman's ball multiplier theoremfc6f835c686a
| Field | From #1237 | To #1828 |
|---|
| note | No Fefferman ball-multiplier result is in Mathlib (`Fefferman` only appears in a tactic file). | No Fefferman ball-multiplier result is in Mathlib. |
modifiedExtension of FT to L^211f4616457cf
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Fourier transform on function spaces","snippet":"The definition of the Fourier transform naturally extends from"},{"type":"math_alttext","value":"{\\displaystyle f(x)\\mapsto {\\widehat {f}}(\\xi )=\\int _{\\mathbb {R} ^{n}}f(x)e^{-i2\\pi \\xi \\cdot x}\\,dx,\\quad \\forall \\xi \\in \\mathbb {R} ^{n}.}"},{"type":"math_alttext","value":"{\\displaystyle \\sup _{\\xi \\in \\mathbb {R} ^{n}}\\left\\vert {\\widehat {f}}(\\xi )\\right\\vert \\leq \\int _{\\mathbb {R} ^{n}}\\vert f(x)\\vert \\,dx,}"}] | — |
modifiedFT on L^2 is unitarya6ba7126e8b7
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Fourier transform on function spaces","snippet":"is a unitary operator"},{"type":"math_alttext","value":"{\\displaystyle \\int _{\\mathbb {R} ^{n}}f(x){\\mathcal {F}}g(x)\\,dx=\\int _{\\mathbb {R} ^{n}}{\\mathcal {F}}f(x)g(x)\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\int _{\\mathbb {R} ^{n}}{\\overline {{\\mathcal {F}}f(x)}}{\\mathcal {F}}g(x)\\,dx&=\\int _{\\mathbb {R} ^{n}}{\\mathcal {F}}^{-1}{\\overline {f(x)}}{\\mathcal {F}}g(x)\\,dx\\\\&=\\int _{\\mathbb {R} ^{n}}{\\mathcal {F}}{\\mathcal {F}}^{-1}{\\overline {f(x)}}g(x)\\,dx=\\int _{\\mathbb {R} ^{n}}{\\overline {f(x)}}g(x)\\,dx\\end{aligned}}}"}] | — |
| note | `MeasureTheory.Lp.fourierTransformₗᵢ` is a `LinearIsometryEquiv`, which on a Hilbert space is exactly a unitary operator; `Lp.norm_fourier_eq` records norm preservation. | `MeasureTheory.Lp.fourierTransformₗᵢ` is a `LinearIsometryEquiv`, which on a Hilbert space is exactly a unitary operator. |
modifiedFourier transform of a tempered distributionbe8236da751c
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Tempered distributions","snippet":"The Fourier transform can also be defined for tempered distributions"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {F}}:C_{c}^{\\infty }(\\mathbb {R} ^{n})\\rightarrow {\\mathcal {S}}(\\mathbb {R} ^{n})\\setminus C_{c}^{\\infty }(\\mathbb {R} ^{n}).}"}] | — |
| note | The Fourier transform on `𝓢'(E, F)` is defined via `𝓕 f g = f (𝓕 g)` (see `fourier_apply`), and an instance is registered making `𝓕` available on tempered distributions. | The Fourier transform on `𝓢'(E, F)` is defined via `𝓕 f g = f (𝓕 g)` (see `TemperedDistribution.fourier_apply`). |
addedFourier transform is an automorphism of the Schwartz space7ebc2bbc555e
modifiedFourier–Stieltjes transform of a finite Borel measure015f3a436134
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Fourier–Stieltjes transform on measurable spaces","snippet":"The Fourier transform of a finite Borel measure"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {\\mu }}(\\xi )=\\int _{\\mathbb {R} ^{n}}e^{-i2\\pi x\\cdot \\xi }\\,d\\mu ,}"},{"type":"math_alttext","value":"{\\displaystyle d\\mu =f(x)\\,dx,}"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {\\mu }}(\\xi )={\\widehat {f}}(\\xi ),}"}] | — |
| note | `charFun μ t = ∫ x, exp(⟪x,t⟫ * I) ∂μ` is the characteristic function / Fourier–Stieltjes transform of a finite measure (also `charFun_eq_fourierIntegral` connects it explicitly to `𝓕`). | `MeasureTheory.charFun μ t = ∫ x, exp(⟪x,t⟫ * I) ∂μ` is the characteristic function / Fourier–Stieltjes transform of a finite measure. |
addedPontryagin dual of a locally compact abelian group9544db6f7f80
modifiedFourier transform on a locally compact abelian groupa686ba9a3c22
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Locally compact abelian groups","snippet":"The Fourier transform may be generalized to any locally compact abelian group"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {f}}(\\xi )=\\int _{G}{\\overline {\\xi (x)}}f(x)\\,d\\mu \\quad {\\text{for any }}\\xi \\in {\\widehat {G}}.}"}] | — |
| note | Mathlib defines `PontryaginDual A` (continuous homs `A →* Circle`) but does not develop the Fourier transform `L¹(G) → C₀(Ĝ)` for general LCA groups; only the Euclidean and finite-abelian cases are formalized. | Mathlib defines `PontryaginDual A` but does not develop the Fourier transform `L¹(G) → C₀(Ĝ)` for general LCA groups; only the Euclidean and finite-abelian cases are formalized. |
modifiedPeter–Weyl theorem and Plancherel formula6fec0c98e945
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Compact non-abelian groups","snippet":"The Peter–Weyl theorem holds"},{"type":"math_alttext","value":"{\\displaystyle f(g)=\\sum _{\\sigma \\in \\Sigma }d_{\\sigma }\\operatorname {tr} \\left({\\widehat {f}}(\\sigma )U_{g}^{(\\sigma )}\\right),}"},{"type":"math_alttext","value":"{\\displaystyle \\|f\\|_{2}^{2}=\\sum _{\\sigma \\in \\Sigma }d_{\\sigma }\\|{\\widehat {f}}(\\sigma )\\|_{\\mathrm {HS} }^{2},}"}] | — |
modifiedSolving the wave equation via Fourier transform92ad827b8851
| Field | From #1237 | To #1828 |
|---|
| anchors | [{"section":"Analysis of differential equations","snippet":"Perhaps the most important use of the Fourier transformation is to solve partial differential equations"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\partial ^{2}y(x,t)}{\\partial ^{2}x}}={\\frac {\\partial y(x,t)}{\\partial t}}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\partial ^{2}y(x,t)}{\\partial ^{2}x}}={\\frac {\\partial ^{2}y(x,t)}{\\partial ^{2}t}}.}"}] | — |
| note | No wave-equation (or general PDE) solution via Fourier transform is formalized in Mathlib (`waveEquation` / `wave_equation` grep returns nothing). | No wave-equation (or general PDE) solution via Fourier transform is formalized in Mathlib. |