3.2. Fourier slice method: formalization details🔗

The machinery behind the results of the previous chapter, organized by Lean dependency rather than by publication order. Each section corresponds to one file of LeanRidgelet/FS/.

Status: every file exists, and all of Sections 2--7 is proved — Section 5 conditionally on an inversion formula out of Mathlib's reach, and Section 6 in full, including its inversion formula and all three of its reconstruction formulas in every codimension. What remains is stated rather than described: FS.Targets carries the two outstanding propositions with a sorry each — the existence of the fractional derivative, which is the one hypothesis Section 6's own form still carries, and the Jacobian of the singular value decomposition. No proof in this chapter depends on either. Three further results of the article are not stated at all, and FS.Targets says why: the inversion formula of Section 5 with its two examples needs the geometry constructed first, and Rubin's transform cannot be checked against its source.

FS.Defs: the scalar every case shares

Definition3.2.1

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 3.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Fourier slice pairing. (\!(\sigma,\rho)\!)_r=\frac{1}{2\pi}\int_{\omega\neq0}\sigma^\sharp(\omega)\overline{\rho^\sharp(\omega)}|\omega|^{-r}\,\mathrm d\omega, taking the two spectra rather than the two functions as arguments, since the activation is a tempered distribution in the manuscript and only its spectrum is ever used. The integral is over the complement of the origin, matching LeanRidgelet.admissibilityConstant of the L1 theory, which is the same scalar in the same convention.

Lean code for Definition3.2.1●1 definition

defdefined in LeanRidgelet/FS/Defs.lean

complete

def LeanRidgelet.fourierSlicePairing (r : ℝ) (Fσ Fρ : ℝ → ℂ) : ℂ

def LeanRidgelet.fourierSlicePairing (r : ℝ)
  (Fσ Fρ : ℝ → ℂ) : ℂ

Implementation after :=

:=
  (2 * (Real.pi : ℂ))⁻¹ *
    ∫ ω in {(0 : ℝ)}ᶜ, Fσ ω * conj (Fρ ω) / ((|ω| ^ r : ℝ) : ℂ)

The Fourier slice pairing `⦅σ, ρ⦆_r = (2π)⁻¹ ∫_{ω ≠ 0} σ♯(ω) conj (ρ♯(ω)) |ω|^{-r} dω`
of an activation spectrum `Fσ` against a ridgelet spectrum `Fρ`, at scale dimension `r`.

The arguments are the spectra rather than the functions themselves, because the activation is a
tempered distribution in the manuscript and only its spectrum is ever used.

Lemma3.2.2

uses 1used by 0✓L∃∀N

The pairing is sesquilinear. It vanishes when either spectrum does, it is homogeneous in the activation spectrum, and exchanging the two spectra conjugates it. These hold unconditionally, without any integrability hypothesis, because both sides degenerate to the same junk value when the integrand fails to be integrable.

Lean code for Lemma3.2.2●4 theorems

theoremdefined in LeanRidgelet/FS/Defs.lean

complete

theorem LeanRidgelet.fs_fourierSlicePairing_zero_left (r : ℝ) (Fρ : ℝ → ℂ) :
  LeanRidgelet.fourierSlicePairing r (fun x ↦ 0) Fρ = 0

theorem LeanRidgelet.fs_fourierSlicePairing_zero_left
  (r : ℝ) (Fρ : ℝ → ℂ) :
  LeanRidgelet.fourierSlicePairing r
      (fun x ↦ 0) Fρ =
    0

The pairing vanishes on a zero activation spectrum.

theoremdefined in LeanRidgelet/FS/Defs.lean

complete

theorem LeanRidgelet.fs_fourierSlicePairing_zero_right (r : ℝ) (Fσ : ℝ → ℂ) :
  (LeanRidgelet.fourierSlicePairing r Fσ fun x ↦ 0) = 0

theorem LeanRidgelet.fs_fourierSlicePairing_zero_right
  (r : ℝ) (Fσ : ℝ → ℂ) :
  (LeanRidgelet.fourierSlicePairing r Fσ
      fun x ↦ 0) =
    0

The pairing vanishes on a zero ridgelet spectrum.

theoremdefined in LeanRidgelet/FS/Defs.lean

complete

theorem LeanRidgelet.fs_fourierSlicePairing_const_mul_left (r : ℝ) (c : ℂ)
  (Fσ Fρ : ℝ → ℂ) :
  LeanRidgelet.fourierSlicePairing r (fun ω ↦ c * Fσ ω) Fρ =
    c * LeanRidgelet.fourierSlicePairing r Fσ Fρ

theorem LeanRidgelet.fs_fourierSlicePairing_const_mul_left
  (r : ℝ) (c : ℂ) (Fσ Fρ : ℝ → ℂ) :
  LeanRidgelet.fourierSlicePairing r
      (fun ω ↦ c * Fσ ω) Fρ =
    c *
      LeanRidgelet.fourierSlicePairing r
        Fσ Fρ

The pairing is homogeneous in the activation spectrum.

theoremdefined in LeanRidgelet/FS/Defs.lean

complete

theorem LeanRidgelet.fs_fourierSlicePairing_conj (r : ℝ) (Fσ Fρ : ℝ → ℂ) :
  (starRingEnd ℂ) (LeanRidgelet.fourierSlicePairing r Fσ Fρ) =
    LeanRidgelet.fourierSlicePairing r Fρ Fσ

theorem LeanRidgelet.fs_fourierSlicePairing_conj
  (r : ℝ) (Fσ Fρ : ℝ → ℂ) :
  (starRingEnd ℂ)
      (LeanRidgelet.fourierSlicePairing r
        Fσ Fρ) =
    LeanRidgelet.fourierSlicePairing r Fρ
      Fσ

Swapping the two spectra conjugates the pairing: the manuscript's scalar product of the
activation against the ridgelet function is a genuine sesquilinear pairing.

FS.Scheme: the three steps as one conditional theorem

Theorem3.2.3

Statement uses 2

Statement dependency previews

Preview

Definition 3.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 3.2.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The abstract reconstruction theorem. The scale space is a finite-dimensional real inner product space V with an additive Haar measure, whose dimension is the exponent r; the direction space U carries a measure; the input domain X needs no structure at all, since only the composite distance and the weight see it. Step 2 is the scaling behaviour of the Haar measure and holds for every integrand and every ω, both sides degenerating together. Steps 2 and 3 meet in the weight integral at a fixed bias frequency, which the ansatz turns into the inversion integral rescaled by the Jacobian. The reconstruction theorem composes them, with the inversion formula on the input domain as its only hypothesis.

Lean code for Theorem3.2.3●9 declarations

defdefined in LeanRidgelet/FS/Scheme.lean

complete

def LeanRidgelet.fourierSlicePhase (t : ℝ) : ℂ

def LeanRidgelet.fourierSlicePhase (t : ℝ) : ℂ

Implementation after :=

:= Complex.exp (Complex.I * (t : ℂ))

The plane wave `e^{i t}`, the inverse-transform phase of the article's convention.

defdefined in LeanRidgelet/FS/Scheme.lean

complete

def LeanRidgelet.fourierExpressionSynthesis.{u_1, u_2, u_3} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  {U : Type u_2} [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V) (ν : MeasureTheory.Measure U)
  (Fσ : ℝ → ℂ) (Γ : V → U → ℝ → ℂ) (π : X → U → V) (w : X → U → ℂ)
  (x : X) : ℂ

def LeanRidgelet.fourierExpressionSynthesis.{u_1,
    u_2, u_3}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [MeasurableSpace V] {U : Type u_2}
  [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V)
  (ν : MeasureTheory.Measure U)
  (Fσ : ℝ → ℂ) (Γ : V → U → ℝ → ℂ)
  (π : X → U → V) (w : X → U → ℂ)
  (x : X) : ℂ

Implementation after :=

:=
  (2 * (Real.pi : ℂ))⁻¹ *
    ∫ ω : ℝ, ∫ a : V, ∫ u : U,
      Γ a u ω * Fσ ω * fourierSlicePhase (ω * inner ℝ a (π x u)) * w x u ∂ν ∂μ

The network in Fourier expression form, the output of Step 1:
`S[γ](x) = (2π)⁻¹ ∫∫∫ γ♯(a,u,ω) σ♯(ω) e^{iω⟪a, π(x,u)⟫} w(x,u) dν du dω`,
with the bias frequency outermost.

defdefined in LeanRidgelet/FS/Scheme.lean

complete

def LeanRidgelet.separationOfVariables.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] {U : Type u_2}
  (F : V → U → ℂ) (κ : V → ℝ) (Fρ : ℝ → ℂ) : V → U → ℝ → ℂ

def LeanRidgelet.separationOfVariables.{u_1,
    u_2}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] {U : Type u_2}
  (F : V → U → ℂ) (κ : V → ℝ)
  (Fρ : ℝ → ℂ) : V → U → ℝ → ℂ

Implementation after :=

:=
  fun a u ω => F (ω • a) u * ((κ (ω • a) : ℝ) : ℂ) * conj (Fρ ω)

The separation-of-variables ansatz of Step 3: a principal factor carrying the Fourier data of
the target function and the density of its inversion formula, and an auxiliary factor carrying the
ridgelet spectrum, coupled through `ξ = ω a`.

defdefined in LeanRidgelet/FS/Scheme.lean

complete

def LeanRidgelet.inversionIntegral.{u_1, u_2, u_3} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  {U : Type u_2} [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V) (ν : MeasureTheory.Measure U)
  (F : V → U → ℂ) (κ : V → ℝ) (π : X → U → V) (w : X → U → ℂ) (x : X) :
  ℂ

def LeanRidgelet.inversionIntegral.{u_1, u_2,
    u_3}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [MeasurableSpace V] {U : Type u_2}
  [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V)
  (ν : MeasureTheory.Measure U)
  (F : V → U → ℂ) (κ : V → ℝ)
  (π : X → U → V) (w : X → U → ℂ)
  (x : X) : ℂ

Implementation after :=

:=
  ∫ lam : V, ∫ u : U,
    F lam u * ((κ lam : ℝ) : ℂ) * fourierSlicePhase (inner ℝ lam (π x u)) * w x u ∂ν ∂μ

The integral evaluated by the inversion formula on the input domain:
`∫∫ F(λ,u) κ(λ) e^{i⟪λ, π(x,u)⟫} w(x,u) dν dλ`. On a Euclidean space with `U` a point this is the
Fourier inversion integral; on a symmetric space it is the Helgason--Fourier inversion integral,
with `κ = |W|⁻¹|c(λ)|⁻²`.

theoremdefined in LeanRidgelet/FS/Scheme.lean

complete

theorem LeanRidgelet.fs_changeOfVariables.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.Measure V)
  [μ.IsAddHaarMeasure] (G : V → ℂ) (ω : ℝ) :
  ∫ (a : V), G (ω • a) ∂μ =
    (|ω| ^ ↑(Module.finrank ℝ V))⁻¹ • ∫ (lam : V), G lam ∂μ

theorem LeanRidgelet.fs_changeOfVariables.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  (μ : MeasureTheory.Measure V)
  [μ.IsAddHaarMeasure] (G : V → ℂ)
  (ω : ℝ) :
  ∫ (a : V), G (ω • a) ∂μ =
    (|ω| ^ ↑(Module.finrank ℝ V))⁻¹ •
      ∫ (lam : V), G lam ∂μ

**Step 2**: the change of variables `ξ = ω a` on the scale space, with Jacobian `|ω|^{-r}`
where `r` is the dimension. It holds for every integrand and every `ω`, including `ω = 0`, since
both sides degenerate together.

theoremdefined in LeanRidgelet/FS/Scheme.lean

complete

theorem LeanRidgelet.fs_slice_of_inversion.{u_1, u_2, u_3} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {U : Type u_2} [MeasurableSpace U]
  {X : Type u_3} (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure U) (Fσ Fρ : ℝ → ℂ) (F : V → U → ℂ)
  (κ : V → ℝ) (π : X → U → V) (w : X → U → ℂ) (f : X → ℂ)
  (hinv : ∀ (y : X), LeanRidgelet.inversionIntegral μ ν F κ π w y = f y)
  (x : X) (ω : ℝ) :
  ∫ (a : V),
      ∫ (u : U),
        LeanRidgelet.separationOfVariables F κ Fρ a u ω * Fσ ω *
            LeanRidgelet.fourierSlicePhase (ω * inner ℝ a (π x u)) *
          w x u ∂ν ∂μ =
    Fσ ω * (starRingEnd ℂ) (Fρ ω) * ↑(|ω| ^ ↑(Module.finrank ℝ V))⁻¹ *
      f x

theorem LeanRidgelet.fs_slice_of_inversion.{u_1,
    u_2, u_3}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {U : Type u_2} [MeasurableSpace U]
  {X : Type u_3}
  (μ : MeasureTheory.Measure V)
  [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure U)
  (Fσ Fρ : ℝ → ℂ) (F : V → U → ℂ)
  (κ : V → ℝ) (π : X → U → V)
  (w : X → U → ℂ) (f : X → ℂ)
  (hinv :
    ∀ (y : X),
      LeanRidgelet.inversionIntegral μ ν F
          κ π w y =
        f y)
  (x : X) (ω : ℝ) :
  ∫ (a : V),
      ∫ (u : U),
        LeanRidgelet.separationOfVariables
                F κ Fρ a u ω *
              Fσ ω *
            LeanRidgelet.fourierSlicePhase
              (ω * inner ℝ a (π x u)) *
          w x u ∂ν ∂μ =
    Fσ ω * (starRingEnd ℂ) (Fρ ω) *
        ↑(|ω| ^ ↑(Module.finrank ℝ V))⁻¹ *
      f x

Where Steps 2 and 3 meet. Substituting the ansatz, the weight integral at a fixed bias
frequency is the inversion integral rescaled by the Jacobian, hence `|ω|^{-r} f(x)`. The bias
frequency leaves the two inner integrals as a constant, which is why no integrability hypothesis
is needed.

defdefined in LeanRidgelet/FS/Scheme.lean

complete

def LeanRidgelet.sliceSynthesis.{u_1, u_2, u_3} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  {U : Type u_2} [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V) (ν : MeasureTheory.Measure U)
  (σ : ℝ → ℂ) (γ : V → U → ℝ → ℂ) (π : X → U → V) (w : X → U → ℂ)
  (x : X) : ℂ

def LeanRidgelet.sliceSynthesis.{u_1, u_2,
    u_3}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [MeasurableSpace V] {U : Type u_2}
  [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V)
  (ν : MeasureTheory.Measure U)
  (σ : ℝ → ℂ) (γ : V → U → ℝ → ℂ)
  (π : X → U → V) (w : X → U → ℂ)
  (x : X) : ℂ

Implementation after :=

:=
  ∫ a : V, (∫ u : U, (∫ b : ℝ, γ a u b * σ (inner ℝ a (π x u) - b) * w x u) ∂ν) ∂μ

The network as the article writes it, an integral of `γ(a,u,b) σ(⟪a, π(x,u)⟫ - b) w(x,u)`
over weights, directions and biases.

theoremdefined in LeanRidgelet/FS/Scheme.lean

complete

theorem LeanRidgelet.fs_fourierExpression_of_bias.{u_1, u_2, u_3} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  {U : Type u_2} [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V) (ν : MeasureTheory.Measure U)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (σ Fσ : ℝ → ℂ)
  (γ Γ : V → U → ℝ → ℂ) (π : X → U → V) (w : X → U → ℂ) (x : X)
  (hbias :
    ∀ (a : V) (u : U),
      ∫ (b : ℝ), γ a u b * σ (inner ℝ a (π x u) - b) * w x u =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            Γ a u ω * Fσ ω *
                LeanRidgelet.fourierSlicePhase (ω * inner ℝ a (π x u)) *
              w x u)
  (hint :
    MeasureTheory.Integrable
      (fun p ↦
        Γ p.2.1 p.2.2 p.1 * Fσ p.1 *
            LeanRidgelet.fourierSlicePhase
              (p.1 * inner ℝ p.2.1 (π x p.2.2)) *
          w x p.2.2)
      (MeasureTheory.volume.prod (μ.prod ν))) :
  LeanRidgelet.sliceSynthesis μ ν σ γ π w x =
    LeanRidgelet.fourierExpressionSynthesis μ ν Fσ Γ π w x

theorem LeanRidgelet.fs_fourierExpression_of_bias.{u_1,
    u_2, u_3}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [MeasurableSpace V] {U : Type u_2}
  [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V)
  (ν : MeasureTheory.Measure U)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] (σ Fσ : ℝ → ℂ)
  (γ Γ : V → U → ℝ → ℂ) (π : X → U → V)
  (w : X → U → ℂ) (x : X)
  (hbias :
    ∀ (a : V) (u : U),
      ∫ (b : ℝ),
          γ a u b *
              σ (inner ℝ a (π x u) - b) *
            w x u =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            Γ a u ω * Fσ ω *
                LeanRidgelet.fourierSlicePhase
                  (ω *
                    inner ℝ a (π x u)) *
              w x u)
  (hint :
    MeasureTheory.Integrable
      (fun p ↦
        Γ p.2.1 p.2.2 p.1 * Fσ p.1 *
            LeanRidgelet.fourierSlicePhase
              (p.1 *
                inner ℝ p.2.1
                  (π x p.2.2)) *
          w x p.2.2)
      (MeasureTheory.volume.prod
        (μ.prod ν))) :
  LeanRidgelet.sliceSynthesis μ ν σ γ π w
      x =
    LeanRidgelet.fourierExpressionSynthesis
      μ ν Fσ Γ π w x

**Step 1**: the network equals its Fourier expression.

The analytic input is one-dimensional and is the hypothesis `hbias`: at a fixed weight and
direction, convolving in the bias and inverting turns the bias integral into an integral against
the bias frequency. Everything else is Fubini, moving that frequency outside the weight and
direction integrals, which is the hypothesis `hint` — the article's standing assumption that the
triple integral converges absolutely so that the order of integration may be changed freely.

theoremdefined in LeanRidgelet/FS/Scheme.lean

complete

theorem LeanRidgelet.fs_reconstruction_of_inversion.{u_1, u_2, u_3}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  {U : Type u_2} [MeasurableSpace U] {X : Type u_3}
  (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure U) (Fσ Fρ : ℝ → ℂ) (F : V → U → ℂ)
  (κ : V → ℝ) (π : X → U → V) (w : X → U → ℂ) (f : X → ℂ)
  (hinv : ∀ (y : X), LeanRidgelet.inversionIntegral μ ν F κ π w y = f y)
  (x : X) :
  LeanRidgelet.fourierExpressionSynthesis μ ν Fσ
      (LeanRidgelet.separationOfVariables F κ Fρ) π w x =
    LeanRidgelet.fourierSlicePairing (↑(Module.finrank ℝ V)) Fσ Fρ * f x

theorem LeanRidgelet.fs_reconstruction_of_inversion.{u_1,
    u_2, u_3}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {U : Type u_2} [MeasurableSpace U]
  {X : Type u_3}
  (μ : MeasureTheory.Measure V)
  [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure U)
  (Fσ Fρ : ℝ → ℂ) (F : V → U → ℂ)
  (κ : V → ℝ) (π : X → U → V)
  (w : X → U → ℂ) (f : X → ℂ)
  (hinv :
    ∀ (y : X),
      LeanRidgelet.inversionIntegral μ ν F
          κ π w y =
        f y)
  (x : X) :
  LeanRidgelet.fourierExpressionSynthesis
      μ ν Fσ
      (LeanRidgelet.separationOfVariables
        F κ Fρ)
      π w x =
    LeanRidgelet.fourierSlicePairing
        (↑(Module.finrank ℝ V)) Fσ Fρ *
      f x

**The reconstruction formula of the Fourier slice method.** Given an inversion formula on the
input domain, the network built from the separation-of-variables ansatz reproduces the target
function up to the Fourier slice pairing of the activation spectrum against the ridgelet spectrum.

The inversion formula is the only hypothesis. Each of the article's cases is an instance: the
input domain and its inversion formula change, the three steps do not.

No integrability hypothesis appears in the reconstruction theorem, and none is needed: substituting the ansatz makes the bias frequency factor out of both inner integrals as a constant, so that proof never exchanges an order of integration. Fubini enters in Step 1 instead, and there it is unavoidable: fs_fourierExpression_of_bias takes the one-dimensional bias identity and the integrability of the triple integrand, and the rearrangement itself is the upstream-candidate integral_integral_integral_swap_left. Over a finite field both hypotheses are finite-sum statements and fs_finite_field_detail discharges them.

FS.Euclidean: the classical case, and agreement with the L1 development

Theorem3.2.4

Statement uses 2

Statement dependency previews

Preview

Theorem 3.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 3.2.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Euclidean instance, and the check against the L1 development. Taking the direction space to be a point collapses its integral, leaving the plain inversion integral on \mathbb R^m; the scale space is \mathbb R^m itself, so r=m. Two identities then check the abstraction against the L1 formalization, which predates it and was built independently: the ansatz at homogeneity index s=0 is the L1 Fourier expression eq:fstridge, and the L1 admissibility constant is (2\pi)^m times the Fourier slice pairing of the same two spectra.

Lean code for Theorem3.2.4●13 theorems

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_inversionIntegral_euclidean (m : ℕ)
  (Ff : LeanRidgelet.InputSpace m → ℂ)
  (κ : LeanRidgelet.InputSpace m → ℝ) (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.inversionIntegral MeasureTheory.volume
      (MeasureTheory.Measure.dirac ()) (fun ξ x ↦ Ff ξ) κ (fun y x ↦ y)
      (fun x x_1 ↦ 1) x =
    ∫ (ξ : LeanRidgelet.InputSpace m),
      Ff ξ * ↑(κ ξ) * LeanRidgelet.fourierSlicePhase (inner ℝ ξ x)

theorem LeanRidgelet.fs_inversionIntegral_euclidean
  (m : ℕ)
  (Ff : LeanRidgelet.InputSpace m → ℂ)
  (κ : LeanRidgelet.InputSpace m → ℝ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.inversionIntegral
      MeasureTheory.volume
      (MeasureTheory.Measure.dirac ())
      (fun ξ x ↦ Ff ξ) κ (fun y x ↦ y)
      (fun x x_1 ↦ 1) x =
    ∫ (ξ : LeanRidgelet.InputSpace m),
      Ff ξ * ↑(κ ξ) *
        LeanRidgelet.fourierSlicePhase
          (inner ℝ ξ x)

With a one-point direction space, the identity as composite distance and unit weight, the
inversion integral of the abstract scheme is the plain inversion integral on `ℝ^m`.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_finrank_inputSpace (m : ℕ) :
  Module.finrank ℝ (LeanRidgelet.InputSpace m) = m

theorem LeanRidgelet.fs_finrank_inputSpace
  (m : ℕ) :
  Module.finrank ℝ
      (LeanRidgelet.InputSpace m) =
    m

The scale space of the Euclidean instance has dimension `m`, so the Jacobian exponent of
Step 2 is `m`.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_reconstruction_euclidean (m : ℕ) (Fσ Fρ : ℝ → ℂ)
  (Ff : LeanRidgelet.InputSpace m → ℂ)
  (κ : LeanRidgelet.InputSpace m → ℝ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (hinv :
    ∀ (x : LeanRidgelet.InputSpace m),
      ∫ (ξ : LeanRidgelet.InputSpace m),
          Ff ξ * ↑(κ ξ) * LeanRidgelet.fourierSlicePhase (inner ℝ ξ x) =
        f x)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.fourierExpressionSynthesis MeasureTheory.volume
      (MeasureTheory.Measure.dirac ()) Fσ
      (LeanRidgelet.separationOfVariables (fun ξ x ↦ Ff ξ) κ Fρ)
      (fun y x ↦ y) (fun x x_1 ↦ 1) x =
    LeanRidgelet.fourierSlicePairing (↑m) Fσ Fρ * f x

theorem LeanRidgelet.fs_reconstruction_euclidean
  (m : ℕ) (Fσ Fρ : ℝ → ℂ)
  (Ff : LeanRidgelet.InputSpace m → ℂ)
  (κ : LeanRidgelet.InputSpace m → ℝ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (hinv :
    ∀ (x : LeanRidgelet.InputSpace m),
      ∫ (ξ : LeanRidgelet.InputSpace m),
          Ff ξ * ↑(κ ξ) *
            LeanRidgelet.fourierSlicePhase
              (inner ℝ ξ x) =
        f x)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.fourierExpressionSynthesis
      MeasureTheory.volume
      (MeasureTheory.Measure.dirac ()) Fσ
      (LeanRidgelet.separationOfVariables
        (fun ξ x ↦ Ff ξ) κ Fρ)
      (fun y x ↦ y) (fun x x_1 ↦ 1) x =
    LeanRidgelet.fourierSlicePairing (↑m)
        Fσ Fρ *
      f x

**The reconstruction formula for the fully-connected network on `ℝ^m`**, as the instance of
the abstract scheme with a one-point direction space. The only hypothesis is the Fourier inversion
formula on `ℝ^m` in the article's convention, carried by the inversion density `κ`.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform (m : ℕ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (fun b ↦ LeanRidgelet.euclideanRidgeletTransform m 0 ψ f (a, b))
      ζ =
    LeanRidgelet.separationOfVariables
      (fun ξ x ↦ LeanRidgelet.Fourier.angularFourierIntegralInner f ξ)
      (fun x ↦ 1) (LeanRidgelet.angularFourier1D ψ) a () ζ

theorem LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform
  (m : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m)
  (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (fun b ↦
        LeanRidgelet.euclideanRidgeletTransform
          m 0 ψ f (a, b))
      ζ =
    LeanRidgelet.separationOfVariables
      (fun ξ x ↦
        LeanRidgelet.Fourier.angularFourierIntegralInner
          f ξ)
      (fun x ↦ 1)
      (LeanRidgelet.angularFourier1D ψ) a
      () ζ

**The ansatz is the L1 Fourier expression.** The bias spectrum of the classical ridgelet
transform at homogeneity index `s = 0`, computed in `L1.FourierExpression` as `eq:fstridge`, is
exactly the separation-of-variables form the abstract scheme prescribes: the Fourier data of the
target evaluated at `ζ a`, against the conjugate ridgelet spectrum.

Nothing about the abstract scheme was used to prove the L1 identity, which predates it; this is
the check that the two agree.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing (m : ℕ)
  (hm : 1 ≤ m) (ψ Fη : ℝ → ℂ) :
  LeanRidgelet.admissibilityConstant m ψ Fη =
    (2 * ↑Real.pi) ^ m *
      LeanRidgelet.fourierSlicePairing (↑m) Fη
        (LeanRidgelet.angularFourier1D ψ)

theorem LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
  (m : ℕ) (hm : 1 ≤ m) (ψ Fη : ℝ → ℂ) :
  LeanRidgelet.admissibilityConstant m ψ
      Fη =
    (2 * ↑Real.pi) ^ m *
      LeanRidgelet.fourierSlicePairing
        (↑m) Fη
        (LeanRidgelet.angularFourier1D ψ)

**The two scalars agree.** The L1 admissibility constant `K_{ψ,η}` is `(2π)^m` times the
Fourier slice pairing of the activation spectrum against the ridgelet spectrum.

The factor is where the normalization of the Fourier inversion formula sits: the article's
coefficient function does not carry the inversion density `κ = (2π)^{-m}`, so its constant part
ends up in the article's `⦅σ,ρ⦆`, whereas the ansatz of the abstract scheme carries it. The
hypothesis `1 ≤ m` is only needed because `admissibilityConstant` writes the exponent as the
truncated subtraction `m - 1`.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_inversionIntegral_polar (m : ℕ)
  [Nontrivial (LeanRidgelet.InputSpace m)]
  (Ff : LeanRidgelet.InputSpace m → ℂ) (kappa : ℝ)
  (x : LeanRidgelet.InputSpace m)
  (hF :
    MeasureTheory.Integrable
      (fun ξ ↦
        Ff ξ * ↑kappa * LeanRidgelet.fourierSlicePhase (inner ℝ ξ x))
      MeasureTheory.volume)
  (hprod :
    MeasureTheory.Integrable
      (fun p ↦
        |p.1| ^ (Module.finrank ℝ (LeanRidgelet.InputSpace m) - 1) •
          (Ff (p.1 • ↑p.2) * ↑kappa *
            LeanRidgelet.fourierSlicePhase (inner ℝ (p.1 • ↑p.2) x)))
      (MeasureTheory.volume.prod MeasureTheory.volume.toSphere)) :
  LeanRidgelet.inversionIntegral MeasureTheory.volume
      MeasureTheory.volume.toSphere (fun lam u ↦ Ff (lam • ↑u))
      (fun lam ↦
        2⁻¹ * kappa *
          |lam| ^ (Module.finrank ℝ (LeanRidgelet.InputSpace m) - 1))
      (fun y u ↦ inner ℝ (↑u) y) (fun x x_1 ↦ 1) x =
    ∫ (ξ : LeanRidgelet.InputSpace m),
      Ff ξ * ↑kappa * LeanRidgelet.fourierSlicePhase (inner ℝ ξ x)

theorem LeanRidgelet.fs_inversionIntegral_polar
  (m : ℕ)
  [Nontrivial (LeanRidgelet.InputSpace m)]
  (Ff : LeanRidgelet.InputSpace m → ℂ)
  (kappa : ℝ)
  (x : LeanRidgelet.InputSpace m)
  (hF :
    MeasureTheory.Integrable
      (fun ξ ↦
        Ff ξ * ↑kappa *
          LeanRidgelet.fourierSlicePhase
            (inner ℝ ξ x))
      MeasureTheory.volume)
  (hprod :
    MeasureTheory.Integrable
      (fun p ↦
        |p.1| ^
            (Module.finrank ℝ
                (LeanRidgelet.InputSpace
                  m) -
              1) •
          (Ff (p.1 • ↑p.2) * ↑kappa *
            LeanRidgelet.fourierSlicePhase
              (inner ℝ (p.1 • ↑p.2) x)))
      (MeasureTheory.volume.prod
        MeasureTheory.volume.toSphere)) :
  LeanRidgelet.inversionIntegral
      MeasureTheory.volume
      MeasureTheory.volume.toSphere
      (fun lam u ↦ Ff (lam • ↑u))
      (fun lam ↦
        2⁻¹ * kappa *
          |lam| ^
            (Module.finrank ℝ
                (LeanRidgelet.InputSpace
                  m) -
              1))
      (fun y u ↦ inner ℝ (↑u) y)
      (fun x x_1 ↦ 1) x =
    ∫ (ξ : LeanRidgelet.InputSpace m),
      Ff ξ * ↑kappa *
        LeanRidgelet.fourierSlicePhase
          (inner ℝ ξ x)

**The same Euclidean network, parametrized in polar coordinates.** Writing the weight as
`a = λ u` with `u` on the unit sphere turns the instance above, whose scale space is `ℝ^m` and
whose direction space is a point, into one whose scale space is `ℝ` and whose direction space is
the sphere. The inversion integral is the same, so both are instances of the scheme for the same
domain and the same target.

The Jacobian exponent is therefore `m` in one and `1` in the other: **the rank of the scheme is a
property of the parametrization of the weight, not of the input domain.** The `r = 1` shape is the
one the symmetric-space case takes, with the sphere in the role of the boundary `∂X`.

The inversion density carries the factor `2⁻¹` of the two-sided polar formula, which is the double
cover `(λ, u) ↦ λ u` of `ℝ^m ∖ {0}`. Both hypotheses are the absolute convergence the article
assumes in Section 2.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_integrable_angularFourier_iff.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] (f : V → ℂ) :
  MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume ↔
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume

theorem LeanRidgelet.fs_integrable_angularFourier_iff.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  (f : V → ℂ) :
  MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume ↔
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume

The two conventions have the same integrable Fourier transforms: they differ by the rescaling
`ξ ↦ (2π)⁻¹ ξ`, which preserves integrability.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_angularFourier_inversion_inner.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {f : V → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume)
  {x : V} (hx : ContinuousAt f x) :
  ∫ (ξ : V),
      LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
        LeanRidgelet.fourierSlicePhase (inner ℝ ξ x) =
    ↑((2 * Real.pi) ^ Module.finrank ℝ V) * f x

theorem LeanRidgelet.fs_angularFourier_inversion_inner.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {f : V → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume)
  {x : V} (hx : ContinuousAt f x) :
  ∫ (ξ : V),
      LeanRidgelet.Fourier.angularFourierIntegralInner
          f ξ *
        LeanRidgelet.fourierSlicePhase
          (inner ℝ ξ x) =
    ↑((2 * Real.pi) ^
          Module.finrank ℝ V) *
      f x

**Fourier inversion in the article's angular convention** on a finite-dimensional real inner
product space: the inversion integral of the angular Fourier transform returns `(2π)^r` times the
function, `r` the dimension of the space.

This is Mathlib's `MeasureTheory.Integrable.fourierInv_fourier_eq` after the change of variables
`ξ ↦ (2π) ξ` that passes between the two conventions; the constant is the Jacobian `(2π)^r` of that
rescaling. Together with the inversion density `κ = (2π)^{-r}` it discharges the hypothesis of
`LeanRidgelet.fs_reconstruction_euclidean`.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_integrable_angularFourier_mul_phase.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {f : V → ℂ}
  (hFf :
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume)
  (x : V) :
  MeasureTheory.Integrable
    (fun ξ ↦
      LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
        LeanRidgelet.fourierSlicePhase (inner ℝ ξ x))
    MeasureTheory.volume

theorem LeanRidgelet.fs_integrable_angularFourier_mul_phase.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {f : V → ℂ}
  (hFf :
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume)
  (x : V) :
  MeasureTheory.Integrable
    (fun ξ ↦
      LeanRidgelet.Fourier.angularFourierIntegralInner
          f ξ *
        LeanRidgelet.fourierSlicePhase
          (inner ℝ ξ x))
    MeasureTheory.volume

The inversion integrand is integrable as soon as the Fourier transform is: the plane wave is
unimodular.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_angularFourier_inversion_inputSpace {m : ℕ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume)
  {x : LeanRidgelet.InputSpace m} (hx : ContinuousAt f x) :
  ∫ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
        LeanRidgelet.fourierSlicePhase (inner ℝ ξ x) =
    ↑((2 * Real.pi) ^ m) * f x

theorem LeanRidgelet.fs_angularFourier_inversion_inputSpace
  {m : ℕ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume)
  {x : LeanRidgelet.InputSpace m}
  (hx : ContinuousAt f x) :
  ∫ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner
          f ξ *
        LeanRidgelet.fourierSlicePhase
          (inner ℝ ξ x) =
    ↑((2 * Real.pi) ^ m) * f x

Fourier inversion in the article's angular convention on `ℝ^m`, with the dimension read off the
index type.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_angularFourier_inversion_ae {h : ℝ → ℂ}
  (hh : MeasureTheory.Integrable h MeasureTheory.volume)
  (hFh :
    MeasureTheory.Integrable (FourierTransform.fourier h)
      MeasureTheory.volume) :
  ∀ᵐ (t : ℝ),
    h t =
      (2 * ↑Real.pi)⁻¹ *
        ∫ (ω : ℝ),
          LeanRidgelet.angularFourier1D h ω *
            LeanRidgelet.fourierSlicePhase (ω * t)

theorem LeanRidgelet.fs_angularFourier_inversion_ae
  {h : ℝ → ℂ}
  (hh :
    MeasureTheory.Integrable h
      MeasureTheory.volume)
  (hFh :
    MeasureTheory.Integrable
      (FourierTransform.fourier h)
      MeasureTheory.volume) :
  ∀ᵐ (t : ℝ),
    h t =
      (2 * ↑Real.pi)⁻¹ *
        ∫ (ω : ℝ),
          LeanRidgelet.angularFourier1D h
              ω *
            LeanRidgelet.fourierSlicePhase
              (ω * t)

Fourier inversion in the article's angular convention, almost everywhere.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_angularFourier1D_convolution {γ σ : ℝ → ℂ}
  (hγ : MeasureTheory.Integrable γ MeasureTheory.volume)
  (hσ : MeasureTheory.Integrable σ MeasureTheory.volume) (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (MeasureTheory.convolution γ σ (ContinuousLinearMap.mul ℂ ℂ)
        MeasureTheory.volume)
      ζ =
    LeanRidgelet.angularFourier1D γ ζ *
      LeanRidgelet.angularFourier1D σ ζ

theorem LeanRidgelet.fs_angularFourier1D_convolution
  {γ σ : ℝ → ℂ}
  (hγ :
    MeasureTheory.Integrable γ
      MeasureTheory.volume)
  (hσ :
    MeasureTheory.Integrable σ
      MeasureTheory.volume)
  (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (MeasureTheory.convolution γ σ
        (ContinuousLinearMap.mul ℂ ℂ)
        MeasureTheory.volume)
      ζ =
    LeanRidgelet.angularFourier1D γ ζ *
      LeanRidgelet.angularFourier1D σ ζ

The convolution theorem in the article's angular convention: rescaling the frequency does not
disturb it.

theoremdefined in LeanRidgelet/FS/Euclidean.lean

complete

theorem LeanRidgelet.fs_bias_fourierExpression_ae {γ σ : ℝ → ℂ}
  (hγ : MeasureTheory.Integrable γ MeasureTheory.volume)
  (hσ : MeasureTheory.Integrable σ MeasureTheory.volume)
  (hprod :
    MeasureTheory.Integrable
      (FourierTransform.fourier
        (MeasureTheory.convolution γ σ (ContinuousLinearMap.mul ℂ ℂ)
          MeasureTheory.volume))
      MeasureTheory.volume) :
  ∀ᵐ (t : ℝ),
    ∫ (b : ℝ), γ b * σ (t - b) =
      (2 * ↑Real.pi)⁻¹ *
        ∫ (ω : ℝ),
          LeanRidgelet.angularFourier1D γ ω *
              LeanRidgelet.angularFourier1D σ ω *
            LeanRidgelet.fourierSlicePhase (ω * t)

theorem LeanRidgelet.fs_bias_fourierExpression_ae
  {γ σ : ℝ → ℂ}
  (hγ :
    MeasureTheory.Integrable γ
      MeasureTheory.volume)
  (hσ :
    MeasureTheory.Integrable σ
      MeasureTheory.volume)
  (hprod :
    MeasureTheory.Integrable
      (FourierTransform.fourier
        (MeasureTheory.convolution γ σ
          (ContinuousLinearMap.mul ℂ ℂ)
          MeasureTheory.volume))
      MeasureTheory.volume) :
  ∀ᵐ (t : ℝ),
    ∫ (b : ℝ), γ b * σ (t - b) =
      (2 * ↑Real.pi)⁻¹ *
        ∫ (ω : ℝ),
          LeanRidgelet.angularFourier1D γ
                ω *
              LeanRidgelet.angularFourier1D
                σ ω *
            LeanRidgelet.fourierSlicePhase
              (ω * t)

**Step 1 over `ℝ`, the one-dimensional bias identity.** For an integrable coefficient function
and an integrable activation, the bias integral of the network at a fixed weight and direction is
the inverse transform of the product of the two spectra. This is the hypothesis `hbias` of
`LeanRidgelet.fs_fourierExpression_of_bias`, discharged for integrable activations; the finite
field case discharges the corresponding statement there.

The conclusion holds almost everywhere, which is what Fourier inversion gives without a continuity
hypothesis. The factor `(2π)⁻¹` is the Jacobian of the passage from the Mathlib convention to the
article's angular one.

The polar instance is there too: writing the weight as \boldsymbol a=\lambda\boldsymbol u turns the instance with scale space \mathbb R^m and a point for directions into one with scale space \mathbb R and the sphere for directions, and fs_inversionIntegral_polar shows the inversion integral is the same. So both are instances of the scheme for the same domain and the same target, with Jacobian exponents m and 1: the rank is a property of the parametrization of the weight, not of the input domain. The r=1 shape is the one the symmetric-space case takes, with the sphere in the role of the boundary. The density carries the factor 2^{-1} of the two-sided polar formula, which is the double cover (\lambda,\boldsymbol u)\mapsto\lambda\boldsymbol u.

The one-dimensional input of Step 1 is discharged here too, for an integrable activation: fs_bias_fourierExpression_ae is the convolution theorem in the angular convention followed by Fourier inversion, and it holds almost everywhere, which is what inversion gives without a continuity hypothesis. Both are transported from the Mathlib 2\pi convention by rescaling the frequency, and the factor (2\pi)^{-1} in front of the Fourier expression is the Jacobian of that rescaling.

So is the inversion formula that the abstract scheme asks for as a hypothesis: on a Euclidean input domain it is a theorem, fs_angularFourier_inversion_inner, Mathlib's inversion formula at a continuity point rescaled into the angular convention, and the constant (2\pi)^r it produces is the reciprocal of the inversion density \kappa=(2\pi)^{-r} the instance carries. The same rescaling matches the integrable Fourier transforms of the two conventions, which is what makes the inversion integrand integrable.

FS.FiniteField: the discrete case

Theorem3.2.5

uses 1used by 1✓L∃∀N

Master identity over a finite field. Steps 2 and 3 meet in the weight sum at a fixed bias frequency: at \omega\neq0 the change of variables turns it into Fourier inversion of f at x, and at \omega=0 the change of variables is unavailable and the sum collapses onto the total mass \sum_yf(y) instead. That asymmetry is the entire difference from the Euclidean case, and it is what produces the rank-one defect in the unconditional identity. Everything is a finite sum, so no analytic hypothesis appears anywhere in the file.

Lean code for Theorem3.2.5●2 theorems

theoremdefined in LeanRidgelet/FS/FiniteField.lean

complete

theorem LeanRidgelet.fs_finiteField_sum_slice.{u_1} {p : ℕ} [NeZero p]
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Fact (Nat.Prime p)]
  (f : (ι → ZMod p) → ℂ) (ω : ZMod p) (x : ι → ZMod p) :
  ∑ a, ZMod.piDFT f (ω • a) * ZMod.stdAddChar (ω * a ⬝ᵥ x) =
    if ω = 0 then ↑p ^ Fintype.card ι * ∑ y, f y
    else ↑p ^ Fintype.card ι * f x

theorem LeanRidgelet.fs_finiteField_sum_slice.{u_1}
  {p : ℕ} [NeZero p] {ι : Type u_1}
  [Fintype ι] [DecidableEq ι]
  [Fact (Nat.Prime p)]
  (f : (ι → ZMod p) → ℂ) (ω : ZMod p)
  (x : ι → ZMod p) :
  ∑ a,
      ZMod.piDFT f (ω • a) *
        ZMod.stdAddChar (ω * a ⬝ᵥ x) =
    if ω = 0 then
      ↑p ^ Fintype.card ι * ∑ y, f y
    else ↑p ^ Fintype.card ι * f x

The weight sum at a fixed bias frequency, which is where Steps 2 and 3 meet. At `ω ≠ 0` the
change of variables turns it into the Fourier inversion of `f` at `x`; at `ω = 0` the change of
variables is unavailable and the sum collapses onto the total mass of `f` instead.

This asymmetry is the whole difference between the finite field and the Euclidean case.

theoremdefined in LeanRidgelet/FS/FiniteField.lean

complete

theorem LeanRidgelet.fs_finiteField_synthesis_ridgelet.{u_1} {p : ℕ} [NeZero p]
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Fact (Nat.Prime p)]
  (σ ρ : ZMod p → ℂ) (f : (ι → ZMod p) → ℂ) (x : ι → ZMod p) :
  LeanRidgelet.finiteFieldSynthesis σ
      (LeanRidgelet.finiteFieldRidgelet ρ f) x =
    LeanRidgelet.finiteFieldPairing p ι σ ρ * f x +
      ↑p ^ Fintype.card ι / ↑p *
          (ZMod.dft σ 0 * (starRingEnd ℂ) (ZMod.dft ρ 0)) *
        ∑ y, f y

theorem LeanRidgelet.fs_finiteField_synthesis_ridgelet.{u_1}
  {p : ℕ} [NeZero p] {ι : Type u_1}
  [Fintype ι] [DecidableEq ι]
  [Fact (Nat.Prime p)] (σ ρ : ZMod p → ℂ)
  (f : (ι → ZMod p) → ℂ)
  (x : ι → ZMod p) :
  LeanRidgelet.finiteFieldSynthesis σ
      (LeanRidgelet.finiteFieldRidgelet ρ
        f)
      x =
    LeanRidgelet.finiteFieldPairing p ι σ
          ρ *
        f x +
      ↑p ^ Fintype.card ι / ↑p *
          (ZMod.dft σ 0 *
            (starRingEnd ℂ)
              (ZMod.dft ρ 0)) *
        ∑ y, f y

**The master identity.** With no hypothesis on the ridgelet function, the network built from
the ridgelet transform reproduces `⦅σ,ρ⦆ f` plus a rank-one defect carried by the bias frequency
`ω = 0`, where Step 2 breaks down. The defect is a multiple of the constant function `∑ y, f y`
and so cannot be absorbed into the scalar.

Lemma3.2.6

uses 1used by 0✓L∃∀N

Normalizing the ridgelet function. Subtracting its mean makes any \rho satisfy the vanishing-mean hypothesis, changes no nonzero bias frequency — the spectrum of a constant is supported at the origin — and therefore leaves the scalar (\!(\sigma,\rho)\!) unchanged. So the hypothesis is a normalization, not a restriction on which ridgelet functions may be used.

Lean code for Lemma3.2.6●4 declarations

defdefined in LeanRidgelet/FS/FiniteField.lean

complete

def LeanRidgelet.meanZeroPart (p : ℕ) [NeZero p] (ρ : ZMod p → ℂ) :
  ZMod p → ℂ

def LeanRidgelet.meanZeroPart (p : ℕ)
  [NeZero p] (ρ : ZMod p → ℂ) : ZMod p → ℂ

Implementation after :=

:=
  fun b => ρ b - (p : ℂ)⁻¹ * ∑ c : ZMod p, ρ c

The mean-zero part `ρ - p⁻¹ ∑ ρ` of a ridgelet function.

theoremdefined in LeanRidgelet/FS/FiniteField.lean

complete

theorem LeanRidgelet.fs_sum_meanZeroPart {p : ℕ} [NeZero p] (ρ : ZMod p → ℂ) :
  ∑ b, LeanRidgelet.meanZeroPart p ρ b = 0

theorem LeanRidgelet.fs_sum_meanZeroPart {p : ℕ}
  [NeZero p] (ρ : ZMod p → ℂ) :
  ∑ b, LeanRidgelet.meanZeroPart p ρ b = 0

The mean-zero part has vanishing mean.

theoremdefined in LeanRidgelet/FS/FiniteField.lean

complete

theorem LeanRidgelet.fs_dft_meanZeroPart {p : ℕ} [NeZero p] {ω : ZMod p}
  (hω : ω ≠ 0) (ρ : ZMod p → ℂ) :
  ZMod.dft (LeanRidgelet.meanZeroPart p ρ) ω = ZMod.dft ρ ω

theorem LeanRidgelet.fs_dft_meanZeroPart {p : ℕ}
  [NeZero p] {ω : ZMod p} (hω : ω ≠ 0)
  (ρ : ZMod p → ℂ) :
  ZMod.dft (LeanRidgelet.meanZeroPart p ρ)
      ω =
    ZMod.dft ρ ω

Subtracting the mean changes no nonzero bias frequency, since the spectrum of a constant is
supported at the origin.

theoremdefined in LeanRidgelet/FS/FiniteField.lean

complete

theorem LeanRidgelet.fs_finiteFieldPairing_meanZeroPart.{u_1} {p : ℕ} [NeZero p]
  {ι : Type u_1} [Fintype ι] (σ ρ : ZMod p → ℂ) :
  LeanRidgelet.finiteFieldPairing p ι σ
      (LeanRidgelet.meanZeroPart p ρ) =
    LeanRidgelet.finiteFieldPairing p ι σ ρ

theorem LeanRidgelet.fs_finiteFieldPairing_meanZeroPart.{u_1}
  {p : ℕ} [NeZero p] {ι : Type u_1}
  [Fintype ι] (σ ρ : ZMod p → ℂ) :
  LeanRidgelet.finiteFieldPairing p ι σ
      (LeanRidgelet.meanZeroPart p ρ) =
    LeanRidgelet.finiteFieldPairing p ι σ
      ρ

Subtracting the mean does not change the scalar of the reconstruction formula, because the
scalar only sees the nonzero bias frequencies.

FS.GroupConv: reduction to the Euclidean case

Theorem3.2.7

Statement uses 2

Statement dependency previews

Preview

Theorem 3.1.10

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

The reduction, and what it costs. The file is algebra. One identity does the work — pairing a filter of the span of the frame against any input is pairing their coordinate vectors — and everything else follows from it: the network is a Euclidean network at the coordinate vector of the translated input, the ridgelet transform is the Euclidean ridgelet transform of the pulled-back target, and the network's dependence on the input factors through those coordinates. Orthonormality of the frame is needed only where the coordinates have to recover the coefficients: in the ridgelet transform, and in identifying the projection with the identity on the span.

Lean code for Theorem3.2.7●3 theorems

theoremdefined in LeanRidgelet/FS/GroupConv.lean

complete

theorem LeanRidgelet.fs_frameCoord_frameVector.{u_1} {m : ℕ} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {fr : Fin m → H}
  (hfr : Orthonormal ℝ fr) (c : LeanRidgelet.InputSpace m) :
  LeanRidgelet.frameCoord fr (LeanRidgelet.frameVector fr c) = c

theorem LeanRidgelet.fs_frameCoord_frameVector.{u_1}
  {m : ℕ} {H : Type u_1}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {fr : Fin m → H}
  (hfr : Orthonormal ℝ fr)
  (c : LeanRidgelet.InputSpace m) :
  LeanRidgelet.frameCoord fr
      (LeanRidgelet.frameVector fr c) =
    c

For an orthonormal frame the coordinates recover the coefficients.

theoremdefined in LeanRidgelet/FS/GroupConv.lean

complete

theorem LeanRidgelet.fs_groupConvRidgelet_eq_euclidean.{u_1, u_2} {m : ℕ}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  {G : Type u_2} [Group G] {fr : Fin m → H} (hfr : Orthonormal ℝ fr)
  (ρ : ℝ → ℂ) (f : H → G → ℂ)
  (p : LeanRidgelet.RidgeletParameterSpace m) :
  LeanRidgelet.groupConvRidgelet fr ρ f p =
    LeanRidgelet.euclideanRidgeletTransform m 0 ρ
      (fun y ↦ f (LeanRidgelet.frameVector fr y) 1) p

theorem LeanRidgelet.fs_groupConvRidgelet_eq_euclidean.{u_1,
    u_2}
  {m : ℕ} {H : Type u_1}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {G : Type u_2}
  [Group G] {fr : Fin m → H}
  (hfr : Orthonormal ℝ fr) (ρ : ℝ → ℂ)
  (f : H → G → ℂ)
  (p :
    LeanRidgelet.RidgeletParameterSpace
      m) :
  LeanRidgelet.groupConvRidgelet fr ρ f
      p =
    LeanRidgelet.euclideanRidgeletTransform
      m 0 ρ
      (fun y ↦
        f (LeanRidgelet.frameVector fr y)
          1)
      p

The ridgelet transform is the Euclidean ridgelet transform of the target pulled back to the
coordinates of the frame.

theoremdefined in LeanRidgelet/FS/GroupConv.lean

complete

theorem LeanRidgelet.fs_groupConv_compat_of_mem.{u_1, u_2} {m : ℕ}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  {G : Type u_2} [Group G] {fr : Fin m → H} (hfr : Orthonormal ℝ fr)
  {T : G → H → H} (f : H → G → ℂ) {x : H} {g : G}
  (hx : T g⁻¹ x ∈ Submodule.span ℝ (Set.range fr)) :
  f (LeanRidgelet.frameProjection fr (T g⁻¹ x)) 1 = f (T g⁻¹ x) 1

theorem LeanRidgelet.fs_groupConv_compat_of_mem.{u_1,
    u_2}
  {m : ℕ} {H : Type u_1}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {G : Type u_2}
  [Group G] {fr : Fin m → H}
  (hfr : Orthonormal ℝ fr) {T : G → H → H}
  (f : H → G → ℂ) {x : H} {g : G}
  (hx :
    T g⁻¹ x ∈
      Submodule.span ℝ (Set.range fr)) :
  f
      (LeanRidgelet.frameProjection fr
        (T g⁻¹ x))
      1 =
    f (T g⁻¹ x) 1

First sufficient condition for compatibility: the translated input already lies in the span of
the frame.

The Euclidean reconstruction formula enters as a hypothesis rather than a fixed theorem, so the L¹ reconstruction of the L1 development and the Fourier slice scheme are both usable and the case commits to neither.

FS.Symmetric: the conditional case

Theorem3.2.8

Statement uses 2

Statement dependency previews

Preview

Theorem 3.1.15

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Reconstruction on a symmetric space, conditional on inversion. The rank-r instance of the abstract theorem, with the Helgason--Fourier inversion formula as an explicit hypothesis. Since the scale space is \mathbb R^r, the Jacobian exponent is the rank rather than the dimension of the space, which is the one structural difference from the Euclidean case.

Lean code for Theorem3.2.8●2 theorems

theoremdefined in LeanRidgelet/FS/Symmetric.lean

complete

theorem LeanRidgelet.horosphericalWeight_zero.{u_1, u_2} {r : ℕ} {X : Type u_1}
  {U : Type u_2} (cd : X → U → LeanRidgelet.InputSpace r) (x : X)
  (u : U) : LeanRidgelet.horosphericalWeight 0 cd x u = 1

theorem LeanRidgelet.horosphericalWeight_zero.{u_1,
    u_2}
  {r : ℕ} {X : Type u_1} {U : Type u_2}
  (cd : X → U → LeanRidgelet.InputSpace r)
  (x : X) (u : U) :
  LeanRidgelet.horosphericalWeight 0 cd x
      u =
    1

theoremdefined in LeanRidgelet/FS/Symmetric.lean

complete

theorem LeanRidgelet.fs_symmetric_reconstruction_of_inversion.{u_1, u_2} {r : ℕ}
  {X : Type u_1} {U : Type u_2} [MeasurableSpace U]
  (ν : MeasureTheory.Measure U) (ϱ : LeanRidgelet.InputSpace r)
  (cd : X → U → LeanRidgelet.InputSpace r) (Fσ Fρ : ℝ → ℂ)
  (Ff : LeanRidgelet.InputSpace r → U → ℂ) (W : ℝ)
  (cfun : LeanRidgelet.InputSpace r → ℂ) (f : X → ℂ)
  (hinv :
    ∀ (y : X),
      ∫ (lam : LeanRidgelet.InputSpace r),
          ∫ (u : U),
            Ff lam u * ↑(LeanRidgelet.harishChandraDensity W cfun lam) *
                LeanRidgelet.fourierSlicePhase (inner ℝ lam (cd y u)) *
              LeanRidgelet.horosphericalWeight ϱ cd y u ∂ν =
        f y)
  (x : X) :
  LeanRidgelet.symmetricFourierExpression ν ϱ cd Fσ
      (LeanRidgelet.separationOfVariables Ff
        (LeanRidgelet.harishChandraDensity W cfun) Fρ)
      x =
    LeanRidgelet.fourierSlicePairing (↑r) Fσ Fρ * f x

theorem LeanRidgelet.fs_symmetric_reconstruction_of_inversion.{u_1,
    u_2}
  {r : ℕ} {X : Type u_1} {U : Type u_2}
  [MeasurableSpace U]
  (ν : MeasureTheory.Measure U)
  (ϱ : LeanRidgelet.InputSpace r)
  (cd : X → U → LeanRidgelet.InputSpace r)
  (Fσ Fρ : ℝ → ℂ)
  (Ff : LeanRidgelet.InputSpace r → U → ℂ)
  (W : ℝ)
  (cfun : LeanRidgelet.InputSpace r → ℂ)
  (f : X → ℂ)
  (hinv :
    ∀ (y : X),
      ∫ (lam : LeanRidgelet.InputSpace r),
          ∫ (u : U),
            Ff lam u *
                  ↑(LeanRidgelet.harishChandraDensity
                      W cfun lam) *
                LeanRidgelet.fourierSlicePhase
                  (inner ℝ lam (cd y u)) *
              LeanRidgelet.horosphericalWeight
                ϱ cd y u ∂ν =
        f y)
  (x : X) :
  LeanRidgelet.symmetricFourierExpression
      ν ϱ cd Fσ
      (LeanRidgelet.separationOfVariables
        Ff
        (LeanRidgelet.harishChandraDensity
          W cfun)
        Fρ)
      x =
    LeanRidgelet.fourierSlicePairing (↑r)
        Fσ Fρ *
      f x

**The reconstruction formula on a noncompact symmetric space** (Theorem 5.2), as the instance
of the abstract scheme in which the input domain is `G/K`, the direction space is the boundary
`∂X`, the scale space is `𝔞* ≅ ℝ^r`, the weight is `e^{ϱ⟪x,u⟫}`, the Fourier data is the
Helgason--Fourier transform of the target and the inversion density is `|W|⁻¹|c(λ)|⁻²`.

The Helgason--Fourier inversion formula is the hypothesis. Mathlib carries none of the theory
needed to prove it — no Iwasawa decomposition, no spherical functions, no `c`-function — so it
enters here and only here, as an explicit hypothesis of a theorem.

Discharging the hypothesis in Euclidean polar coordinates would exhibit the same shape with r=1 and an honest direction space, and so keep the conditional theorem from being vacuous in a stronger sense than the one-point boundary already does. It is not here, and the obstacle is worth recording: the polar inversion formula needs \int_{\mathbb R}\int_{\mathbb S}|\lambda|^{m-1}G(\lambda u)=2\int_{\mathbb S}\int_0^\infty r^{m-1}G(ru), whose doubling step is invariance of the sphere measure under the antipodal map — a statement Mathlib does not have for Measure.toSphere. It is an upstream candidate in its own right, not an incidental step.

FS.DPlane: the pooling case

The case is large enough to have a directory of its own, LeanRidgelet/FS/DPlane/, split along the boundaries the article draws; FS.DPlane is the guide to it and carries the list of deviations. The paragraphs below follow those parts.

FS.DPlane.Defs: what every codimension shares

Theorem3.2.9

Statement uses 2

Statement dependency previews

Preview

Theorem 3.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

What the d-plane case rests on. The transform and its Fourier slice theorem are in the upstream-candidates chapter, in general codimension; on top of them sits the identity that over the Stiefel manifold the coefficient function is the d-plane transform of a fractional derivative of the target.

Lean code for Theorem3.2.9●3 declarations

defdefined in LeanRidgelet/FS/DPlane/Defs.lean

complete

def LeanRidgelet.dPlaneCoord.{u_1} {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (L : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) (x : E) :
  EuclideanSpace ℝ (Fin k)

def LeanRidgelet.dPlaneCoord.{u_1} {k : ℕ}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E)
  (x : E) : EuclideanSpace ℝ (Fin k)

Implementation after :=

:=
  WithLp.toLp 2 fun i => ⟪L (EuclideanSpace.single i (1 : ℝ)), x⟫

The coordinate vector `Aᵀ x` of the input against the frame `A = L`, the argument of the
multivariate activation.

defdefined in LeanRidgelet/FS/DPlane/Defs.lean

complete

def LeanRidgelet.stiefelSynthesis.{u_1} {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E))
  (σ : EuclideanSpace ℝ (Fin k) → ℂ)
  (γ :
    (EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) → EuclideanSpace ℝ (Fin k) → ℂ)
  (x : E) : ℂ

def LeanRidgelet.stiefelSynthesis.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (ν :
    MeasureTheory.Measure
      (EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E))
  (σ : EuclideanSpace ℝ (Fin k) → ℂ)
  (γ :
    (EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) →
      EuclideanSpace ℝ (Fin k) → ℂ)
  (x : E) : ℂ

Implementation after :=

:=
  ∫ L, (∫ b : EuclideanSpace ℝ (Fin k), γ L b * σ (dPlaneCoord L x - b)) ∂ν

The `d`-plane layer over the Stiefel manifold, `S[γ](x) = ∫ γ(U,b) σ(Uᵀx - b) dU db`, with the
weight ranging over orthonormal `k`-frames against a measure `ν` on them.

The measure is left as a parameter because the reconstruction formula fixes only the invariant one,
and that one now exists: `ContinuousLinearMap.stiefelMeasure` is the pushforward of the Haar
probability measure of the orthogonal group along its action on a frame. The Borel structure the
integral needs comes from `ContinuousLinearMap.instMeasurableSpaceLinearIsometry`.

theoremdefined in LeanRidgelet/FS/DPlane/Defs.lean

complete

theorem LeanRidgelet.fs_fourier_dPlaneTransform_fractional.{u_1} {k : ℕ}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : ℝ}
  {f g : E → ℂ} (hg : MeasureTheory.Integrable g MeasureTheory.volume)
  (hmul :
    ∀ (ξ : E),
      FourierTransform.fourier g ξ =
        ↑(‖ξ‖ ^ s) * FourierTransform.fourier f ξ)
  (L : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E)
  (ω : EuclideanSpace ℝ (Fin k)) :
  FourierTransform.fourier (MeasureTheory.dPlaneTransform g L) ω =
    ↑(‖ω‖ ^ s) * FourierTransform.fourier f (L ω)

theorem LeanRidgelet.fs_fourier_dPlaneTransform_fractional.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {s : ℝ} {f g : E → ℂ}
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hmul :
    ∀ (ξ : E),
      FourierTransform.fourier g ξ =
        ↑(‖ξ‖ ^ s) *
          FourierTransform.fourier f ξ)
  (L : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E)
  (ω : EuclideanSpace ℝ (Fin k)) :
  FourierTransform.fourier
      (MeasureTheory.dPlaneTransform g L)
      ω =
    ↑(‖ω‖ ^ s) *
      FourierTransform.fourier f (L ω)

**The identity behind the Stiefel reconstruction formula.** If `g` is a fractional derivative
of `f` of order `s`, in the sense that its Fourier transform is `‖ξ‖^s` times that of `f`, then the
bias spectrum of the `d`-plane transform of `g` along a frame is `‖ω‖^s` times the Fourier data of
`f` along that frame.

The article's separation-of-variables ansatz over the Stiefel manifold is
`γ♯(U,ω) = f̂(Uω)|Uω|^{d-t}`, which is exactly the right-hand side with `s = d - t`; so the
coefficient function is the `d`-plane transform of a fractional derivative of the target, and over
the Stiefel manifold the ridgelet transform degenerates to a Radon transform. The fractional
Laplacian is not in Mathlib, so its multiplier property is the hypothesis rather than a
definition.

The two conventions do not agree on what a fractional derivative is: a multiplier \|\xi\|^s in the Mathlib convention is (2\pi)^s\|\xi\|^s in the angular one, so the codimension-one statements carry their own angular form of fs_fourier_dPlaneTransform_fractional rather than reusing it. The frequency \omega=0, where the exponent arithmetic |\omega|^{d-t}|\omega|^t=|\omega|^d fails, is null over \mathbb R and the hypothesis is stated almost everywhere — the finite-field case is where that same point costs a rank-one defect instead.

FS.DPlane.CodimOne: the sphere

Theorem3.2.10

Statement uses 6

Statement dependency previews

Preview

Theorem 3.1.20

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Codimension one, where the Stiefel manifold is a sphere. The layer over the sphere carries no scale parameter, so Step 2 is absent and Step 1 needs no Fubini: with nothing to rescale, the bias frequency may stay inside the direction integral. What is left is the master identity, whose hypothesis is that \gamma^\sharp(\boldsymbol u,\omega)\sigma^\sharp(\omega) be a constant multiple of \widehat f(\omega\boldsymbol u)|\omega|^{m-1} almost everywhere in \omega, and whose proof is the two-sided polar formula followed by Fourier inversion. Everything the article's Appendix C needs at k=1 is fs_matrixPolarIntegration_codim_one, and the identification of the coefficient function with a Radon transform is the slice theorem in the angular convention.

Lean code for Theorem3.2.10●11 declarations

defdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

def LeanRidgelet.sphereSynthesis {m : ℕ} (σ : ℝ → ℂ)
  (γ : ↑(Metric.sphere 0 1) → ℝ → ℂ) (x : LeanRidgelet.InputSpace m) : ℂ

def LeanRidgelet.sphereSynthesis {m : ℕ}
  (σ : ℝ → ℂ)
  (γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m) : ℂ

Implementation after :=

:=
  ∫ u : sphere (0 : InputSpace m) 1,
      (∫ b : ℝ, γ u b * σ (inner ℝ (u : InputSpace m) x - b))
    ∂(volume : Measure (InputSpace m)).toSphere

The `d`-plane layer at codimension one, `S[γ](x) = ∫_{𝕊^{m-1}} ∫_ℝ γ(u,b) σ(⟪u,x⟫ - b) db du`:
the weight ranges over `V_{m,1} = 𝕊^{m-1}` against the surface measure and carries no scale
factor.

defdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

def LeanRidgelet.sphereFourierExpression {m : ℕ} (Fσ : ℝ → ℂ)
  (Γ : ↑(Metric.sphere 0 1) → ℝ → ℂ) (x : LeanRidgelet.InputSpace m) : ℂ

def LeanRidgelet.sphereFourierExpression
  {m : ℕ} (Fσ : ℝ → ℂ)
  (Γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m) : ℂ

Implementation after :=

:=
  (2 * (Real.pi : ℂ))⁻¹ *
    ∫ u : sphere (0 : InputSpace m) 1,
        (∫ ω : ℝ, Γ u ω * Fσ ω * fourierSlicePhase (ω * inner ℝ (u : InputSpace m) x))
      ∂(volume : Measure (InputSpace m)).toSphere

The Fourier expression of the codimension-one layer, the output of Step 1:
`S[γ](x) = (2π)⁻¹ ∫_{𝕊^{m-1}} ∫_ℝ γ♯(u,ω) σ♯(ω) e^{iω⟪u,x⟫} dω du`.

theoremdefined in LeanRidgelet/FS/DPlane/Defs.lean

complete

theorem LeanRidgelet.norm_smul_coe_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : ℝ)
  (u : ↑(Metric.sphere 0 1)) : ‖b • ↑u‖ = |b|

theorem LeanRidgelet.norm_smul_coe_sphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (b : ℝ)
  (u : ↑(Metric.sphere 0 1)) :
  ‖b • ↑u‖ = |b|

Scaling a unit vector scales the norm: at `k = 1` the article's weight `|U b|^{m-k}` is
`|b|^{m-1}`.

theoremdefined in LeanRidgelet/FS/DPlane/Defs.lean

complete

theorem LeanRidgelet.fs_matrixPolarIntegration_codim_one (m : ℕ)
  [Nontrivial (LeanRidgelet.InputSpace m)]
  {F : LeanRidgelet.InputSpace m → ℂ}
  (hF : MeasureTheory.Integrable F MeasureTheory.volume) :
  2 • ∫ (x : LeanRidgelet.InputSpace m), F x =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ),
        ‖b • ↑u‖ ^ (Module.finrank ℝ (LeanRidgelet.InputSpace m) - 1) •
          F (b • ↑u) ∂MeasureTheory.volume.toSphere

theorem LeanRidgelet.fs_matrixPolarIntegration_codim_one
  (m : ℕ)
  [Nontrivial (LeanRidgelet.InputSpace m)]
  {F : LeanRidgelet.InputSpace m → ℂ}
  (hF :
    MeasureTheory.Integrable F
      MeasureTheory.volume) :
  2 •
      ∫ (x : LeanRidgelet.InputSpace m),
        F x =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ),
        ‖b • ↑u‖ ^
            (Module.finrank ℝ
                (LeanRidgelet.InputSpace
                  m) -
              1) •
          F
            (b •
              ↑u) ∂MeasureTheory.volume.toSphere

**The matrix polar integration formula at codimension one** — the article's Lemma C.2 with
`k = 1`, where the Stiefel manifold `V_{m,1}` is the unit sphere and the constant is
`c_{m,1} = ∫_{𝕊⁰ × V_{m,0}} = 2`.

In this case the formula is the two-sided polar formula of `ToMathlib.PolarCoordinates`: the
article's weight `|U b|^{m-k}` is `‖b u‖^{m-1} = |b|^{m-1}`, and its constant is the factor `2` of
the double cover. So codimension one needs no Stiefel machinery at all, which is why the `k = 1`
reconstruction formulas are the ones within reach.

For general `k` the formula does need an invariant measure on `V_{m,k}`, and Mathlib has none: no
Stiefel manifold, no compactness or Haar measure plumbed for the orthogonal group, and no
invariance of the sphere measure under rotations. The development plan records the route and the
two gaps.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_sphere_fourierExpression_of_bias {m : ℕ} (σ Fσ : ℝ → ℂ)
  (γ Γ : ↑(Metric.sphere 0 1) → ℝ → ℂ) (x : LeanRidgelet.InputSpace m)
  (hbias :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ), γ u b * σ (inner ℝ (↑u) x - b) =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            Γ u ω * Fσ ω *
              LeanRidgelet.fourierSlicePhase (ω * inner ℝ (↑u) x)) :
  LeanRidgelet.sphereSynthesis σ γ x =
    LeanRidgelet.sphereFourierExpression Fσ Γ x

theorem LeanRidgelet.fs_sphere_fourierExpression_of_bias
  {m : ℕ} (σ Fσ : ℝ → ℂ)
  (γ Γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hbias :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ),
          γ u b * σ (inner ℝ (↑u) x - b) =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            Γ u ω * Fσ ω *
              LeanRidgelet.fourierSlicePhase
                (ω * inner ℝ (↑u) x)) :
  LeanRidgelet.sphereSynthesis σ γ x =
    LeanRidgelet.sphereFourierExpression
      Fσ Γ x

**Step 1 at codimension one**: the layer equals its Fourier expression.

The analytic input is the one-dimensional bias identity at each direction, exactly as in the
abstract scheme, and it enters as the hypothesis `hbias` for the same reason: which form of it is
available depends on the class the activation is taken from, and the activations of the Stiefel
theorem are tempered distributions rather than integrable functions. Unlike in the abstract scheme
no Fubini rearrangement is needed, because with no scale parameter to change variables in the bias
frequency may stay inside the direction integral.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_sphere_reconstruction_of_inversion {m : ℕ}
  [Nontrivial (LeanRidgelet.InputSpace m)] (c : ℂ) (Fσ : ℝ → ℂ)
  (Γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (Ff f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (hansatz :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∀ᵐ (ω : ℝ), Γ u ω * Fσ ω = c * ↑(|ω| ^ (↑m - 1)) * Ff (ω • ↑u))
  (hF :
    MeasureTheory.Integrable
      (fun ξ ↦ Ff ξ * LeanRidgelet.fourierSlicePhase (inner ℝ ξ x))
      MeasureTheory.volume)
  (hinv :
    ∫ (ξ : LeanRidgelet.InputSpace m),
        Ff ξ * LeanRidgelet.fourierSlicePhase (inner ℝ ξ x) =
      ↑((2 * Real.pi) ^ m) * f x) :
  LeanRidgelet.sphereFourierExpression Fσ Γ x =
    c * 2 * ↑((2 * Real.pi) ^ (m - 1)) * f x

theorem LeanRidgelet.fs_sphere_reconstruction_of_inversion
  {m : ℕ}
  [Nontrivial (LeanRidgelet.InputSpace m)]
  (c : ℂ) (Fσ : ℝ → ℂ)
  (Γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (Ff f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hansatz :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∀ᵐ (ω : ℝ),
        Γ u ω * Fσ ω =
          c * ↑(|ω| ^ (↑m - 1)) *
            Ff (ω • ↑u))
  (hF :
    MeasureTheory.Integrable
      (fun ξ ↦
        Ff ξ *
          LeanRidgelet.fourierSlicePhase
            (inner ℝ ξ x))
      MeasureTheory.volume)
  (hinv :
    ∫ (ξ : LeanRidgelet.InputSpace m),
        Ff ξ *
          LeanRidgelet.fourierSlicePhase
            (inner ℝ ξ x) =
      ↑((2 * Real.pi) ^ m) * f x) :
  LeanRidgelet.sphereFourierExpression Fσ
      Γ x =
    c * 2 * ↑((2 * Real.pi) ^ (m - 1)) *
      f x

**The reconstruction formula of the Fourier slice method at codimension one.** The
separation-of-variables condition of the Stiefel case is that the product of the bias spectrum of
the coefficient function with the activation spectrum be a constant multiple of
`f̂(ω u) |ω|^{m-1}` — the article's `eq:sov.hom`, whose auxiliary factor `φ♯` is required to be
constant. Under it the network reproduces the target up to the constant `c · c_{m,1} (2π)^{m-1}`.

Both integrals of the derivation are absolutely convergent by hypothesis, which is the article's
standing assumption of Section 2. The direction integral is then evaluated by the matrix polar
integration formula `fs_matrixPolarIntegration_codim_one`, whose constant `c_{m,1} = 2` is the
double cover `(ω, u) ↦ ω u` of `ℝ^m ∖ {0}`, and the remaining Euclidean integral by the inversion
formula, which is the hypothesis `hinv`; on a Euclidean input domain that hypothesis is the theorem
`fs_angularFourier_inversion_inner`, and its constant is the `(2π)^m` appearing here.

The hypothesis is on the *product* `γ♯(u,ω) σ♯(ω)`, so the activation spectrum need not be even;
this is what lets the classical Radon formula be an instance.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_angularFourier_slice_radonTransform {m : ℕ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  {u : LeanRidgelet.InputSpace m} (hu : ‖u‖ = 1) (ω : ℝ) :
  LeanRidgelet.Fourier.angularFourierIntegralInner
      (MeasureTheory.radonTransform f u) ω =
    LeanRidgelet.Fourier.angularFourierIntegralInner f (ω • u)

theorem LeanRidgelet.fs_angularFourier_slice_radonTransform
  {m : ℕ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  {u : LeanRidgelet.InputSpace m}
  (hu : ‖u‖ = 1) (ω : ℝ) :
  LeanRidgelet.Fourier.angularFourierIntegralInner
      (MeasureTheory.radonTransform f u)
      ω =
    LeanRidgelet.Fourier.angularFourierIntegralInner
      f (ω • u)

**The Fourier slice theorem in the article's angular convention** at codimension one: the bias
spectrum of the Radon transform of `f` along a unit direction is the angular Fourier data of `f` on
the ray through that direction. Rescaling the frequency does not disturb the slice theorem.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_angularFourier_radonTransform_fractional {m : ℕ} {s : ℝ}
  {f g : LeanRidgelet.InputSpace m → ℂ}
  (hg : MeasureTheory.Integrable g MeasureTheory.volume)
  (hmul :
    ∀ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner g ξ =
        ↑(‖ξ‖ ^ s) *
          LeanRidgelet.Fourier.angularFourierIntegralInner f ξ)
  {u : LeanRidgelet.InputSpace m} (hu : ‖u‖ = 1) (ω : ℝ) :
  LeanRidgelet.Fourier.angularFourierIntegralInner
      (MeasureTheory.radonTransform g u) ω =
    ↑(|ω| ^ s) *
      LeanRidgelet.Fourier.angularFourierIntegralInner f (ω • u)

theorem LeanRidgelet.fs_angularFourier_radonTransform_fractional
  {m : ℕ} {s : ℝ}
  {f g : LeanRidgelet.InputSpace m → ℂ}
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hmul :
    ∀ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner
          g ξ =
        ↑(‖ξ‖ ^ s) *
          LeanRidgelet.Fourier.angularFourierIntegralInner
            f ξ)
  {u : LeanRidgelet.InputSpace m}
  (hu : ‖u‖ = 1) (ω : ℝ) :
  LeanRidgelet.Fourier.angularFourierIntegralInner
      (MeasureTheory.radonTransform g u)
      ω =
    ↑(|ω| ^ s) *
      LeanRidgelet.Fourier.angularFourierIntegralInner
        f (ω • u)

**The coefficient function is the Radon transform of a fractional derivative.** If `g` is the
fractional derivative of order `s` of `f`, in the sense that its angular Fourier transform is
`‖ξ‖^s` times that of `f`, then the bias spectrum of `P_d[g](u,·)` is `|ω|^s` times the Fourier
data of `f` along `u`.

This is the codimension-one form of `fs_fourier_dPlaneTransform_fractional`, in the convention the
reconstruction formula is stated in — the two conventions do not agree here, since a multiplier
`‖ξ‖^s` becomes `(2π)^s ‖ξ‖^s` under the rescaling of the frequency. The fractional Laplacian is
not in Mathlib, so its multiplier property is the hypothesis rather than a definition.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_ae_ne_zero : ∀ᵐ (ω : ℝ), ω ≠ 0

theorem LeanRidgelet.fs_ae_ne_zero :
  ∀ᵐ (ω : ℝ), ω ≠ 0

Over `ℝ` the singular frequency is negligible, unlike over a finite field where it is an
atom.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_stiefel_reconstruction_codim_one {m : ℕ}
  [Nontrivial (LeanRidgelet.InputSpace m)] (t : ℝ) (σ : ℝ → ℂ)
  (f g : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume)
  (hx : ContinuousAt f x)
  (hg : MeasureTheory.Integrable g MeasureTheory.volume)
  (hfrac :
    ∀ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner g ξ =
        ↑(‖ξ‖ ^ (↑m - 1 - t)) *
          LeanRidgelet.Fourier.angularFourierIntegralInner f ξ)
  (hbias :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ),
          MeasureTheory.radonTransform g (↑u) b *
            σ (inner ℝ (↑u) x - b) =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            LeanRidgelet.Fourier.angularFourierIntegralInner
                  (MeasureTheory.radonTransform g ↑u) ω *
                ↑(|ω| ^ t) *
              LeanRidgelet.fourierSlicePhase (ω * inner ℝ (↑u) x)) :
  LeanRidgelet.sphereSynthesis σ
      (fun u ↦ MeasureTheory.radonTransform g ↑u) x =
    2 * ↑((2 * Real.pi) ^ (m - 1)) * f x

theorem LeanRidgelet.fs_stiefel_reconstruction_codim_one
  {m : ℕ}
  [Nontrivial (LeanRidgelet.InputSpace m)]
  (t : ℝ) (σ : ℝ → ℂ)
  (f g : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume)
  (hx : ContinuousAt f x)
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hfrac :
    ∀ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner
          g ξ =
        ↑(‖ξ‖ ^ (↑m - 1 - t)) *
          LeanRidgelet.Fourier.angularFourierIntegralInner
            f ξ)
  (hbias :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ),
          MeasureTheory.radonTransform g
              (↑u) b *
            σ (inner ℝ (↑u) x - b) =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            LeanRidgelet.Fourier.angularFourierIntegralInner
                  (MeasureTheory.radonTransform
                    g ↑u)
                  ω *
                ↑(|ω| ^ t) *
              LeanRidgelet.fourierSlicePhase
                (ω * inner ℝ (↑u) x)) :
  LeanRidgelet.sphereSynthesis σ
      (fun u ↦
        MeasureTheory.radonTransform g ↑u)
      x =
    2 * ↑((2 * Real.pi) ^ (m - 1)) * f x

**The reconstruction formula over the Stiefel manifold at codimension one** — the article's
`thm:stiefel` with `k = 1`, where the Stiefel manifold is the unit sphere and `c_{m,1} = 2`.

The activation has spectrum `σ♯(ω) = |ω|^t`, and the coefficient function is the Radon transform of
the fractional derivative `g = △^{(d-t)/2} f` of the target, `d = m - 1`: this is the article's
`R[f](U,b) = P_d[△^{(d-t)/2}f](U,b)`, whose bias spectrum
`fs_angularFourier_radonTransform_fractional` computes. The conclusion is
`S[R[f]](x) = c_{m,1} (2π)^{d} f(x)`.

*The constant is the reciprocal of the article's*; see the *Deviations from the article* section of
this module, and `fs_radon_reconstruction_codim_one` for the independent confirmation.

theoremdefined in LeanRidgelet/FS/DPlane/CodimOne.lean

complete

theorem LeanRidgelet.fs_radon_reconstruction_codim_one {m : ℕ}
  [Nontrivial (LeanRidgelet.InputSpace m)] (σ : ℝ → ℂ)
  (f : LeanRidgelet.InputSpace m → ℂ) (γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume)
  (hx : ContinuousAt f x)
  (hγ :
    ∀ (u : ↑(Metric.sphere 0 1)) (ω : ℝ),
      LeanRidgelet.Fourier.angularFourierIntegralInner (γ u) ω =
        Complex.I * ↑ω * ↑(|ω| ^ (↑m - 1)) *
          LeanRidgelet.Fourier.angularFourierIntegralInner
            (MeasureTheory.radonTransform f ↑u) ω)
  (hbias :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ), γ u b * σ (inner ℝ (↑u) x - b) =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            LeanRidgelet.Fourier.angularFourierIntegralInner (γ u) ω *
                (Complex.I * ↑ω)⁻¹ *
              LeanRidgelet.fourierSlicePhase (ω * inner ℝ (↑u) x)) :
  LeanRidgelet.sphereSynthesis σ γ x =
    2 * ↑((2 * Real.pi) ^ (m - 1)) * f x

theorem LeanRidgelet.fs_radon_reconstruction_codim_one
  {m : ℕ}
  [Nontrivial (LeanRidgelet.InputSpace m)]
  (σ : ℝ → ℂ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (γ : ↑(Metric.sphere 0 1) → ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hFf :
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume)
  (hx : ContinuousAt f x)
  (hγ :
    ∀ (u : ↑(Metric.sphere 0 1)) (ω : ℝ),
      LeanRidgelet.Fourier.angularFourierIntegralInner
          (γ u) ω =
        Complex.I * ↑ω *
            ↑(|ω| ^ (↑m - 1)) *
          LeanRidgelet.Fourier.angularFourierIntegralInner
            (MeasureTheory.radonTransform
              f ↑u)
            ω)
  (hbias :
    ∀ (u : ↑(Metric.sphere 0 1)),
      ∫ (b : ℝ),
          γ u b * σ (inner ℝ (↑u) x - b) =
        (2 * ↑Real.pi)⁻¹ *
          ∫ (ω : ℝ),
            LeanRidgelet.Fourier.angularFourierIntegralInner
                  (γ u) ω *
                (Complex.I * ↑ω)⁻¹ *
              LeanRidgelet.fourierSlicePhase
                (ω * inner ℝ (↑u) x)) :
  LeanRidgelet.sphereSynthesis σ γ x =
    2 * ↑((2 * Real.pi) ^ (m - 1)) * f x

**The classical Radon formula** of Carroll--Dickinson and Ito — the article's `thm:ito.radon` —
as an instance of the codimension-one reconstruction formula.

The activation is the Heaviside step function, whose spectrum is `πδ(ω) + (iω)^{-1}`; its
homogeneous part `(iω)^{-1}` is the hypothesis `hbias` here. The coefficient function is
`∂_b(-△_b)^{(m-1)/2} P_d[f](u,b)`, whose bias spectrum is `iω|ω|^{m-1}` times that of the Radon
transform — the hypothesis `hγ`. The conclusion `S[γ](x) = 2(2π)^{m-1} f(x)` is the classical
formula solved for `S[γ]`, and its constant is the reciprocal of the `(2(2π)^{m-1})^{-1}` the
article quotes: this is the independent confirmation of the constant of
`fs_stiefel_reconstruction_codim_one`.

This is *not* the `t = -1` instance of that theorem. The step function's spectrum
`(iω)^{-1} = -i sgn(ω)|ω|^{-1}` is not `|ω|^{-1}`, and the odd factor is exactly what turns the
coefficient function `△_b^{m/2} P_d[f]` of `thm:stiefel` at `t = -1` into the classical
`∂_b(-△_b)^{(m-1)/2} P_d[f]`. Both are instances of `fs_sphere_reconstruction_of_inversion`, whose
hypothesis constrains only the product of the two spectra.

FS.DPlane.Stiefel: general codimension, and the inversion formula

The Stiefel case in general codimension is fs_dplane_stiefel, and it is the same three moves with the sphere replaced by the Stiefel manifold: the measure theory it rests on — a compact orthogonal group, an invariant measure on the Stiefel manifold, uniqueness of the rotation-invariant measure on the sphere, and the matrix polar integration formula — is all in the upstream-candidates chapter, none of it being in Mathlib. The article's own form of the theorem follows by specializing the auxiliary factor to 1, the coefficient function being the d-plane transform of a fractional derivative; the fractional Laplacian enters only through its multiplier property in the angular convention, which is a different statement from the Mathlib-convention one because the rescaling of the frequency changes the multiplier by (2\pi)^s.

Neither the Stiefel case nor the similitude case carries the article's standing absolute-convergence assumption. The two hypotheses of the matrix polar integration formula are discharged in the upstream-candidates chapter from strong measurability of the Fourier data — the unsigned form of the formula computes the integral of the norm, and almost every fibre of a finite integral is finite — so the master identities ask for measurability and the article's own form of thm:stiefel asks for nothing at all beyond integrability of the target and of its Fourier transform.

FS.DPlane.Similitude: the scale that does not factor out

The similitude case is fs_dplane_similitude. It is the one place where the scale genuinely interacts with the frequency — the two couple through y=ar, so the network is not a scale mixture of Stiefel networks — and the interaction is handled by putting the Fubini exchange into Step 1, where the article puts it, after which the assembly needs polar coordinates in the frequency, a one-dimensional substitution, and the direction average, and no further exchange.

FS.DPlane.Affine: all full-column-rank matrices

The full-column-rank case is fs_dplane_affine, formalized in the singular value coordinates A=UDV^\top because the Jacobian \mathrm dA=\delta(D)\,\mathrm dD\,\mathrm dU\,\mathrm dV that converts them to Lebesgue measure on the matrix space — the article's Lemma C.3 — is not: its published proof goes through exterior differential forms, and Mathlib has singular values but not the decomposition, nor the Jacobian of the matrix polar decomposition, nor Weyl's integration formula for real symmetric matrices. The weight is therefore a parameter of the layer, which costs little: it enters the separation-of-variables condition only as a factor of the coefficient function, and the article's coefficient function carries its reciprocal, so the two cancel and the reconstruction formula holds for every weight. What the derivation needs instead is the rotation of the frequency by V and the coordinatewise trade of the singular values against it, mathlib_diagonal_scaling, after which the matrix polar integration formula finishes exactly as in the Stiefel case. The fractional Laplacian as a Fourier multiplier is a further upstream candidate; where it is needed it enters as a multiplier hypothesis, never as a definition, and its multivariate form is what specializing the general-codimension identity to the article's σ♯ = |ω|^t family would need.

FS.DPlane.Consistency: the two developments agree at codimension one

That the two developments are the same construction is fs_stiefelSynthesis_codimOne: at k=1 the layer over the Stiefel manifold is the layer over the sphere, up to the total mass of the surface measure. Three identifications go into it, all of them in the upstream-candidates chapter — of the two parameter spaces, by mathlib_stiefel_codim_one; of the bias space \mathbb R^1 with \mathbb R; and of the frame coordinate with the inner product against the unit vector, which is the transpose identity at k=1.