feat(Analysis/Fourier): the Plancherel theorem for the Clifford-Fourier transform#41922
feat(Analysis/Fourier): the Plancherel theorem for the Clifford-Fourier transform#41922junjihashimoto wants to merge 5 commits into
Conversation
…omplex structure The pseudoscalar of the Clifford algebra of Euclidean n-space squares to (-1)^(n.choose 2) and commutes with every element up to (-1)^(n-1); hence for n = 2, 3 mod 4 left multiplication by it is a complex structure (Module C via Complex.liftAux), and for n = 3 mod 4 the algebra is even a complex algebra. This makes the Clifford-Fourier transform an instance of the vector-valued Fourier transform (follow-up PR).
The Clifford-Fourier transform (Ebling-Scheuermann) replaces the imaginary unit in the Fourier kernel by the pseudoscalar of Cl(n,0). For n = 2, 3 mod 4 the pseudoscalar squares to -1, so left multiplication by the kernel is complex scalar multiplication for the pseudoscalar complex structure, and Plancherel's theorem and the Fourier inversion formula follow from the vector-valued L^2 Fourier theory.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 5bebe42782Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5016 | 2 | exposed public sections |
Current commit 5bebe42782
Reference commit 8c79cb4f54
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
|
This PR/issue depends on: |
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
junjihashimoto
changed the title
1 participant
The Clifford–Fourier transform (Ebling–Scheuermann, IEEE TVCG 2005; Brackx–De Schepper–Sommen, J. Fourier Anal. Appl. 2005) of
f : ℝⁿ → Cl(n,0)replaces the imaginary unit in the Fourier kernel by the pseudoscalarω:ℱ f ξ = ∫ x, (cos (2π ⟪x, ξ⟫) - sin (2π ⟪x, ξ⟫) ω) * f x.For
n ≡ 2, 3 [MOD 4]the pseudoscalar squares to-1(#41920), so left multiplication by the kernel is complex scalar multiplication for the pseudoscalar complex structure, and the Clifford–Fourier transform is literally the ordinary vector-valued Fourier transform (cliffordFourierIntegral_eq_fourier). Plancherel's theorem (integral_norm_sq_cliffordFourier), the Fourier inversion formula (cliffordFourierInv_cliffordFourier) and theL²isometry (cliffordFourierL2) are then inherited from the vector-valuedL²Fourier theory. The casen = 3is the transform used for 3D vector field analysis in visualization;n ≡ 2 [MOD 4]covers the two-dimensional (quaternionic-style) transform, where the pseudoscalar is not central.