Radon transform: Fourier-slice diagonalization and pseudo-inversion

radon_transform_inversion — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Radon's theorem (diagonalization + pseudo-inversion).** The Fourier slice
theorem diagonalizes the Radon transform, and the transform admits a left
inverse on the Schwartz space. -/
theorem radon_can_be_diagonalized_and_pseudo_inverted :
    (∀ φ : SchwartzMap (ℝ × ℝ) ℂ, ∀ θ k : ℝ,
        fourier1 (fun p => radon (φ : ℝ × ℝ → ℂ) (p, θ)) k =
          fourier2 (φ : ℝ × ℝ → ℂ) (k * Real.cos θ, k * Real.sin θ)) ∧
    (∃ Rinv : (ℝ × ℝ → ℂ) → (ℝ × ℝ → ℂ),
        ∀ φ : SchwartzMap (ℝ × ℝ) ℂ,
          Rinv (radon (φ : ℝ × ℝ → ℂ)) = (φ : ℝ × ℝ → ℂ)) := by
  sorry

Informal solution sketch

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(·,θ) = 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.

Source

J. Radon (1917); R. N. Bracewell (Fourier slice theorem, 1956). Knill, Some fundamental theorems in mathematics, §100.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: radon_can_be_diagonalized_and_pseudo_inverted
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.