feat(Analysis/Fourier): the Plancherel theorem for hypercomplex Fourier transforms#41921
feat(Analysis/Fourier): the Plancherel theorem for hypercomplex Fourier transforms#41921junjihashimoto wants to merge 5 commits into
Conversation
Define the Cayley-Dickson double of a (possibly non-associative) star ring, and show that it preserves NonAssocRing and StarRing, so the construction iterates: quaternions -> octonions -> sedenions -> ... The doubling unit l = (0, 1) satisfies l * (l * x) = -x at every level of the tower, by a computation using only that star is an involution (no alternativity is developed). Left multiplication by l is therefore a complex structure on every Cayley-Dickson algebra.
…s on the Cayley-Dickson tower Cayley-Dickson algebras beyond the quaternions are not associative, but the Fourier theory only needs a complex module structure on the codomain: left multiplication by the doubling unit squares to -1 at every level of the tower, so Complex.liftAux into the endomorphism algebra makes every Cayley-Dickson algebra a complex vector space. Plancherel's theorem and the Fourier inversion formula for the left-sided hypercomplex Fourier transform then follow from the vector-valued L^2 theory, at every level of the tower, including the sedenions.
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 617900d3e2Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5017 | 3 | exposed public sections |
Current commit 617900d3e2
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. |
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
junjihashimoto
changed the title
1 participant
The (left-sided) hypercomplex Fourier transform of
f : V → CayleyDickson Areplaces the imaginary unit in the Fourier kernel by the Cayley–Dickson doubling unitℓ:ℱ f ξ = ∫ x, (cos (2π ⟪x, ξ⟫) - sin (2π ⟪x, ξ⟫) ℓ) * f x.Cayley–Dickson algebras beyond the quaternions are not associative — the sedenions are not even alternative and have zero divisors — but the Fourier theory only needs a complex module structure on the codomain:
ℓ * (ℓ * x) = -xholds at every level of the tower, soComplex.liftAuxintoModule.End ℝ (CayleyDickson A)(where associativity lives) makes every Cayley–Dickson algebra a complex vector space. Equipping it with a compatible complex Hilbert space structure, Plancherel's theorem (CayleyDickson.integral_norm_sq_fourierIntegral) and the Fourier inversion formula (CayleyDickson.fourierInvIntegral_fourierIntegral) are inherited from the vector-valuedL²Fourier theory (#24063-styleLp.fourierTransformₗᵢ), on any finite-dimensional real inner product space domain.Taking
A = ℍ[ℝ]gives the octonion Fourier transform (Hahn–Snopek; Błaszczyk, J. Fourier Anal. Appl. 2020);A = Octonion ℝgives the sedenion one, recorded explicitly asSedenion.integral_norm_sq_fourierIntegral.