Radon transform

DefinitionRadon transform on the plane#✓fully proved

For \(f : \mathbb{R}^2 \to \mathbb{C}\) and \(p, \theta \in \mathbb{R}\), the Radon transform of \(f\) at \((p, \theta)\) is the integral of \(f\) along the line \(x \cos\theta + y \sin\theta = p\) with respect to arc length,

\[Rf(p, \theta) = \int_{\mathbb{R}} f(p\cos\theta - t\sin\theta, p\sin\theta + t\cos\theta)\,dt,\]

where the integral is taken to be \(0\) when the integrand is not integrable.

noncomputable def radon (f : ℝ × ℝ → ℂ) (pθ : ℝ × ℝ) : ℂ :=
  ∫ t : ℝ, f (pθ.1 * Real.cos pθ.2 - t * Real.sin pθ.2,
              pθ.1 * Real.sin pθ.2 + t * Real.cos pθ.2)

Used by 1

Used byFourier slice theorem and injectivity of the Radon transform on Schwartz functions

DefinitionOne-dimensional Fourier transform#✓fully proved

For \(g : \mathbb{R} \to \mathbb{C}\) and \(k \in \mathbb{R}\), the Fourier transform of \(g\) at \(k\) is

\[\hat g(k) = \int_{\mathbb{R}} e^{-2\pi i p k} \, g(p) \, dp,\]

where the integral is taken to be \(0\) when the integrand is not integrable.

noncomputable def fourier1 (g : ℝ → ℂ) (k : ℝ) : ℂ :=
  ∫ p : ℝ, Complex.exp (-(2 * Real.pi * p * k) * Complex.I) * g p

Used by 1

Used byFourier slice theorem and injectivity of the Radon transform on Schwartz functions

DefinitionTwo-dimensional Fourier transform#✓fully proved

For \(f : \mathbb{R}^2 \to \mathbb{C}\) and \(k = (k_1, k_2) \in \mathbb{R}^2\), the Fourier transform of \(f\) at \(k\) is

\[\hat f(k) = \int_{\mathbb{R}^2} e^{-2\pi i (x_1 k_1 + x_2 k_2)} \, f(x) \, dx,\]

where \(dx\) is Lebesgue measure on \(\mathbb{R}^2\) and the integral is taken to be \(0\) when the integrand is not integrable.

noncomputable def fourier2 (f : ℝ × ℝ → ℂ) (k : ℝ × ℝ) : ℂ :=
  ∫ x : ℝ × ℝ,
    Complex.exp (-(2 * Real.pi * (x.1 * k.1 + x.2 * k.2)) * Complex.I) * f x

Used by 1

Used byFourier slice theorem and injectivity of the Radon transform on Schwartz functions

TheoremFourier slice theorem and injectivity of the Radon transform on Schwartz functions#●ready to prove

Write \(R\) for the Radon transform, \(\hat g\) for the one-dimensional Fourier transform of \(g : \mathbb{R} \to \mathbb{C}\) and \(\hat f\) for the two-dimensional Fourier transform of \(f : \mathbb{R}^2 \to \mathbb{C}\). For every Schwartz function \(\varphi : \mathbb{R}^2 \to \mathbb{C}\) and all \(\theta, k \in \mathbb{R}\), the Fourier transform of \(p \mapsto R\varphi(p, \theta)\) at \(k\) equals \(\hat\varphi(k\cos\theta, k\sin\theta)\). Moreover, there is a map \(S\) sending functions \(\mathbb{R}^2 \to \mathbb{C}\) to functions \(\mathbb{R}^2 \to \mathbb{C}\) such that \(S(R\varphi) = \varphi\) for every Schwartz function \(\varphi\).

The second part says only that \(R\) is injective on Schwartz functions; no formula, linearity or continuity is asserted for the left inverse \(S\).

public theorem_wanted 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 (φ : ℝ × ℝ → ℂ)) = (φ : ℝ × ℝ → ℂ))

Sources

• J. Radon (1917); R. N. Bracewell (Fourier slice theorem, 1956). Knill, Some fundamental theorems in mathematics, §100. Problem radon_transform_inversion of the lean-eval benchmark.

Uses 3

Statement usesOne-dimensional Fourier transform · Two-dimensional Fourier transform · Radon transform on the plane

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.