Conversation
toh995
commented
Sep 13, 2026
| - Notes: The Fourier slice theorem diagonalizes the Radon transform (1D Fourier of a projection = a 2D-Fourier slice), and the transform has a left inverse on Schwartz functions. Trusted helpers radon, fourier1, fourier2 (non-holes). Mathlib has the 1D/2D Fourier transforms and Schwartz space but no Radon transform, Fourier slice theorem, or filtered back-projection. The pseudo-inverse is stated existentially (the explicit filtered-back-projection form would need the Hilbert transform / Riesz potential). Candidate from §100 of the Knill survey. | ||
| - Source: J. Radon (1917); R. N. Bracewell (Fourier slice theorem, 1956). Knill, *Some fundamental theorems in mathematics*, §100. | ||
| - Informal solution: Fourier slice theorem: writing the Radon projection R f(p,θ) and taking its 1D Fourier transform in p, interchange integrals (Fubini) and change variables so the line-integral-then-Fourier becomes the 2D Fourier transform of f restricted to the line through the origin at angle θ: F₁[Rf(·,θ)](k) = F₂[f](k cos θ, k sin θ). This diagonalizes R (it becomes a slice/multiplication operator). Pseudo-inversion: the slice identity plus 2D Fourier inversion on Schwartz functions makes R injective on 𝓢, so a left inverse exists; the canonical one is filtered back-projection u ↦ backproject(Hilbert-filter(u)). Mathlib lacks the slice theorem and the filter. | ||
| - Informal solution: Fourier slice theorem: writing the Radon projection R f(p,θ) and taking its 1D Fourier transform in p, interchange integrals (Fubini) and change variables so the line-integral-then-Fourier becomes the 2D Fourier transform of f restricted to the line through the origin at angle θ: F₁\[Rf(·,θ)\](k) = F₂[f](k cos θ, k sin θ). This diagonalizes R (it becomes a slice/multiplication operator). Pseudo-inversion: the slice identity plus 2D Fourier inversion on Schwartz functions makes R injective on 𝓢, so a left inverse exists; the canonical one is filtered back-projection u ↦ backproject(Hilbert-filter(u)). Mathlib lacks the slice theorem and the filter. |
Author
There was a problem hiding this comment.
This was an interesting one, basically we need the escape \. Without it, markdown was interpreting it as a link [Rf(·,θ)](k) lol
Author
There was a problem hiding this comment.
Should we consider pinning links in this doc to a particular commit SHA, rather than linking to the master branch? The code could evolve over time and become stale, or the file could be deleted, etc.
If yes, I"m not sure which commit SHA to use (maybe just the latest one...?)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hello, this is my first time contributing here.
I used a tool lychee to identify all broken relative links for this PR. For the suggested link fixes, I used an LLM coding agent.
If there is interest, perhaps I could set up a github CI job to run that tool and catch broken links in future PRs! We could configure it to only run on PR's with markdown file edits or something like that.
Perhaps the CI job should be a separate follow-up PR.