Lean Ridgelet Blueprint

3.1. Fourier slice method: arXiv:2402.15984 implementation map🔗

The definitions and numbered results of

S. Sonoda, I. Ishikawa and M. Ikeda, A unified Fourier slice method to derive ridgelet transform for a variety of depth-2 neural networks, arXiv:2402.15984,

in publication order, each linked to the declaration carrying it. This chapter is the place to check what of that article is formalized.

Where the other two developments establish what the ridgelet transform of a depth-2 fully-connected network on a Euclidean space is, this one abstracts the derivation and runs it on other input domains. The article's contribution is a three-step procedure: turn the network into its Fourier expression, change variables in the scale parameter so that the feature map splits into a principal and an auxiliary factor, and close with a separation-of-variables ansatz for the unknown coefficient function. Accordingly the formalization centres on one conditional theorem carrying the three steps, and each case supplies an inversion formula on its own domain, the Jacobian of the change of variables, and the integrability needed to exchange the order of integration. An inversion formula out of reach of the current Mathlib enters as an explicit hypothesis of a theorem; it is never a structure field, a typeclass field, or an axiom.

Status: Sections 2--7 are complete except for the inversion formula of Section 5, which Lean takes as a hypothesis; Section 6 has its transform, its slice theorem, its inversion formula and all three of its reconstruction formulas — over the Stiefel manifold, over the similitude group and over all full-column-rank matrices — in every codimension. The measure theory the general codimension needs is in the ToMathlib / Invariant geometry page, none of it being in Mathlib. Nodes with no Lean declaration record what is still to be proved. Three nodes carry a sorry: the Jacobian of the singular value decomposition, and the Helgason--Fourier inversion formula on each of real hyperbolic space and the manifold of positive definite matrices. No proof in the development depends on either.

Section 2: the method

Definition3.1.1
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 3.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

The Fourier slice pairing. For a scale dimension r, an activation spectrum \sigma^\sharp and a ridgelet spectrum \rho^\sharp, (\!(\sigma,\rho)\!)_r:=\frac{1}{2\pi}\int_{\omega\neq0}\sigma^\sharp(\omega)\overline{\rho^\sharp(\omega)}\,|\omega|^{-r}\,\mathrm d\omega. This one scalar is the factor left in front of the reconstructed function in every case of the article: only r, the dimension of the scale variable, changes. What differs between the cases is not the pairing but the normalization of the inversion formula, which the separation-of-variables ansatz absorbs into the coefficient function. The restriction to \omega\neq0 is where the change of variables \boldsymbol a\mapsto\omega\boldsymbol a is a bijection; over \mathbb R the excluded point is null, which is why the article leaves the restriction implicit.

Lean code for Definition3.1.11 definition
  • complete
    def LeanRidgelet.fourierSlicePairing (r : ) (  :   ) : 
    def LeanRidgelet.fourierSlicePairing (r : )
      (  :   ) : 
    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. 
Theorem3.1.2
Statement uses 2
Statement dependency previews
Preview
Definition 3.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 3.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

The three steps. Given a domain X, a direction space U, a composite distance \pi:X\times U\to V into a finite-dimensional real inner product space, a weight w, Fourier data F and an inversion density \kappa satisfying the inversion formula f(x)=\int F(\lambda,u)\kappa(\lambda)e^{i\langle\lambda,\pi(x,u)\rangle}w(x,u), the network in Fourier expression form, evaluated at the separation-of-variables coefficient \gamma^\sharp(a,u,\omega)=F(\omega a,u)\kappa(\omega a)\overline{\rho^\sharp(\omega)}, equals (\!(\sigma,\rho)\!)_r\,f with r=\dim V.

Lean code for Theorem3.1.28 declarations
  • 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)
      ( :   ) (Γ : 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)
      ( :   ) (Γ : 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. 
  • complete
    def LeanRidgelet.separationOfVariables.{u_1, u_2} {V : Type u_1}
      [NormedAddCommGroup V] [InnerProductSpace  V] {U : Type u_2}
      (F : V  U  ) (κ : V  ) ( :   ) : 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  )
      ( :   ) : 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`. 
  • 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 : 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 κ  a u ω *  ω *
                LeanRidgelet.fourierSlicePhase (ω * inner  a (π x u)) *
              w x u ν μ =
         ω * (starRingEnd ) ( ω) * (|ω| ^ (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 : 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 κ  a u ω *
                   ω *
                LeanRidgelet.fourierSlicePhase
                  (ω * inner  a (π x u)) *
              w x u ν μ =
         ω * (starRingEnd ) ( ω) *
            (|ω| ^ (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. 
  • 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 ν] (σ  :   )
      (γ Γ : 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 ω *  ω *
                    LeanRidgelet.fourierSlicePhase (ω * inner  a (π x u)) *
                  w x u)
      (hint :
        MeasureTheory.Integrable
          (fun p 
            Γ p.2.1 p.2.2 p.1 *  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 μ ν  Γ π 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 ν] (σ  :   )
      (γ Γ : 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 ω *  ω *
                    LeanRidgelet.fourierSlicePhase
                      (ω *
                        inner  a (π x u)) *
                  w x u)
      (hint :
        MeasureTheory.Integrable
          (fun p 
            Γ p.2.1 p.2.2 p.1 *  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
          μ ν  Γ π 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 : 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 μ ν 
          (LeanRidgelet.separationOfVariables F κ ) π w x =
        LeanRidgelet.fourierSlicePairing (↑(Module.finrank  V))   * 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 : 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
          μ ν 
          (LeanRidgelet.separationOfVariables
            F κ )
          π w x =
        LeanRidgelet.fourierSlicePairing
            (↑(Module.finrank  V))   *
          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. 

That inversion formula is the only hypothesis of the reconstruction theorem: no integrability condition appears in it. 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, and the change of variables of Step 2 holds for every integrand because both sides degenerate together.

Step 1, which turns the network as the article writes it into the Fourier expression above, is where the analysis and the integrability live. Its analytic input is one-dimensional — at a fixed weight and direction, convolving in the bias and inverting — and is a hypothesis, since which form of it is available depends on the class the activation is taken from. It is discharged for an integrable activation over \mathbb R and, as a finite-sum identity, over a finite field. The rest is Fubini, moving the bias frequency outside the weight and direction integrals, which is the article's standing assumption that the triple integral converges absolutely.

Theorem3.1.3
Statement uses 2
Statement dependency previews
Preview
Definition 3.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 6
Reverse dependency previews
Preview
Theorem 3.1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Reconstruction formula for the fully-connected network (Theorem 1.1). The Euclidean instance of the method: the direction space is a point, so the weight is a plain vector of \mathbb R^m, the composite distance is the identity, the weight function is 1, and the Jacobian exponent is r=m. What remains is the inversion density \kappa=(2\pi)^{-m}, which is the hypothesis.

Lean code for Theorem3.1.32 theorems
  • 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`. 
  • complete
    theorem LeanRidgelet.fs_reconstruction_euclidean (m : ) (  :   )
      (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 ()) 
          (LeanRidgelet.separationOfVariables (fun ξ x  Ff ξ) κ )
          (fun y x  y) (fun x x_1  1) x =
        LeanRidgelet.fourierSlicePairing (↑m)   * f x
    theorem LeanRidgelet.fs_reconstruction_euclidean
      (m : ) (  :   )
      (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 ()) 
          (LeanRidgelet.separationOfVariables
            (fun ξ x  Ff ξ) κ )
          (fun y x  y) (fun x x_1  1) x =
        LeanRidgelet.fourierSlicePairing (↑m)
              *
          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 `κ`. 
Theorem3.1.4
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

Agreement with the L1 development. Two identities check the abstraction against a formalization that predates it and was built independently. The separation-of-variables ansatz, specialized to the Euclidean setting at homogeneity index s=0, is exactly the Fourier expression eq:fstridge of the classical ridgelet transform; and the L1 admissibility constant is (2\pi)^m times the Fourier slice pairing of the same two spectra.

Lean code for Theorem3.1.42 theorems
  • complete
    theorem LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform (m : )
      {ψ :   } {f : LeanRidgelet.InputSpace m  }
      (hf : MeasureTheory.Integrable f MeasureTheory.volume)
      ( : 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)
      ( :
        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. 
  • complete
    theorem LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing (m : )
      (hm : 1  m) (ψ  :   ) :
      LeanRidgelet.admissibilityConstant m ψ  =
        (2 * Real.pi) ^ m *
          LeanRidgelet.fourierSlicePairing (↑m) 
            (LeanRidgelet.angularFourier1D ψ)
    theorem LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
      (m : ) (hm : 1  m) (ψ  :   ) :
      LeanRidgelet.admissibilityConstant m ψ
           =
        (2 * Real.pi) ^ m *
          LeanRidgelet.fourierSlicePairing
            (↑m) 
            (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`. 

The factor (2\pi)^m is not a discrepancy but the place where the normalization of the inversion formula sits: the article's coefficient function does not carry the inversion density, so its constant part ends up in the article's (\!(\sigma,\rho)\!), whereas the ansatz here carries \kappa. The article itself states the Euclidean constant without the factor (2\pi)^{m-1} in Section 1 and with it in Section 2; the latter is the one consistent with the derivation and with the L1 development.

Section 3: networks on a finite field

Definition3.1.5
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 3.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Network, ridgelet transform and scalar on \mathbb F_p^m. S[\gamma](x)=\sum_{(a,b)}\gamma(a,b)\sigma(a\cdot x-b), R[f;\rho](a,b)=\sum_xf(x)\overline{\rho(a\cdot x-b)}, and (\!(\sigma,\rho)\!)=|\mathbb F_p|^{m-1}\sum_{\omega\neq0}\sigma^\sharp(\omega)\overline{\rho^\sharp(\omega)}, all sums finite. The dimension is Fintype.card ι, and the scalar is written with p^m/p so that it is also correct for m=0.

Lean code for Definition3.1.53 definitions
  • complete
    def LeanRidgelet.finiteFieldSynthesis.{u_1} {p : } [NeZero p]
      {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : ZMod p  )
      (γ : LeanRidgelet.FiniteFieldParameter p ι  ) (x : ι  ZMod p) : 
    def LeanRidgelet.finiteFieldSynthesis.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      (σ : ZMod p  )
      (γ :
        LeanRidgelet.FiniteFieldParameter p
            ι 
          )
      (x : ι  ZMod p) : 
    Implementation after :=
    :=
      ∑ q : FiniteFieldParameter p ι, γ q * σ (q.1 ⬝ᵥ x - q.2)
    The depth-2 fully-connected network over `𝔽_p`,
    `S[γ](x) = ∑_{(a,b)} γ(a,b) σ(a ⬝ x - b)`. 
  • complete
    def LeanRidgelet.finiteFieldRidgelet.{u_1} {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι] (ρ : ZMod p  ) (f : (ι  ZMod p)  )
      (q : LeanRidgelet.FiniteFieldParameter p ι) : 
    def LeanRidgelet.finiteFieldRidgelet.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      (ρ : ZMod p  ) (f : (ι  ZMod p)  )
      (q :
        LeanRidgelet.FiniteFieldParameter p
          ι) :
      
    Implementation after :=
    :=
      ∑ x : ι → ZMod p, f x * conj (ρ (q.1 ⬝ᵥ x - q.2))
    The ridgelet transform over `𝔽_p`,
    `R[f;ρ](a,b) = ∑_x f(x) conj (ρ (a ⬝ x - b))`. 
  • complete
    def LeanRidgelet.finiteFieldPairing.{u_2} (p : ) (ι : Type u_2) [NeZero p]
      [Fintype ι] (σ ρ : ZMod p  ) : 
    def LeanRidgelet.finiteFieldPairing.{u_2}
      (p : ) (ι : Type u_2) [NeZero p]
      [Fintype ι] (σ ρ : ZMod p  ) : 
    Implementation after :=
    :=
      (p : ℂ) ^ Fintype.card ι / p *
        ∑ ω ∈ ({0} : Finset (ZMod p))ᶜ, dft σ ω * conj (dft ρ ω)
    The scalar `⦅σ,ρ⦆ = |𝔽_p|^{m-1} ∑_{ω ≠ 0} σ♯(ω) conj (ρ♯(ω))` of the reconstruction formula,
    written `p^m / p` so that it is also correct when `ι` is empty. 
Theorem3.1.6
Statement uses 2
Statement dependency previews
Preview
Definition 3.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

Reconstruction formula over a finite field (Theorem 3.2). For \rho of vanishing mean, S[R[f;\rho]]=(\!(\sigma,\rho)\!)f. Without that hypothesis the master identity computes what is left over: S[R[f;\rho]]=(\!(\sigma,\rho)\!)f+|\mathbb F_p|^{m-1}\sigma^\sharp(0)\overline{\rho^\sharp(0)}\sum_yf(y). Subtracting its mean makes any \rho usable and leaves the scalar unchanged.

Lean code for Theorem3.1.63 theorems
  • 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. 
  • complete
    theorem LeanRidgelet.fs_finiteField_reconstruction.{u_1} {p : } [NeZero p]
      {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Fact (Nat.Prime p)]
      (σ ρ : ZMod p  ) (f : (ι  ZMod p)  ) ( :  b, ρ b = 0) :
      LeanRidgelet.finiteFieldSynthesis σ
          (LeanRidgelet.finiteFieldRidgelet ρ f) =
        fun x  LeanRidgelet.finiteFieldPairing p ι σ ρ * f x
    theorem LeanRidgelet.fs_finiteField_reconstruction.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      [Fact (Nat.Prime p)] (σ ρ : ZMod p  )
      (f : (ι  ZMod p)  )
      ( :  b, ρ b = 0) :
      LeanRidgelet.finiteFieldSynthesis σ
          (LeanRidgelet.finiteFieldRidgelet ρ
            f) =
        fun x 
        LeanRidgelet.finiteFieldPairing p ι σ
            ρ *
          f x
    **The reconstruction formula over a finite field** (Theorem 3.2). A ridgelet function of
    vanishing mean kills the `ω = 0` defect, and the network reproduces the target exactly up to the
    scalar `⦅σ,ρ⦆`. 
  • complete
    theorem LeanRidgelet.fs_finiteField_reconstruction_meanZeroPart.{u_1} {p : }
      [NeZero p] {ι : Type u_1} [Fintype ι] [DecidableEq ι]
      [Fact (Nat.Prime p)] (σ ρ : ZMod p  ) (f : (ι  ZMod p)  ) :
      LeanRidgelet.finiteFieldSynthesis σ
          (LeanRidgelet.finiteFieldRidgelet (LeanRidgelet.meanZeroPart p ρ)
            f) =
        fun x  LeanRidgelet.finiteFieldPairing p ι σ ρ * f x
    theorem LeanRidgelet.fs_finiteField_reconstruction_meanZeroPart.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      [Fact (Nat.Prime p)] (σ ρ : ZMod p  )
      (f : (ι  ZMod p)  ) :
      LeanRidgelet.finiteFieldSynthesis σ
          (LeanRidgelet.finiteFieldRidgelet
            (LeanRidgelet.meanZeroPart p ρ)
            f) =
        fun x 
        LeanRidgelet.finiteFieldPairing p ι σ
            ρ *
          f x
    **Every ridgelet function is usable after normalization.** Running the reconstruction formula
    with the mean-zero part of an arbitrary `ρ` reproduces `f` up to the same scalar `⦅σ,ρ⦆`, so the
    vanishing-mean hypothesis is a normalization rather than a restriction. 
Theorem3.1.7
uses 1used by 1L∃∀N

The three steps over a finite field. Step 1, the Fourier expression S[\gamma](x)=p^{-1}\sum_{a,\omega}\gamma^\sharp(a,\omega)\sigma^\sharp(\omega)\mathrm e(\omega\,a\cdot x), from the convolution theorem in the bias. Step 2, the change of variables \xi=\omega a, valid for \omega\neq0 because \mathbb F_p is a field — this is the only place primality is used. Step 3, the separation-of-variables form \gamma^\sharp(a,\omega)=\widehat f(\omega a)\overline{\rho^\sharp(\omega)} of the ridgelet transform, obtained by reindexing the bias.

Lean code for Theorem3.1.73 theorems
  • complete
    theorem LeanRidgelet.fs_finiteField_fourierExpression.{u_1} {p : } [NeZero p]
      {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : ZMod p  )
      (γ : LeanRidgelet.FiniteFieldParameter p ι  ) (x : ι  ZMod p) :
      LeanRidgelet.finiteFieldSynthesis σ γ x =
        (↑p)⁻¹ *
           a,
             ω,
              ZMod.dft (fun b  γ (a, b)) ω * ZMod.dft σ ω *
                ZMod.stdAddChar (ω * a ⬝ᵥ x)
    theorem LeanRidgelet.fs_finiteField_fourierExpression.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      (σ : ZMod p  )
      (γ :
        LeanRidgelet.FiniteFieldParameter p
            ι 
          )
      (x : ι  ZMod p) :
      LeanRidgelet.finiteFieldSynthesis σ γ
          x =
        (↑p)⁻¹ *
           a,
             ω,
              ZMod.dft (fun b  γ (a, b)) ω *
                  ZMod.dft σ ω *
                ZMod.stdAddChar (ω * a ⬝ᵥ x)
    **Step 1**: the Fourier expression of the network. Convolving in the bias turns `S[γ](x)`
    into `p⁻¹ ∑_{a,ω} γ♯(a,ω) σ♯(ω) e(ω (a ⬝ x))`.
    
    The article writes the activation itself where its spectrum is meant; the convolution theorem
    produces `σ♯`. 
  • complete
    theorem LeanRidgelet.fs_finiteField_changeOfVariables.{u_1} {p : } [NeZero p]
      {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Fact (Nat.Prime p)]
      {ω : ZMod p} ( : ω  0) (F : (ι  ZMod p)  ) :
       a, F (ω  a) =  ξ, F ξ
    theorem LeanRidgelet.fs_finiteField_changeOfVariables.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      [Fact (Nat.Prime p)] {ω : ZMod p}
      ( : ω  0) (F : (ι  ZMod p)  ) :
       a, F (ω  a) =  ξ, F ξ
    **Step 2**: the change of variables `ξ = ω a`. For `ω ≠ 0` the map `a ↦ ω • a` permutes the
    weight space, because `𝔽_p` is a field. This is the only place primality is used. 
  • complete
    theorem LeanRidgelet.fs_dft_finiteFieldRidgelet.{u_1} {p : } [NeZero p]
      {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ZMod p  )
      (f : (ι  ZMod p)  ) (a : ι  ZMod p) (ω : ZMod p) :
      ZMod.dft (fun b  LeanRidgelet.finiteFieldRidgelet ρ f (a, b)) ω =
        ZMod.piDFT f (ω  a) * (starRingEnd ) (ZMod.dft ρ ω)
    theorem LeanRidgelet.fs_dft_finiteFieldRidgelet.{u_1}
      {p : } [NeZero p] {ι : Type u_1}
      [Fintype ι] [DecidableEq ι]
      (ρ : ZMod p  ) (f : (ι  ZMod p)  )
      (a : ι  ZMod p) (ω : ZMod p) :
      ZMod.dft
          (fun b 
            LeanRidgelet.finiteFieldRidgelet ρ
              f (a, b))
          ω =
        ZMod.piDFT f (ω  a) *
          (starRingEnd ) (ZMod.dft ρ ω)
    **Step 3**: the ridgelet transform is already in separation-of-variables form. Its bias
    spectrum factors as a principal part carrying the target function and an auxiliary part carrying
    the ridgelet function, `γ♯(a, ω) = f̂(ω a) conj (ρ♯(ω))`.
    
    Reindexing the bias by `c = a ⬝ x - b` is what produces the factorization. 

Two deviations from the article are recorded here. The constant carries |\mathbb F_p|^{m-1}, as in the article's own proof, rather than its reciprocal as in the article's statement. And the frequency \omega=0 has to be excluded: the change of variables a\mapsto\omega a is a bijection of \mathbb F_p^m only for \omega\neq0, and over a finite field the excluded frequency is an atom rather than a null set, so it contributes a rank-one defect |\mathbb F_p|^{m-1}\sigma^\sharp(0)\overline{\rho^\sharp(0)}\sum_yf(y). Requiring \rho to have vanishing mean kills it, which is the discrete counterpart of the admissibility condition of the continuous theory and the usual vanishing-moment convention for a wavelet. Any \rho can be used after subtracting its mean, which changes neither the constant nor the conclusion.

Section 4: group convolutional networks on a Hilbert space

Definition3.1.8
uses 0used by 1L∃∀N

Generalized group convolution and the group CNN. For a representation T:G\to GL(\mathcal H), the convolution (a*x)(g)=\langle T_{g^{-1}}[x],a\rangle_{\mathcal H}, the network S[\gamma](x)(g)=\int\gamma(a,b)\sigma((a*x)(g)-b), with the filter a ranging over the span of an orthonormal m-frame, and the ridgelet transform R[f;\rho](a,b)=\int_{\mathcal H_m}f(x)(e)\overline{\rho(\langle a,x\rangle-b)}. The filter and the domain of the ridgelet integral are parametrized by their coordinates in the frame, which is what the article means by the Lebesgue measure on \mathcal H_m induced from \mathbb R^m.

Lean code for Definition3.1.87 definitions
  • complete
    def LeanRidgelet.frameCoord.{u_1} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] (fr : Fin m  H)
      (x : H) : LeanRidgelet.InputSpace m
    def LeanRidgelet.frameCoord.{u_1} {m : }
      {H : Type u_1} [NormedAddCommGroup H]
      [InnerProductSpace  H] (fr : Fin m  H)
      (x : H) : LeanRidgelet.InputSpace m
    Implementation after :=
    :=
      WithLp.toLp 2 fun i => inner ℝ (fr i) x
    The coordinates of `x` in the frame `fr`, that is `⟪fr i, x⟫` for each `i`. 
  • complete
    def LeanRidgelet.frameVector.{u_1} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] (fr : Fin m  H)
      (c : LeanRidgelet.InputSpace m) : H
    def LeanRidgelet.frameVector.{u_1} {m : }
      {H : Type u_1} [NormedAddCommGroup H]
      [InnerProductSpace  H] (fr : Fin m  H)
      (c : LeanRidgelet.InputSpace m) : H
    Implementation after :=
    := ∑ i, WithLp.ofLp c i • fr i
    The vector of `ℋ` with coordinates `c` in the frame `fr`. Its image is the span of the
    frame, the `m`-dimensional subspace `ℋ_m` the article restricts the convolution filter to. 
  • complete
    def LeanRidgelet.frameProjection.{u_1} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] (fr : Fin m  H)
      (x : H) : H
    def LeanRidgelet.frameProjection.{u_1} {m : }
      {H : Type u_1} [NormedAddCommGroup H]
      [InnerProductSpace  H] (fr : Fin m  H)
      (x : H) : H
    Implementation after :=
    := frameVector fr (frameCoord fr x)
    The orthogonal projection onto the span of the frame, in the form the reconstruction formula
    produces it. 
  • complete
    def LeanRidgelet.groupConvolution.{u_1, u_2} {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] {G : Type u_2}
      [Group G] (T : G  H  H) (a x : H) (g : G) : 
    def LeanRidgelet.groupConvolution.{u_1, u_2}
      {H : Type u_1} [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      [Group G] (T : G  H  H) (a x : H)
      (g : G) : 
    Implementation after :=
    := inner ℝ a (T g⁻¹ x)
    The generalized `(G,T)`-convolution `(a * x)(g) = ⟪T_{g⁻¹}[x], a⟫`. 
  • complete
    def LeanRidgelet.groupConvSynthesis.{u_1, u_2} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] {G : Type u_2}
      [Group G] (fr : Fin m  H) (T : G  H  H) (σ :   )
      (γ : LeanRidgelet.RidgeletParameterSpace m  ) (x : H) (g : G) : 
    def LeanRidgelet.groupConvSynthesis.{u_1, u_2}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      [Group G] (fr : Fin m  H)
      (T : G  H  H) (σ :   )
      (γ :
        LeanRidgelet.RidgeletParameterSpace
            m 
          )
      (x : H) (g : G) : 
    Implementation after :=
    :=
      ∫ p : RidgeletParameterSpace m, γ p * σ (groupConvolution T (frameVector fr p.1) x g - p.2)
    The group convolutional network. The filter ranges over the span of the frame, parametrized by
    its coordinates, which is what the article means by the Lebesgue measure on `ℋ_m` induced from
    `ℝ^m`. 
  • complete
    def LeanRidgelet.groupConvRidgelet.{u_1, u_2} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] {G : Type u_2}
      [Group G] (fr : Fin m  H) (ρ :   ) (f : H  G  )
      (p : LeanRidgelet.RidgeletParameterSpace m) : 
    def LeanRidgelet.groupConvRidgelet.{u_1, u_2}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      [Group G] (fr : Fin m  H) (ρ :   )
      (f : H  G  )
      (p :
        LeanRidgelet.RidgeletParameterSpace
          m) :
      
    Implementation after :=
    :=
      ∫ y : InputSpace m, f (frameVector fr y) 1 *
        conj (ρ (inner ℝ (frameVector fr p.1) (frameVector fr y) - p.2))
    The ridgelet transform of the article: the filter is paired with the input by the plain scalar
    product, not by the convolution, because both the target and the network are equivariant. 
  • complete
    def LeanRidgelet.IsGroupEquivariant.{u_1, u_2} {H : Type u_1} {G : Type u_2}
      [Group G] (T : G  H  H) (f : H  G  ) : Prop
    def LeanRidgelet.IsGroupEquivariant.{u_1, u_2}
      {H : Type u_1} {G : Type u_2} [Group G]
      (T : G  H  H) (f : H  G  ) : Prop
    Implementation after :=
    :=
      ∀ (x : H) (g h : G), f (T g x) h = f x (g⁻¹ * h)
    `(G,T)`-equivariance of a map `ℋ → ℂ^G`. 
Theorem3.1.9
Statement uses 2
Statement dependency previews
Preview
Theorem 3.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Reconstruction formula for the group CNN (Theorem 4.2). The case reduces exactly to the Euclidean one: pairing a filter of \mathcal H_m against any input is pairing their coordinate vectors, so the network is a Euclidean network read at the coordinate vector of the translated input, and the ridgelet transform is the Euclidean ridgelet transform of the target pulled back to those coordinates. The network is equivariant by construction. The master identity is then S[R[f;\rho]](x)(g)=(\!(\sigma,\rho)\!)f(P_{\mathcal H_m}(T_{g^{-1}}[x]))(e) with no hypothesis on f, and equals (\!(\sigma,\rho)\!)f(x)(g) whenever the projection is invisible to f at that point.

Lean code for Theorem3.1.95 theorems
  • complete
    theorem LeanRidgelet.fs_inner_frameVector.{u_1} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] (fr : Fin m  H)
      (c : LeanRidgelet.InputSpace m) (x : H) :
      inner  (LeanRidgelet.frameVector fr c) x =
        inner  c (LeanRidgelet.frameCoord fr x)
    theorem LeanRidgelet.fs_inner_frameVector.{u_1}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] (fr : Fin m  H)
      (c : LeanRidgelet.InputSpace m)
      (x : H) :
      inner  (LeanRidgelet.frameVector fr c)
          x =
        inner  c
          (LeanRidgelet.frameCoord fr x)
    **The identity the whole case rests on.** Pairing a vector of `ℋ_m` against any vector of `ℋ`
    is pairing their coordinate vectors, so the input enters only through its coordinates. Linearity
    of the frame is all this needs; orthonormality is not used. 
  • complete
    theorem LeanRidgelet.fs_groupConvSynthesis_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) (T : G  H  H) (σ :   )
      (γ : LeanRidgelet.RidgeletParameterSpace m  ) (x : H) (g : G) :
      LeanRidgelet.groupConvSynthesis fr T σ γ x g =
        LeanRidgelet.euclideanDualRidgeletTransform m 0 σ γ
          (LeanRidgelet.frameCoord fr (T g⁻¹ x))
    theorem LeanRidgelet.fs_groupConvSynthesis_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)
      (T : G  H  H) (σ :   )
      (γ :
        LeanRidgelet.RidgeletParameterSpace
            m 
          )
      (x : H) (g : G) :
      LeanRidgelet.groupConvSynthesis fr T σ γ
          x g =
        LeanRidgelet.euclideanDualRidgeletTransform
          m 0 σ γ
          (LeanRidgelet.frameCoord fr
            (T g⁻¹ x))
    The network is a Euclidean network read at the coordinate vector of the translated input.
    This is `fs_inner_frameVector` under the integral sign, and it is the whole of the reduction. 
  • complete
    theorem LeanRidgelet.fs_groupConvSynthesis_equivariant.{u_1, u_2} {m : }
      {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace  H]
      {G : Type u_2} [Group G] (fr : Fin m  H) {T : G  H  H}
      (hT :  (a b : G) (y : H), T a (T b y) = T (a * b) y) (σ :   )
      (γ : LeanRidgelet.RidgeletParameterSpace m  ) (x : H) (g h : G) :
      LeanRidgelet.groupConvSynthesis fr T σ γ (T g x) h =
        LeanRidgelet.groupConvSynthesis fr T σ γ x (g⁻¹ * h)
    theorem LeanRidgelet.fs_groupConvSynthesis_equivariant.{u_1,
        u_2}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      [Group G] (fr : Fin m  H)
      {T : G  H  H}
      (hT :
         (a b : G) (y : H),
          T a (T b y) = T (a * b) y)
      (σ :   )
      (γ :
        LeanRidgelet.RidgeletParameterSpace
            m 
          )
      (x : H) (g h : G) :
      LeanRidgelet.groupConvSynthesis fr T σ γ
          (T g x) h =
        LeanRidgelet.groupConvSynthesis fr T σ
          γ x (g⁻¹ * h)
    **The network is equivariant by construction**, as the article observes. 
  • complete
    theorem LeanRidgelet.fs_groupConv_synthesis_ridgelet.{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) {σ ρ :   } {c : }
      (hrec :
         (F : LeanRidgelet.InputSpace m  )
          (y : LeanRidgelet.InputSpace m),
          LeanRidgelet.euclideanDualRidgeletTransform m 0 σ
              (LeanRidgelet.euclideanRidgeletTransform m 0 ρ F) y =
            c * F y)
      (f : H  G  ) (x : H) (g : G) :
      LeanRidgelet.groupConvSynthesis fr T σ
          (LeanRidgelet.groupConvRidgelet fr ρ f) x g =
        c * f (LeanRidgelet.frameProjection fr (T g⁻¹ x)) 1
    theorem LeanRidgelet.fs_groupConv_synthesis_ridgelet.{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)
      {σ ρ :   } {c : }
      (hrec :
         (F : LeanRidgelet.InputSpace m  )
          (y : LeanRidgelet.InputSpace m),
          LeanRidgelet.euclideanDualRidgeletTransform
              m 0 σ
              (LeanRidgelet.euclideanRidgeletTransform
                m 0 ρ F)
              y =
            c * F y)
      (f : H  G  ) (x : H) (g : G) :
      LeanRidgelet.groupConvSynthesis fr T σ
          (LeanRidgelet.groupConvRidgelet fr ρ
            f)
          x g =
        c *
          f
            (LeanRidgelet.frameProjection fr
              (T g⁻¹ x))
            1
    **The master identity.** With no hypothesis on the target beyond a Euclidean reconstruction
    formula for the pulled-back data, the network built from the ridgelet transform reproduces the
    target read at the *projection* of the translated input.
    
    The Euclidean reconstruction formula is a hypothesis rather than a fixed theorem so that any of
    them may be used: the `L¹` reconstruction of `L1.Reconstruction`, or the Fourier slice scheme. 
  • complete
    theorem LeanRidgelet.fs_groupConv_reconstruction.{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} {σ ρ :   } {c : }
      (hrec :
         (F : LeanRidgelet.InputSpace m  )
          (y : LeanRidgelet.InputSpace m),
          LeanRidgelet.euclideanDualRidgeletTransform m 0 σ
              (LeanRidgelet.euclideanRidgeletTransform m 0 ρ F) y =
            c * F y)
      {f : H  G  } (heq : LeanRidgelet.IsGroupEquivariant T f) {x : H}
      {g : G}
      (hcompat :
        f (LeanRidgelet.frameProjection fr (T g⁻¹ x)) 1 = f (T g⁻¹ x) 1) :
      LeanRidgelet.groupConvSynthesis fr T σ
          (LeanRidgelet.groupConvRidgelet fr ρ f) x g =
        c * f x g
    theorem LeanRidgelet.fs_groupConv_reconstruction.{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}
      {σ ρ :   } {c : }
      (hrec :
         (F : LeanRidgelet.InputSpace m  )
          (y : LeanRidgelet.InputSpace m),
          LeanRidgelet.euclideanDualRidgeletTransform
              m 0 σ
              (LeanRidgelet.euclideanRidgeletTransform
                m 0 ρ F)
              y =
            c * F y)
      {f : H  G  }
      (heq :
        LeanRidgelet.IsGroupEquivariant T f)
      {x : H} {g : G}
      (hcompat :
        f
            (LeanRidgelet.frameProjection fr
              (T g⁻¹ x))
            1 =
          f (T g⁻¹ x) 1) :
      LeanRidgelet.groupConvSynthesis fr T σ
          (LeanRidgelet.groupConvRidgelet fr ρ
            f)
          x g =
        c * f x g
    **The reconstruction formula for the group convolutional network** (Theorem 4.2), under the
    hypothesis that the projection is invisible to the target at the point in question. Equivariance
    then turns the value at the translated input into the value at `(x, g)`. 

Whichever Euclidean reconstruction formula one has is a hypothesis of the two last declarations rather than a fixed choice, so the case does not commit to one analytic setting.

Theorem3.1.10
uses 1used by 1L∃∀N

The projection is a limit of the architecture, and what delimits the ways around it. The value of the network at (x,g) depends on the input only through the coordinate vector of T_{g^{-1}}[x], for every coefficient function; so two inputs with the same coordinates are indistinguishable to every network of this form, and no choice of coefficient function reproduces a target that separates them. The projection in the master identity is therefore not an artifact of the proof.

Lean code for Theorem3.1.105 theorems
  • complete
    theorem LeanRidgelet.fs_groupConvSynthesis_congr_frameCoord.{u_1, u_2} {m : }
      {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace  H]
      {G : Type u_2} [Group G] (fr : Fin m  H) (T : G  H  H) (σ :   )
      (γ : LeanRidgelet.RidgeletParameterSpace m  ) {x x' : H} {g : G}
      (h :
        LeanRidgelet.frameCoord fr (T g⁻¹ x) =
          LeanRidgelet.frameCoord fr (T g⁻¹ x')) :
      LeanRidgelet.groupConvSynthesis fr T σ γ x g =
        LeanRidgelet.groupConvSynthesis fr T σ γ x' g
    theorem LeanRidgelet.fs_groupConvSynthesis_congr_frameCoord.{u_1,
        u_2}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      [Group G] (fr : Fin m  H)
      (T : G  H  H) (σ :   )
      (γ :
        LeanRidgelet.RidgeletParameterSpace
            m 
          )
      {x x' : H} {g : G}
      (h :
        LeanRidgelet.frameCoord fr (T g⁻¹ x) =
          LeanRidgelet.frameCoord fr
            (T g⁻¹ x')) :
      LeanRidgelet.groupConvSynthesis fr T σ γ
          x g =
        LeanRidgelet.groupConvSynthesis fr T σ
          γ x' g
    **The projection is a limit of the architecture, not of the proof.** The value of the network
    depends on the input only through the coordinate vector of the translated input, for every
    coefficient function. Two inputs with the same coordinates are indistinguishable to every network
    of this form, so no choice of coefficient function can reproduce a target that separates them. 
  • complete
    theorem LeanRidgelet.fs_frameProjection_eq_self_of_mem.{u_1} {m : }
      {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace  H]
      {fr : Fin m  H} (hfr : Orthonormal  fr) {x : H}
      (hx : x  Submodule.span  (Set.range fr)) :
      LeanRidgelet.frameProjection fr x = x
    theorem LeanRidgelet.fs_frameProjection_eq_self_of_mem.{u_1}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] {fr : Fin m  H}
      (hfr : Orthonormal  fr) {x : H}
      (hx :
        x  Submodule.span  (Set.range fr)) :
      LeanRidgelet.frameProjection fr x = x
    A vector of the span of the frame is fixed by the projection. 
  • complete
    theorem LeanRidgelet.fs_mem_of_invariant.{u_1, u_2} {m : } {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] {G : Type u_2}
      [Group G] {fr : Fin m  H} {T : G  H  H}
      (hinv :
         (g : G),
           y  Submodule.span  (Set.range fr),
            T g y  Submodule.span  (Set.range fr))
      {x : H} (hx : x  Submodule.span  (Set.range fr)) (g : G) :
      T g⁻¹ x  Submodule.span  (Set.range fr)
    theorem LeanRidgelet.fs_mem_of_invariant.{u_1,
        u_2}
      {m : } {H : Type u_1}
      [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      [Group G] {fr : Fin m  H}
      {T : G  H  H}
      (hinv :
         (g : G),
          
            y 
              Submodule.span  (Set.range fr),
            T g y 
              Submodule.span  (Set.range fr))
      {x : H}
      (hx :
        x  Submodule.span  (Set.range fr))
      (g : G) :
      T g⁻¹ x 
        Submodule.span  (Set.range fr)
    Second sufficient condition: the span of the frame is `T`-invariant and the input lies in it.
    This is the natural one, but it needs a finite-dimensional invariant subspace to exist; see
    `fs_span_orbit_le_of_invariant`. 
  • complete
    theorem LeanRidgelet.fs_span_orbit_le_of_invariant.{u_1, u_2} {H : Type u_1}
      [NormedAddCommGroup H] [InnerProductSpace  H] {G : Type u_2}
      {T : G  H  H} {W : Submodule  H}
      (hinv :  (g : G),  y  W, T g y  W) {x : H} (hx : x  W) :
      Submodule.span  (Set.range fun g  T g x)  W
    theorem LeanRidgelet.fs_span_orbit_le_of_invariant.{u_1,
        u_2}
      {H : Type u_1} [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      {T : G  H  H} {W : Submodule  H}
      (hinv :  (g : G),  y  W, T g y  W)
      {x : H} (hx : x  W) :
      Submodule.span 
          (Set.range fun g  T g x) 
        W
    What delimits the invariance condition: the orbit of a vector of an invariant subspace stays
    inside it, so its span is no larger. A vector whose orbit spans an infinite-dimensional space
    therefore lies in no finite-dimensional invariant subspace, and for a representation with no
    finite-dimensional subrepresentation the condition is vacuous. 
  • complete
    theorem LeanRidgelet.fs_not_finiteDimensional_of_orthonormal_orbit.{u_1, u_2}
      {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace  H]
      {G : Type u_2} {T : G  H  H} {W : Submodule  H}
      (hinv :  (g : G),  y  W, T g y  W) {x : H} (hx : x  W)
      {v :   H} (hv : Orthonormal  v)
      (hmem :  (n : ), v n  Set.range fun g  T g x) :
      ¬FiniteDimensional  W
    theorem LeanRidgelet.fs_not_finiteDimensional_of_orthonormal_orbit.{u_1,
        u_2}
      {H : Type u_1} [NormedAddCommGroup H]
      [InnerProductSpace  H] {G : Type u_2}
      {T : G  H  H} {W : Submodule  H}
      (hinv :  (g : G),  y  W, T g y  W)
      {x : H} (hx : x  W) {v :   H}
      (hv : Orthonormal  v)
      (hmem :
         (n : ),
          v n  Set.range fun g  T g x) :
      ¬FiniteDimensional  W
    **The invariance condition is vacuous for a representation whose orbits are large.** If the
    orbit of `x` contains an infinite orthonormal family, then no finite-dimensional invariant
    subspace contains `x`, so the second sufficient condition above is unavailable and only the
    pointwise hypothesis or a band-limited target remains.
    
    This is what separates the representations the article's construction covers from the ones it does
    not: for a finite group, or any representation with precompact image, finite-dimensional invariant
    subspaces are plentiful; for the translation representation on `L²(ℝ)`, the integer translates of
    an indicator function are orthonormal, so there are none. 

Sufficient conditions for the compatibility hypothesis: the translated input already lies in the span of the frame; or that span is T-invariant and the input lies in it; or f factors through the projection. The second is the natural one and comes with a caveat the article does not raise — it needs a finite-dimensional invariant subspace. The orbit of a vector of an invariant subspace stays inside it, so a vector whose translates span an infinite-dimensional space lies in no finite-dimensional invariant subspace. Such subspaces are plentiful when the closure of the image of T is compact, as for a finite group, for \mathbb T acting on Fourier modes, or for DeepSets; for a representation whose orbit of some vector contains an infinite orthonormal family — the integer translates of an indicator function under translation on L^2(\mathbb R), say — no finite-dimensional invariant subspace contains that vector at all, and only the pointwise hypothesis or a band-limited f remains.

The projection is a deviation from the article, which states the conclusion as (\!(\sigma,\rho)\!)f. Only an inversion formula on \mathcal H_m is available, so what the derivation returns is the target function read at P_{\mathcal H_m}(T_{g^{-1}}[x]). This is not an artifact of the proof: the network sees x only through \langle T_{g^{-1}}[x],a\rangle with a\in\mathcal H_m, hence only through that projection, so no coefficient function can do better. Sufficient conditions for the two to agree are that T_{g^{-1}}[x]\in\mathcal H_m, that \mathcal H_m be T-invariant, or that f factor through the projection. The second is the natural one, but it needs a finite-dimensional invariant subspace, which exists in abundance when the closure of the image of T is compact and only trivially when T has no finite-dimensional subrepresentation.

Section 5: networks on a noncompact symmetric space

Definition3.1.11
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 3.1.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

The network on G/K, and the geometry it needs. S[\gamma](x)=\int\gamma(a,u,b)\sigma(a\langle x,u\rangle-b)e^{\varrho\langle x,u\rangle} and R[f;\rho](a,u,b)=\int_X c[f](x)\overline{\rho(a\langle x,u\rangle-b)}e^{\varrho\langle x,u\rangle}\,\mathrm dx, with \langle x,u\rangle\in\mathfrak a\cong\mathbb R^r the vector-valued composite distance from the origin to the horosphere through x with normal u\in\partial X.

Lean code for Definition3.1.115 definitions
  • complete
    def LeanRidgelet.horosphericalWeight.{u_1, u_2} {r : } {X : Type u_1}
      {U : Type u_2} (ϱ : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r) (x : X) (u : U) : 
    def LeanRidgelet.horosphericalWeight.{u_1,
        u_2}
      {r : } {X : Type u_1} {U : Type u_2}
      (ϱ : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r)
      (x : X) (u : U) : 
    Implementation after :=
    :=
      Complex.exp ((inner ℝ ϱ (cd x u) : ℝ) : ℂ)
    The weight `e^{ϱ⟪x,u⟫}` carried by the layer, where `⟪x,u⟫ ∈ 𝔞 ≅ ℝ^r` is the composite
    distance and `ϱ ∈ 𝔞*` the constant vector of the Helgason--Fourier transform. 
  • complete
    def LeanRidgelet.harishChandraDensity {r : } (W : )
      (cfun : LeanRidgelet.InputSpace r  )
      (lam : LeanRidgelet.InputSpace r) : 
    def LeanRidgelet.harishChandraDensity {r : }
      (W : )
      (cfun : LeanRidgelet.InputSpace r  )
      (lam : LeanRidgelet.InputSpace r) : 
    Implementation after :=
    :=
      (W * ‖cfun lam‖ ^ 2)⁻¹
    The density `|W|⁻¹|c(λ)|⁻²` of the Helgason--Fourier inversion formula, built from the order
    of the Weyl group and the Harish-Chandra `c`-function. Both enter as data. 
  • complete
    def LeanRidgelet.symmetricSynthesis.{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) (σ :   )
      (γ : LeanRidgelet.InputSpace r  U    ) (x : X) : 
    def LeanRidgelet.symmetricSynthesis.{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)
      (σ :   )
      (γ :
        LeanRidgelet.InputSpace r  U    )
      (x : X) : 
    Implementation after :=
    :=
      ∫ a : InputSpace r, ∫ u : U, ∫ b : ℝ,
        γ a u b * σ (inner ℝ a (cd x u) - b) * horosphericalWeight ϱ cd x u ∂volume ∂ν
    The network on a noncompact symmetric space,
    `S[γ](x) = ∫ γ(a,u,b) σ(a ⬝ ⟪x,u⟫ - b) e^{ϱ⟪x,u⟫} da du db`.
    
    Turning this into its Fourier expression is Step 1 of the method, which is one-dimensional — the
    convolution theorem in the bias — and is not part of this file; see the module docstring of
    `FS.Scheme`. 
  • complete
    def LeanRidgelet.symmetricRidgelet.{u_1, u_2} {r : } {X : Type u_1}
      {U : Type u_2} [MeasurableSpace X] (μX : MeasureTheory.Measure X)
      (ϱ : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r) (ρ :   ) (cf : X  )
      (a : LeanRidgelet.InputSpace r) (u : U) (b : ) : 
    def LeanRidgelet.symmetricRidgelet.{u_1, u_2}
      {r : } {X : Type u_1} {U : Type u_2}
      [MeasurableSpace X]
      (μX : MeasureTheory.Measure X)
      (ϱ : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r)
      (ρ :   ) (cf : X  )
      (a : LeanRidgelet.InputSpace r) (u : U)
      (b : ) : 
    Implementation after :=
    :=
      ∫ x : X, cf x * conj (ρ (inner ℝ a (cd x u) - b)) * horosphericalWeight ϱ cd x u ∂μX
    The ridgelet transform on a noncompact symmetric space,
    `R[f;ρ](a,u,b) = ∫_X c[f](x) conj (ρ (a ⬝ ⟪x,u⟫ - b)) e^{ϱ⟪x,u⟫} dx`,
    against the multiplier `c[f]` supplied as data. 
  • complete
    def LeanRidgelet.symmetricFourierExpression.{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) ( :   )
      (Γ : LeanRidgelet.InputSpace r  U    ) (x : X) : 
    def LeanRidgelet.symmetricFourierExpression.{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)
      ( :   )
      (Γ :
        LeanRidgelet.InputSpace r  U    )
      (x : X) : 
    Implementation after :=
    :=
      fourierExpressionSynthesis (volume : Measure (InputSpace r)) ν Fσ Γ cd
        (horosphericalWeight ϱ cd) x
    The network in Fourier expression form on a symmetric space: the specialization of
    `fourierExpressionSynthesis` to the composite distance and the horospherical weight. 

Mathlib has no Iwasawa decomposition, no spherical functions and no Harish-Chandra c-function, and none is needed to state this. The geometry enters as data: the composite distance, the constant \varrho, the density |W|^{-1}|c(\lambda)|^{-2}, and the Helgason--Fourier transform of the target.

Theorem3.1.12
Statement uses 2
Statement dependency previews
Preview
Definition 3.1.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Definition 3.1.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Helgason--Fourier inversion (Section 5). f(x)=|W|^{-1}\int_{\lieA^{*}\times\partial X}\widehat f(\lambda,u)\,e^{(i\lambda+\varrho)\langle x,u\rangle}\,\mathrm d\lambda\,\mathrm du/|c(\lambda)|^{2}. This is a statement, not a theorem: it is a predicate on the geometry, and proving it for a given space is a project of its own.

Lean code for Theorem3.1.123 declarations
  • def SymmetricSpace.HasHelgasonInversion.{u_1, u_2, u_3} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [MeasurableSpace E]
      {X : Type u_2} {B : Type u_3} [MeasurableSpace X] [MeasurableSpace B]
      (μ : MeasureTheory.Measure X) (mua : MeasureTheory.Measure E)
      (nu : MeasureTheory.Measure B) (A : X  B  E) (rho : E) (W : )
      (c : E  ) (f : X  ) : Prop
    def SymmetricSpace.HasHelgasonInversion.{u_1,
        u_2, u_3}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [MeasurableSpace E] {X : Type u_2}
      {B : Type u_3} [MeasurableSpace X]
      [MeasurableSpace B]
      (μ : MeasureTheory.Measure X)
      (mua : MeasureTheory.Measure E)
      (nu : MeasureTheory.Measure B)
      (A : X  B  E) (rho : E) (W : )
      (c : E  ) (f : X  ) : Prop
    Implementation after :=
    :=
      ∀ x : X, helgasonInversionIntegral mua nu A rho (helgasonFourier μ A rho f)
        (plancherelDensity W c) x = f x
    **The Helgason--Fourier inversion formula** for `f`, as a proposition about the geometry:
    the inversion integral of the Helgason--Fourier transform of `f`, against the density
    `(|W| ‖c(λ)‖²)^{-1}`, returns `f`.
    
    This is a `Prop` on data rather than an assumption object: a concrete model instantiates the data
    and then has a definite statement to prove. With the geometry left free it is not even a
    well-posed claim, which is why the constructions of a model have to come first. 
  • theorem SymmetricSpace.hasHelgasonInversion_iff.{u_1, u_2, u_3} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [MeasurableSpace E]
      {X : Type u_2} {B : Type u_3} [MeasurableSpace X] [MeasurableSpace B]
      (μ : MeasureTheory.Measure X) (mua : MeasureTheory.Measure E)
      (nu : MeasureTheory.Measure B) (A : X  B  E) (rho : E) (W : )
      (c : E  ) (f : X  ) :
      SymmetricSpace.HasHelgasonInversion μ mua nu A rho W c f 
         (x : X),
           (lam : E),
               (b : B),
                SymmetricSpace.helgasonFourier μ A rho f lam b *
                    (SymmetricSpace.plancherelDensity W c lam) *
                  SymmetricSpace.horosphericalCharacter rho lam
                    (A x b) nu mua =
            f x
    theorem SymmetricSpace.hasHelgasonInversion_iff.{u_1,
        u_2, u_3}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [MeasurableSpace E] {X : Type u_2}
      {B : Type u_3} [MeasurableSpace X]
      [MeasurableSpace B]
      (μ : MeasureTheory.Measure X)
      (mua : MeasureTheory.Measure E)
      (nu : MeasureTheory.Measure B)
      (A : X  B  E) (rho : E) (W : )
      (c : E  ) (f : X  ) :
      SymmetricSpace.HasHelgasonInversion μ
          mua nu A rho W c f 
         (x : X),
           (lam : E),
               (b : B),
                SymmetricSpace.helgasonFourier
                      μ A rho f lam b *
                    (SymmetricSpace.plancherelDensity
                        W c lam) *
                  SymmetricSpace.horosphericalCharacter
                    rho lam (A x b) nu mua =
            f x
  • theorem SymmetricSpace.hasHelgasonInversion_of_spherical.{u_1, u_2, u_3}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [MeasurableSpace E] {X : Type u_2} {B : Type u_3} [MeasurableSpace X]
      [MeasurableSpace B] (μ : MeasureTheory.Measure X)
      (mua : MeasureTheory.Measure E) (nu : MeasureTheory.Measure B)
      (A : X  B  E) (rho : E) (W : ) (c : E  ) (f : X  )
      (conv : E  X  )
      (hconv :
         (lam : E) (x : X),
           (b : B),
              SymmetricSpace.helgasonFourier μ A rho f lam b *
                SymmetricSpace.horosphericalCharacter rho lam (A x b) nu =
            conv lam x)
      (hsph :
         (x : X),
           (lam : E),
              (SymmetricSpace.plancherelDensity W c lam) *
                conv lam x mua =
            f x) :
      SymmetricSpace.HasHelgasonInversion μ mua nu A rho W c f
    theorem SymmetricSpace.hasHelgasonInversion_of_spherical.{u_1,
        u_2, u_3}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [MeasurableSpace E] {X : Type u_2}
      {B : Type u_3} [MeasurableSpace X]
      [MeasurableSpace B]
      (μ : MeasureTheory.Measure X)
      (mua : MeasureTheory.Measure E)
      (nu : MeasureTheory.Measure B)
      (A : X  B  E) (rho : E) (W : )
      (c : E  ) (f : X  )
      (conv : E  X  )
      (hconv :
         (lam : E) (x : X),
           (b : B),
              SymmetricSpace.helgasonFourier μ
                  A rho f lam b *
                SymmetricSpace.horosphericalCharacter
                  rho lam (A x b) nu =
            conv lam x)
      (hsph :
         (x : X),
           (lam : E),
              (SymmetricSpace.plancherelDensity
                    W c lam) *
                conv lam x mua =
            f x) :
      SymmetricSpace.HasHelgasonInversion μ
        mua nu A rho W c f
    **The reduction of Helgason's proof.** The inversion formula holds as soon as
    
    * `hconv`: the boundary integral `∫_B f̂(λ,b) e^{(iλ+ϱ)(A(x,b))} db` equals a function `conv λ x`
      — in the group setting the convolution `(f × φ_λ)(x)`, by Lemma 1.2 of
      *Geometric Analysis on Symmetric Spaces*, Ch. III §1, which is where the symmetry of the
      spherical function is used; and
    * `hsph`: that function is inverted by the Plancherel density, `∫_{𝔞*} κ(λ) conv λ x dλ = f(x)`
      — Harish-Chandra's inversion formula for the spherical transform.
    
    The proof is then only bookkeeping: the density does not depend on `b`, so it comes out of the
    boundary integral. What the statement buys is the separation of the two inputs, and in particular
    the isolation of the one deep analytic fact. 

FS.Symmetric takes the geometry as data, and with that data free the inversion formula is not a true proposition at all — which is why it was for a time not stated in Lean. The Mathlib-general layer now supplies the vocabulary to state it: the Helgason--Fourier transform, the spherical function and the Plancherel density built from |W| and the c-function. What the statement is worth is that it can now be reduced: the last declaration shows the inversion formula follows from the identification of the boundary integral with the convolution against the spherical function together with Harish-Chandra's inversion formula for the spherical transform, so the deep analytic input is isolated to one hypothesis. The reconstruction formula below takes the inversion formula itself as an explicit hypothesis, which is the whole design of the abstract scheme.

Definition3.1.13
Statement uses 6
Statement dependency previews
Preview
Theorem 3.1.12
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

Continuous horospherical hyperbolic network (Section 5). The Poincaré ball \mathbb B^m with the metric 4(1-|x|^2)^{-2}\sum\mathrm dx_i\otimes\mathrm dx_i, composite distance \langle x,u\rangle=\log\frac{1-|x|^2}{|x-u|^2}, \varrho=(m-1)/2, boundary \mathbb S^{m-1}, |W|=2, and c(\lambda) an explicit ratio of Gamma functions. Rank one, so everything is a closed formula and no Lie theory is needed; this is the first place the inversion formula above could be proved rather than assumed. The model itself is now in Lean — the ball, its boundary, the Poisson kernel, the composite distance, \varrho and the invariant measure — with no Riemannian geometry used, since Mathlib has neither a volume measure nor a Laplace--Beltrami operator to build one from. The Helgason--Fourier transform of the model is there too, and with it the inversion formula as a propositionHyperbolicSpace.HasInversion, a definite claim about a definite space rather than a schema. The Möbius action is there as well, together with the cocycle \langle\varphi_a x,\varphi_a u\rangle=\langle x,u\rangle-\langle a,u\rangle that makes the isometry group act on the transform. The invariance of the volume measure under that action is there too, so the model is complete as a measured space with a group acting on it. On top of it the network, the ridgelet transform and the reconstruction formula of this example are formalized: fs_hyperbolic_reconstruction_of_inversion assumes the Helgason--Fourier inversion formula for \mathbb H^m and nothing else, and that formula is fs_hyperbolicHelgasonInversion, the one remaining target. One by-product settles a design question the development plan had left open: the weight the layer carries is P(x,u)^\varrho, a power of the Poisson kernel, hence a half-density rather than an input-dependent coefficient.

Lean code for Definition3.1.1321 declarations, 1 incomplete
  • def HyperbolicSpace.poincareBall.{u_2} (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E] : Set E
    def HyperbolicSpace.poincareBall.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E] : Set E
    Implementation after :=
    :=
      ball (0 : E) 1
    The Poincaré ball model of real hyperbolic space: the open unit ball of a Euclidean space.
    The dimension of the space is the dimension of `ℍ^m`. 
  • def HyperbolicSpace.idealBoundary.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] : Set E
    def HyperbolicSpace.idealBoundary.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E] : Set E
    Implementation after :=
    :=
      sphere (0 : E) 1
    The ideal boundary `∂ℍ^m = 𝕊^{m-1}`, the unit sphere. 
  • def HyperbolicSpace.poissonKernel.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] (x u : E) : 
    def HyperbolicSpace.poissonKernel.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      (x u : E) : 
    Implementation after :=
    := (1 - ‖x‖ ^ 2) / ‖x - u‖ ^ 2
    The Poisson kernel of the ball, `P(x,u) = (1 - ‖x‖²)/‖x - u‖²`.
    
    Its logarithm is the composite distance and its `ϱ`-th power is the weight `e^{ϱ⟨x,u⟩}` that a
    layer of a network on `ℍ^m` carries. For `m = 2` it is the classical Poisson kernel of the disk;
    for `m > 2` the classical Euclidean one is `(1-‖x‖²)/‖x-u‖^m`, and the two differ because the
    hyperbolic and the Euclidean Laplacians only share their harmonic functions in dimension two. 
  • def HyperbolicSpace.compositeDistance.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] (x u : E) : 
    def HyperbolicSpace.compositeDistance.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      (x u : E) : 
    Implementation after :=
    := Real.log (poissonKernel x u)
    The rank-one vector-valued composite distance `⟨x,u⟩ = log((1 - ‖x‖²)/‖x - u‖²)`, the signed
    distance from the origin to the horosphere through `x` with normal `u`.
    
    The rank of `ℍ^m` is one, so `𝔞 ≅ ℝ` and the "vector-valued" distance is a scalar. 
  • def HyperbolicSpace.rho.{u_2} (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E] : 
    def HyperbolicSpace.rho.{u_2} (E : Type u_2)
      [NormedAddCommGroup E]
      [InnerProductSpace  E] : 
    Implementation after :=
    :=
      ((Module.finrank ℝ E : ℝ) - 1) / 2
    The half-sum of the positive restricted roots of `ℍ^m`, `ϱ = (m-1)/2`, as an element of
    `𝔞* ≅ ℝ`. 
  • def HyperbolicSpace.invariantMeasure.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] : MeasureTheory.Measure E
    def HyperbolicSpace.invariantMeasure.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.Measure E
    Implementation after :=
    :=
      (volume.restrict (poincareBall E)).withDensity fun x => ENNReal.ofReal (volumeDensity x)
    The `G`-invariant measure of `ℍ^m` in the Poincaré ball model. Its invariance under the Möbius
    transformations of the ball is the content of a later file; here it is only defined.
    
    It is a measure on the whole space rather than on the ball as a subtype, concentrated on the ball
    by the restriction. That keeps `ℍ^m` a plain Euclidean space for every downstream construction and
    avoids carrying a subtype through the Helgason--Fourier theory; nothing outside the ball is ever
    seen, since the density is integrated against the restricted measure. 
  • theorem HyperbolicSpace.compositeDistance_origin.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] {u : E} (hu : u = 1) :
      HyperbolicSpace.compositeDistance 0 u = 0
    theorem HyperbolicSpace.compositeDistance_origin.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      {u : E} (hu : u = 1) :
      HyperbolicSpace.compositeDistance 0 u =
        0
    The origin of the ball lies on every horosphere through it: the composite distance from the
    origin to a boundary point vanishes. This is the normalization that makes `e^{(-iλ+ϱ)⟨x,u⟩}` the
    analogue of a plane wave based at the origin. 
  • theorem HyperbolicSpace.exp_compositeDistance.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] {x u : E} (hx : x < 1) (hu : u = 1) :
      Real.exp (HyperbolicSpace.compositeDistance x u) =
        HyperbolicSpace.poissonKernel x u
    theorem HyperbolicSpace.exp_compositeDistance.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      {x u : E} (hx : x < 1)
      (hu : u = 1) :
      Real.exp
          (HyperbolicSpace.compositeDistance x
            u) =
        HyperbolicSpace.poissonKernel x u
    Inside the ball the Poisson kernel is positive, so it is recovered from the composite
    distance. 
  • def HyperbolicSpace.boundaryMeasure.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.Measure (Metric.sphere 0 1)
    def HyperbolicSpace.boundaryMeasure.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] :
      MeasureTheory.Measure
        (Metric.sphere 0 1)
    Implementation after :=
    :=
      ((volume : Measure E).toSphere univ)⁻¹ • (volume : Measure E).toSphere
    The uniform probability measure on the ideal boundary `∂ℍ^m = 𝕊^{m-1}`: Mathlib's surface
    measure divided by its total mass.
    
    Normalizing here rather than carrying the total mass through the theory is what makes the boundary
    integral of the inversion formula an average, which is the form the Helgason--Fourier theory uses
    (`∫ db = 1`). 
  • def HyperbolicSpace.helgasonFourier.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (f : E  ) (lam : )
      (u : (Metric.sphere 0 1)) : 
    def HyperbolicSpace.helgasonFourier.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (f : E  ) (lam : )
      (u : (Metric.sphere 0 1)) : 
    Implementation after :=
    :=
      SymmetricSpace.helgasonFourier (invariantMeasure E) boundaryDistance (rho E) f lam u
    **The Helgason--Fourier transform on `ℍ^m`**,
    `f̂(λ,u) = ∫ f(x) e^{(-iλ+ϱ)⟨x,u⟩} dμ(x) = ∫ f(x) P(x,u)^{ϱ-iλ} dμ(x)`,
    with `μ` the invariant measure of the ball and `ϱ = (m-1)/2`. 
  • def HyperbolicSpace.HasInversion.{u_1} {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] [FiniteDimensional  E] [MeasurableSpace E]
      [BorelSpace E] (W : ) (c :   ) (f : E  ) : Prop
    def HyperbolicSpace.HasInversion.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (W : ) (c :   ) (f : E  ) : Prop
    Implementation after :=
    :=
      SymmetricSpace.HasHelgasonInversion (invariantMeasure E) (volume : Measure ℝ)
        (boundaryMeasure E) boundaryDistance (rho E) W c f
    **The Helgason--Fourier inversion formula on real hyperbolic space**, as a proposition:
    
    `f(x) = |W|^{-1} ∫_ℝ ∫_{𝕊^{m-1}} f̂(λ,u) e^{(iλ+ϱ)⟨x,u⟩} |c(λ)|^{-2} du dλ`.
    
    Rank one, so the frequency variable is a real number and `dλ` is Lebesgue measure on `ℝ`. Fixing
    `dλ` to be Lebesgue is deliberate: Helgason's inversion formula is written against a normalization
    of `dλ` that is not Lebesgue measure, and the difference is exactly where the powers of `π` in the
    constant live, so the constant has to be produced by a proof rather than quoted.
    
    This is a statement, not a theorem. Proving it is the next stage; the route is through the Möbius
    action of the ball, the Abel transform, and Harish-Chandra's inversion of the spherical transform,
    and `SymmetricSpace.hasHelgasonInversion_of_spherical` is where those inputs meet. 
  • def HyperbolicSpace.mobius.{u_1} {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] (a x : E) : E
    def HyperbolicSpace.mobius.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] (a x : E) : E
    Implementation after :=
    := (mobiusBracketSq x a)⁻¹ • mobiusNum a x
    **The Möbius transformation of the unit ball** carrying `a` to the origin,
    `φ_a(x) = ((1-‖a‖²)(x-a) - ‖x-a‖² a)/[x,a]²`.
    
    In one dimension this is `x ↦ (x-a)/(1-ax)`. It sends `a` to `0` and `0` to `-a`; the involution
    that swaps them is its negative. 
  • theorem HyperbolicSpace.compositeDistance_mobius.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] {x u a : E}
      (hx : x < 1) (hu : u = 1) (ha : a < 1) :
      HyperbolicSpace.compositeDistance (HyperbolicSpace.mobius a x)
          (HyperbolicSpace.mobius a u) =
        HyperbolicSpace.compositeDistance x u -
          HyperbolicSpace.compositeDistance a u
    theorem HyperbolicSpace.compositeDistance_mobius.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] {x u a : E}
      (hx : x < 1) (hu : u = 1)
      (ha : a < 1) :
      HyperbolicSpace.compositeDistance
          (HyperbolicSpace.mobius a x)
          (HyperbolicSpace.mobius a u) =
        HyperbolicSpace.compositeDistance x
            u -
          HyperbolicSpace.compositeDistance a
            u
    **The cocycle of the composite distance**, `⟨φ_a x, φ_a u⟩ = ⟨x,u⟩ - ⟨a,u⟩`.
    
    This is the identity the abstract Helgason--Fourier layer asks of a model: it is what turns the
    action of the isometry group on `ℍ^m` into a multiplier on the Helgason--Fourier kernel, since the
    kernel is the exponential of a linear functional of the composite distance and so is multiplicative
    in it. 
  • theorem HyperbolicSpace.lintegral_invariantMeasure_comp_mobius.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E] [MeasurableSpace E]
      [BorelSpace E] {a : E} (ha : a < 1) {g : E  ENNReal}
      (hg : Measurable g) :
      ∫⁻ (x : E),
          g
            (HyperbolicSpace.mobius a
              x) HyperbolicSpace.invariantMeasure E =
        ∫⁻ (x : E), g x HyperbolicSpace.invariantMeasure E
    theorem HyperbolicSpace.lintegral_invariantMeasure_comp_mobius.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] [Nontrivial E]
      [MeasurableSpace E] [BorelSpace E]
      {a : E} (ha : a < 1) {g : E  ENNReal}
      (hg : Measurable g) :
      ∫⁻ (x : E),
          g
            (HyperbolicSpace.mobius a
              x) HyperbolicSpace.invariantMeasure
            E =
        ∫⁻ (x : E),
          g
            x HyperbolicSpace.invariantMeasure
            E
    **The invariant measure of `ℍ^m` is Möbius invariant.**
    
    The change of variables along `φ_a` needs three inputs and no more: differentiability, injectivity
    on the ball, and that the image of the ball is the ball. The density then cancels the Jacobian
    pointwise, and what is left is the same integral. 
  • complete
    def LeanRidgelet.hyperbolicWeight.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] (x : E)
      (u : (Metric.sphere 0 1)) : 
    def LeanRidgelet.hyperbolicWeight.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E] (x : E)
      (u : (Metric.sphere 0 1)) : 
    Implementation after :=
    :=
      SymmetricSpace.horosphericalCharacter (HyperbolicSpace.rho E) 0
        (HyperbolicSpace.boundaryDistance x u)
    The weight `e^{ϱ⟨x,u⟩}` that a layer of the continuous horospherical hyperbolic network
    carries: the horospherical character of `ℍ^m` at zero frequency. 
  • complete
    theorem LeanRidgelet.fs_hyperbolicWeight_eq_poissonKernel_rpow.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E] {x : E}
      {u : (Metric.sphere 0 1)} (hx : x < 1) :
      LeanRidgelet.hyperbolicWeight E x u =
        (HyperbolicSpace.poissonKernel x u ^ HyperbolicSpace.rho E)
    theorem LeanRidgelet.fs_hyperbolicWeight_eq_poissonKernel_rpow.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] {x : E}
      {u : (Metric.sphere 0 1)}
      (hx : x < 1) :
      LeanRidgelet.hyperbolicWeight E x u =
        (HyperbolicSpace.poissonKernel x u ^
            HyperbolicSpace.rho E)
    **The weight is a power of the Poisson kernel**, `e^{ϱ⟨x,u⟩} = P(x,u)^ϱ` with
    `ϱ = (m-1)/2`.
    
    So the layer does not carry an input-dependent coefficient but the half-density that makes the
    Helgason--Fourier transform an isometry; for `m = 2` it is the square root of the Euclidean Poisson
    kernel. This settles in the affirmative the reading of the weight raised as an open design question
    in the development plan. 
  • complete
    def LeanRidgelet.hyperbolicSynthesis.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (σ :   )
      (γ :   (Metric.sphere 0 1)    ) (x : E) : 
    def LeanRidgelet.hyperbolicSynthesis.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (σ :   )
      (γ :   (Metric.sphere 0 1)    )
      (x : E) : 
    Implementation after :=
    :=
      sliceSynthesis (volume : Measure ℝ) (HyperbolicSpace.boundaryMeasure E) σ γ
        HyperbolicSpace.boundaryDistance (hyperbolicWeight E) x
    **The continuous horospherical hyperbolic network** (Section 5),
    `S[γ](x) = ∫_{ℝ × ∂𝔹^m × ℝ} γ(a,u,b) σ(a⟨x,u⟩ - b) e^{ϱ⟨x,u⟩} da du db`.
    
    The scale variable is a real number because `ℍ^m` has rank one, whatever its dimension. 
  • complete
    def LeanRidgelet.hyperbolicRidgelet.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (ρ :   ) (cf : E  ) (a : )
      (u : (Metric.sphere 0 1)) (b : ) : 
    def LeanRidgelet.hyperbolicRidgelet.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (ρ :   ) (cf : E  ) (a : )
      (u : (Metric.sphere 0 1)) (b : ) : 
    Implementation after :=
    :=
      ∫ x : E, cf x * conj (ρ (inner ℝ a (HyperbolicSpace.boundaryDistance x u) - b)) *
        hyperbolicWeight E x u ∂(HyperbolicSpace.invariantMeasure E)
    The ridgelet transform on the Poincaré ball,
    `R[f;ρ](a,u,b) = ∫ c[f](x) conj (ρ(a⟨x,u⟩ - b)) e^{ϱ⟨x,u⟩} dμ(x)`,
    against the multiplier `c[f]` the article inserts to cancel one power of the Harish-Chandra
    density. 
  • complete
    def LeanRidgelet.hyperbolicFourierExpression.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] ( :   )
      (Γ :   (Metric.sphere 0 1)    ) (x : E) : 
    def LeanRidgelet.hyperbolicFourierExpression.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      ( :   )
      (Γ :   (Metric.sphere 0 1)    )
      (x : E) : 
    Implementation after :=
    :=
      fourierExpressionSynthesis (volume : Measure ℝ) (HyperbolicSpace.boundaryMeasure E) Fσ Γ
        HyperbolicSpace.boundaryDistance (hyperbolicWeight E) x
    The network in Fourier expression form on the Poincaré ball. 
  • complete
    theorem LeanRidgelet.fs_hyperbolic_reconstruction_of_inversion.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      (  :   ) (W : ) (c :   ) (f : E  )
      (hinv : HyperbolicSpace.HasInversion W c f) (x : E) :
      LeanRidgelet.hyperbolicFourierExpression E 
          (LeanRidgelet.separationOfVariables
            (HyperbolicSpace.helgasonFourier f)
            (SymmetricSpace.plancherelDensity W c) )
          x =
        LeanRidgelet.fourierSlicePairing 1   * f x
    theorem LeanRidgelet.fs_hyperbolic_reconstruction_of_inversion.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (  :   ) (W : ) (c :   )
      (f : E  )
      (hinv :
        HyperbolicSpace.HasInversion W c f)
      (x : E) :
      LeanRidgelet.hyperbolicFourierExpression
          E 
          (LeanRidgelet.separationOfVariables
            (HyperbolicSpace.helgasonFourier
              f)
            (SymmetricSpace.plancherelDensity
              W c)
            )
          x =
        LeanRidgelet.fourierSlicePairing 1 
             *
          f x
    **The reconstruction formula on real hyperbolic space** (Theorem 5.2 at `X = ℍ^m`), conditional
    on the Helgason--Fourier inversion formula for `ℍ^m` and on nothing else.
    
    Every piece of geometry is now fixed — the invariant measure of the ball, the uniform measure on the
    boundary sphere, the composite distance and `ϱ` — so the hypothesis `HyperbolicSpace.HasInversion`
    is a definite claim about a definite space rather than a schema. That is the difference from
    `fs_symmetric_reconstruction_of_inversion`, whose hypothesis mentions free data.
    
    The scalar is `fourierSlicePairing 1`: rank one, so the Jacobian exponent is `1` and not the
    dimension `m`. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    contains sorry
    theorem LeanRidgelet.fs_hyperbolicHelgasonInversion.{u_2} (E : Type u_2)
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] [Nontrivial E] :
       W c,
        0 < W 
           (f : E  ),
            ContDiff  (↑) f 
              HasCompactSupport f 
                tsupport f  HyperbolicSpace.poincareBall E 
                  HyperbolicSpace.HasInversion W c f
    theorem LeanRidgelet.fs_hyperbolicHelgasonInversion.{u_2}
      (E : Type u_2) [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E] :
       W c,
        0 < W 
           (f : E  ),
            ContDiff  (↑) f 
              HasCompactSupport f 
                tsupport f 
                    HyperbolicSpace.poincareBall
                      E 
                  HyperbolicSpace.HasInversion
                    W c f
    **The Helgason--Fourier inversion formula on `ℍ^m`**, the input the reconstruction formula of
    Section 5 needs at the article's first example:
    
    `f(x) = |W|^{-1} ∫_ℝ ∫_{𝕊^{m-1}} f̂(λ,u) e^{(iλ+ϱ)⟨x,u⟩} |c(λ)|^{-2} du dλ`
    
    in the Poincaré ball model, with `dλ` Lebesgue measure on `ℝ`, `du` the uniform probability measure
    on the boundary sphere, and `dμ` the invariant measure `(2/(1-‖x‖²))^m dx`.
    
    Every piece of that statement is now constructed, which is what makes this a proposition rather
    than a schema: `fs_symmetric_reconstruction_of_inversion` receives the geometry as free data, and
    with free data the formula has no truth value. Feeding the ball model to the abstract layer fixes
    it,
    and `fs_hyperbolic_reconstruction_of_inversion` turns this target into the article's reconstruction
    formula on `ℍ^m` with nothing else assumed.
    
    The order of the Weyl group and the `c`-function are existential rather than fixed, for the same
    reason as in `fs_svdJacobian`: the triple `(|W|, c, dλ)` is only meaningful jointly. S. Helgason
    normalizes `c` by `c(-iϱ) = 1` in *Groups and Geometric Analysis* but writes the inversion formula
    of
    *Geometric Analysis on Symmetric Spaces* against a normalization of `dλ` that is not Lebesgue
    measure, and read with Lebesgue `dλ` the two differ by a power of `π`; the article's appendix mixes
    the two. Producing the constant is part of proving this, not of stating it — the same discipline
    that
    made the constant of the matrix polar integration formula come out as a ratio of sphere areas.
    
    No nonvanishing of `c` is asserted: the rank-one `c`-function is a ratio of Gamma factors with a
    pole
    at the origin, and correspondingly `|c(λ)|^{-2}` vanishes there.
    
    The test functions are the smooth ones compactly supported inside the ball, which is `𝒟(X)` for the
    ball model; that is the class Helgason's Theorem 1.3, Ch. III states the formula for. 
Definition3.1.14
Statement uses 4
Statement dependency previews
Preview
Theorem 3.1.12
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

Continuous horospherical SPD network (Section 5). The symmetric positive definite matrices \mathbb P_m=GL(m,\mathbb R)/O(m), composite distance \langle x,u\rangle_j=\log|(u^\top xu)_j| through the leading principal minors, \varrho=(-\tfrac12,\ldots,-\tfrac12,(m-1)/4), rank m. Higher rank, so the c-function is a product over the restricted root system. This example is now in Lean throughout: the minors the composite distance is read from together with their invariance under the nilpotent and finite factors of the Iwasawa decomposition, the chart model carrying the invariant measure |\det x|^{-(m+1)/2}\prod_{i\le j}\mathrm dx_{ij}, the composite distance, the Helgason--Fourier transform, the network, the ridgelet transform, and the reconstruction formula fs_spd_reconstruction_of_inversion — which assumes the inversion formula for \mathbb P_m and nothing else, that formula being the target fs_spdHelgasonInversion.

The article writes the same composite distance as \tfrac12\log\lambda in the Cholesky diagonal, which is equivalent — the minors are the partial products |Y_j|=\prod_{i\le j}\lambda_i — but takes its constants from Terras, who writes everything in the minors. Formalizing in Terras' coordinates rather than the article's therefore fixes \varrho at the article's stated value instead of leaving it free, and it also removes a dependency: in the Cholesky diagonal the N- and M-invariance of the composite distance need uniqueness of the LDL decomposition, which Mathlib does not have, and in the minors they are elementary. |W| and c remain parameters, pending the conversion from Terras' contour measure to Lebesgue measure on \mathfrak a^*.

Lean code for Definition3.1.1416 declarations, 1 incomplete
  • def Matrix.cornerDet {m : } (Y : Matrix (Fin m) (Fin m) ) (i : Fin m) : 
    def Matrix.cornerDet {m : }
      (Y : Matrix (Fin m) (Fin m) )
      (i : Fin m) : 
    Implementation after :=
    :=
      (Y.submatrix (cornerEmb i) (cornerEmb i)).det
    The determinant of the upper-left `(i+1) × (i+1)` corner of `Y`, the `(i+1)`-st leading
    principal minor. Terras' power function on `ℙ_m` is the product of real powers of these. 
  • theorem Matrix.cornerDet_conj_of_lowerTriangular_unit {m : }
      {L Y : Matrix (Fin m) (Fin m) }
      (hL :  (p q : Fin m), p < q  L p q = 0)
      (hd :  (p : Fin m), L p p = 1) (i : Fin m) :
      (L * Y * L.transpose).cornerDet i = Y.cornerDet i
    theorem Matrix.cornerDet_conj_of_lowerTriangular_unit
      {m : } {L Y : Matrix (Fin m) (Fin m) }
      (hL :
         (p q : Fin m), p < q  L p q = 0)
      (hd :  (p : Fin m), L p p = 1)
      (i : Fin m) :
      (L * Y * L.transpose).cornerDet i =
        Y.cornerDet i
    **`N`-invariance of the leading principal minors.** Conjugating by a lower triangular matrix
    with unit diagonal does not change them. Horospheres in `ℙ_m` are the orbits of the nilpotent factor
    of the Iwasawa decomposition, so this is what makes the composite distance a function of the
    horosphere.
    
    In the Cholesky diagonal the same statement needs uniqueness of the LDL decomposition, which Mathlib
    does not have; here it is the corner identity together with `det L_j = 1`. 
  • theorem Matrix.cornerDet_conj_diagonal_sign {m : }
      {Y : Matrix (Fin m) (Fin m) } {d : Fin m  }
      (hd :  (p : Fin m), d p = 1  d p = -1) (i : Fin m) :
      (Matrix.diagonal d * Y * (Matrix.diagonal d).transpose).cornerDet i =
        Y.cornerDet i
    theorem Matrix.cornerDet_conj_diagonal_sign
      {m : } {Y : Matrix (Fin m) (Fin m) }
      {d : Fin m  }
      (hd :  (p : Fin m), d p = 1  d p = -1)
      (i : Fin m) :
      (Matrix.diagonal d * Y *
              (Matrix.diagonal
                  d).transpose).cornerDet
          i =
        Y.cornerDet i
    **`M`-invariance of the leading principal minors.** Conjugating by a diagonal matrix of signs
    does not change them, because the corner determinant of such a matrix squares to `1`. The boundary
    of `ℙ_m` is `K/M` with `M = D_{±1}`, so this is what makes the composite distance well defined on
    the boundary. 
  • theorem Matrix.cornerDet_of_ldl {m : } {L Y : Matrix (Fin m) (Fin m) }
      {d : Fin m  } (hL :  (p q : Fin m), p < q  L p q = 0)
      (hone :  (p : Fin m), L p p = 1)
      (hY : Y = L * Matrix.diagonal d * L.transpose) (i : Fin m) :
      Y.cornerDet i =  c, d (Matrix.cornerEmb i c)
    theorem Matrix.cornerDet_of_ldl {m : }
      {L Y : Matrix (Fin m) (Fin m) }
      {d : Fin m  }
      (hL :
         (p q : Fin m), p < q  L p q = 0)
      (hone :  (p : Fin m), L p p = 1)
      (hY :
        Y =
          L * Matrix.diagonal d * L.transpose)
      (i : Fin m) :
      Y.cornerDet i =
         c, d (Matrix.cornerEmb i c)
    **The corner determinants are the partial products of the Cholesky diagonal.** If
    `Y = L (diagonal d) Lᵀ` with `L` lower triangular with unit diagonal, then `|Y_j| = ∏_{i ≤ j} d_i`.
    
    This is the translation between the two coordinate systems in which harmonic analysis on `ℙ_m` is
    written: the article's composite distance is `½ log λ` in the Cholesky diagonal, Terras' power
    function is built from `log|Y_j|`, and the two therefore differ by a triangular partial-sum
    substitution. 
  • def SpdSpace.ofUpper {m : } (c : EuclideanSpace  (SpdSpace.UpperIdx m)) :
      Matrix (Fin m) (Fin m) 
    def SpdSpace.ofUpper {m : }
      (c :
        EuclideanSpace 
          (SpdSpace.UpperIdx m)) :
      Matrix (Fin m) (Fin m) 
    Implementation after :=
    :=
      Matrix.of fun i j => if h : i ≤ j then c ⟨(i, j), h⟩ else c ⟨(j, i), (not_le.1 h).le⟩
    The symmetric matrix with prescribed upper-triangular coordinates. Together with
    `SpdSpace.invariantMeasure` this is the chart in which the article's `∏_{i ≤ j} dx_{ij}` is
    Lebesgue measure. 
  • def SpdSpace.invariantMeasure (m : ) :
      MeasureTheory.Measure (EuclideanSpace  (SpdSpace.UpperIdx m))
    def SpdSpace.invariantMeasure (m : ) :
      MeasureTheory.Measure
        (EuclideanSpace 
          (SpdSpace.UpperIdx m))
    Implementation after :=
    :=
      (volume.restrict (chart m)).withDensity fun c => ENNReal.ofReal (invariantDensity m c)
    **The `G`-invariant measure of `ℙ_m`**, `|det x|^{-(m+1)/2} ∏_{i ≤ j} dx_{ij}`, read on
    the chart and concentrated on the positive definite cone.
    
    No manifold theory and no normed-space structure on the symmetric matrices is needed: Lebesgue
    measure of the chart *is* `∏_{i ≤ j} dx_{ij}`. The invariance under `g · x = g x g^⊤` is the
    Jacobian statement of a later file; here the measure is only defined. 
  • def SpdSpace.compositeDistance {m : }
      (c : EuclideanSpace  (SpdSpace.UpperIdx m))
      (Q : SpdSpace.Boundary m) : EuclideanSpace  (Fin m)
    def SpdSpace.compositeDistance {m : }
      (c :
        EuclideanSpace 
          (SpdSpace.UpperIdx m))
      (Q : SpdSpace.Boundary m) :
      EuclideanSpace  (Fin m)
    Implementation after :=
    :=
      WithLp.toLp 2 fun i =>
        Real.log (Matrix.cornerDetTotal ((boundaryMatrix Q)ᵀ * ofUpper c * boundaryMatrix Q) i)
    **The vector-valued composite distance of `ℙ_m`**, `⟨x, kM⟩_j = log|(k^⊤ x k)_j|`, the vector of
    logarithms of the leading principal minors.
    
    The rank of `ℙ_m` is `m`, so this is genuinely vector valued — unlike the rank-one hyperbolic case,
    where the composite distance is a scalar. Pairing it against `s` and exponentiating returns Terras'
    power function `p_s(Y) = ∏_j|Y_j|^{s_j}` exactly, which is what lets her `ϱ`, `c`-function and
    constant be used without a change of variables. The minors are read through
    `Matrix.cornerDetTotal`, the total form, so that no positive-definiteness proof has to be carried
    into the definition; on the chart the matrix is positive definite and the total form agrees with the
    minors. 
  • def SpdSpace.spdRho (m : ) : EuclideanSpace  (Fin m)
    def SpdSpace.spdRho (m : ) :
      EuclideanSpace  (Fin m)
    Implementation after :=
    :=
      WithLp.toLp 2 fun i => if (i : ℕ) + 1 = m then ((m : ℝ) - 1) / 4 else -(1 / 2)
    **Terras' shift** `ϱ = -ρ = (-½,…,-½,(m-1)/4)`, the constant of the Helgason--Fourier transform
    of `ℙ_m` in the coordinates of the power function. The last coordinate is the exceptional one; the
    contour of the inversion formula is `Re s = ϱ`. 
  • def SpdSpace.helgasonFourier {m : } (rho : EuclideanSpace  (Fin m))
      (f : EuclideanSpace  (SpdSpace.UpperIdx m)  )
      (lam : EuclideanSpace  (Fin m)) (Q : SpdSpace.Boundary m) : 
    def SpdSpace.helgasonFourier {m : }
      (rho : EuclideanSpace  (Fin m))
      (f :
        EuclideanSpace 
            (SpdSpace.UpperIdx m) 
          )
      (lam : EuclideanSpace  (Fin m))
      (Q : SpdSpace.Boundary m) : 
    Implementation after :=
    :=
      SymmetricSpace.helgasonFourier (invariantMeasure m) compositeDistance rho f lam Q
    **The Helgason--Fourier transform on `ℙ_m`**,
    `f̂(λ,u) = ∫ f(x) e^{(-iλ+ϱ)⟨x,u⟩} dμ(x)`,
    with `μ` the invariant measure of `ℙ_m` and `ϱ` a parameter. 
  • def SpdSpace.HasInversion {m : } (W : ) (c : EuclideanSpace  (Fin m)  )
      (f : EuclideanSpace  (SpdSpace.UpperIdx m)  ) : Prop
    def SpdSpace.HasInversion {m : } (W : )
      (c : EuclideanSpace  (Fin m)  )
      (f :
        EuclideanSpace 
            (SpdSpace.UpperIdx m) 
          ) :
      Prop
    Implementation after :=
    :=
      SymmetricSpace.HasHelgasonInversion (invariantMeasure m)
        (volume : Measure (EuclideanSpace ℝ (Fin m)))
        (ContinuousLinearMap.orthogonalHaar (E := EuclideanSpace ℝ (Fin m)))
        compositeDistance (spdRho m) W c f
    **The Helgason--Fourier inversion formula on `ℙ_m`**, as a proposition:
    
    `f(x) = |W|^{-1} ∫_{𝔞*} ∫_{∂ℙ_m} f̂(λ,u) e^{(iλ+ϱ)⟨x,u⟩} |c(λ)|^{-2} du dλ`
    
    with `dλ` Lebesgue measure on `𝔞* ≅ ℝ^m`, `du` the Haar probability measure of the orthogonal
    group, and `dμ` the invariant measure `|det x|^{-(m+1)/2} ∏_{i ≤ j} dx_{ij}`.
    
    Rank `m`, so the frequency is a vector and the Jacobian exponent of the reconstruction formula is
    `m` — the opposite extreme from the hyperbolic case, where the rank is one whatever the dimension.
    `ϱ` is Terras' `spdRho`; the order of the Weyl group and the `c`-function remain parameters, for
    the reason given in the module docstring. 
  • complete
    def LeanRidgelet.spdWeight {m : }
      (c : EuclideanSpace  (SpdSpace.UpperIdx m))
      (Q : SpdSpace.Boundary m) : 
    def LeanRidgelet.spdWeight {m : }
      (c :
        EuclideanSpace 
          (SpdSpace.UpperIdx m))
      (Q : SpdSpace.Boundary m) : 
    Implementation after :=
    :=
      SymmetricSpace.horosphericalCharacter (SpdSpace.spdRho m) 0 (SpdSpace.compositeDistance c Q)
    The weight `e^{ϱ⟨x,u⟩}` that a layer of the continuous horospherical SPD network carries: the
    horospherical character of `ℙ_m` at zero frequency. 
  • complete
    def LeanRidgelet.spdSynthesis {m : } (σ :   )
      (γ : EuclideanSpace  (Fin m)  SpdSpace.Boundary m    )
      (x : EuclideanSpace  (SpdSpace.UpperIdx m)) : 
    def LeanRidgelet.spdSynthesis {m : }
      (σ :   )
      (γ :
        EuclideanSpace  (Fin m) 
          SpdSpace.Boundary m    )
      (x :
        EuclideanSpace 
          (SpdSpace.UpperIdx m)) :
      
    Implementation after :=
    :=
      sliceSynthesis (volume : Measure (EuclideanSpace ℝ (Fin m)))
        (ContinuousLinearMap.orthogonalHaar (E := EuclideanSpace ℝ (Fin m))) σ γ
        SpdSpace.compositeDistance spdWeight x
    **The continuous horospherical SPD network** (Section 5),
    `S[γ](x) = ∫_{ℝ^m × ∂ℙ_m × ℝ} γ(a,u,b) σ(a · ⟨x,u⟩ - b) e^{ϱ⟨x,u⟩} da du db`.
    
    The scale variable is a vector of `ℝ^m` because `ℙ_m` has rank `m`. 
  • complete
    def LeanRidgelet.spdRidgelet {m : } (ρ :   )
      (cf : EuclideanSpace  (SpdSpace.UpperIdx m)  )
      (a : EuclideanSpace  (Fin m)) (Q : SpdSpace.Boundary m) (b : ) : 
    def LeanRidgelet.spdRidgelet {m : }
      (ρ :   )
      (cf :
        EuclideanSpace 
            (SpdSpace.UpperIdx m) 
          )
      (a : EuclideanSpace  (Fin m))
      (Q : SpdSpace.Boundary m) (b : ) : 
    Implementation after :=
    :=
      ∫ x : EuclideanSpace ℝ (SpdSpace.UpperIdx m), cf x *
        conj (ρ (inner ℝ a (SpdSpace.compositeDistance x Q) - b)) * spdWeight x Q
        ∂(SpdSpace.invariantMeasure m)
    The ridgelet transform on `ℙ_m`,
    `R[f;ρ](a,u,b) = ∫ c[f](x) conj (ρ(a · ⟨x,u⟩ - b)) e^{ϱ⟨x,u⟩} dμ(x)`,
    against the multiplier `c[f]` the article inserts to cancel one power of the Harish-Chandra
    density. 
  • complete
    def LeanRidgelet.spdFourierExpression {m : } ( :   )
      (Γ : EuclideanSpace  (Fin m)  SpdSpace.Boundary m    )
      (x : EuclideanSpace  (SpdSpace.UpperIdx m)) : 
    def LeanRidgelet.spdFourierExpression {m : }
      ( :   )
      (Γ :
        EuclideanSpace  (Fin m) 
          SpdSpace.Boundary m    )
      (x :
        EuclideanSpace 
          (SpdSpace.UpperIdx m)) :
      
    Implementation after :=
    :=
      fourierExpressionSynthesis (volume : Measure (EuclideanSpace ℝ (Fin m)))
        (ContinuousLinearMap.orthogonalHaar (E := EuclideanSpace ℝ (Fin m))) Fσ Γ
        SpdSpace.compositeDistance spdWeight x
    The network in Fourier expression form on `ℙ_m`. 
  • complete
    theorem LeanRidgelet.fs_spd_reconstruction_of_inversion {m : } (  :   )
      (W : ) (c : EuclideanSpace  (Fin m)  )
      (f : EuclideanSpace  (SpdSpace.UpperIdx m)  )
      (hinv : SpdSpace.HasInversion W c f)
      (x : EuclideanSpace  (SpdSpace.UpperIdx m)) :
      LeanRidgelet.spdFourierExpression 
          (LeanRidgelet.separationOfVariables
            (SpdSpace.helgasonFourier (SpdSpace.spdRho m) f)
            (SymmetricSpace.plancherelDensity W c) )
          x =
        LeanRidgelet.fourierSlicePairing (↑m)   * f x
    theorem LeanRidgelet.fs_spd_reconstruction_of_inversion
      {m : } (  :   ) (W : )
      (c : EuclideanSpace  (Fin m)  )
      (f :
        EuclideanSpace 
            (SpdSpace.UpperIdx m) 
          )
      (hinv : SpdSpace.HasInversion W c f)
      (x :
        EuclideanSpace 
          (SpdSpace.UpperIdx m)) :
      LeanRidgelet.spdFourierExpression 
          (LeanRidgelet.separationOfVariables
            (SpdSpace.helgasonFourier
              (SpdSpace.spdRho m) f)
            (SymmetricSpace.plancherelDensity
              W c)
            )
          x =
        LeanRidgelet.fourierSlicePairing (↑m)
              *
          f x
    **The reconstruction formula on the manifold of positive definite matrices** (Theorem 5.2 at
    `X = ℙ_m`), conditional on the Helgason--Fourier inversion formula for `ℙ_m` and on nothing else.
    
    The geometry is fixed: the invariant measure `|det x|^{-(m+1)/2} ∏_{i ≤ j} dx_{ij}`, the Haar
    probability measure of the orthogonal group standing in for the boundary `K/M`, and the composite
    distance `⟨x,u⟩_j = log|(u^⊤ x u)_j|` in the leading principal minors, and the shift
    `ϱ = (-½,…,-½,(m-1)/4)`. So the hypothesis `SpdSpace.HasInversion` is a definite claim about a
    definite space.
    
    The scalar is `fourierSlicePairing m`: rank `m`, so the Jacobian exponent is the rank, which here
    coincides with a dimension count only because `ℙ_m` is a maximal-rank space. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    contains sorry
    theorem LeanRidgelet.fs_spdHelgasonInversion (m : ) :
       W c,
        0 < W 
           (f : EuclideanSpace  (SpdSpace.UpperIdx m)  ),
            ContDiff  (↑) f 
              HasCompactSupport f 
                tsupport f  SpdSpace.chart m  SpdSpace.HasInversion W c f
    theorem LeanRidgelet.fs_spdHelgasonInversion
      (m : ) :
       W c,
        0 < W 
          
            (f :
              EuclideanSpace 
                  (SpdSpace.UpperIdx m) 
                ),
            ContDiff  (↑) f 
              HasCompactSupport f 
                tsupport f 
                    SpdSpace.chart m 
                  SpdSpace.HasInversion W c f
    **The Helgason--Fourier inversion formula on `ℙ_m = GL(m,ℝ)/O(m)`**, the input the
    reconstruction formula of Section 5 needs at the article's second example:
    
    `f(x) = |W|^{-1} ∫_{𝔞*} ∫_{∂ℙ_m} f̂(λ,u) e^{(iλ+ϱ)⟨x,u⟩} |c(λ)|^{-2} du dλ`
    
    read in the chart of upper-triangular coordinates, with `dλ` Lebesgue measure on `𝔞* ≅ ℝ^m`, `du`
    the Haar probability measure of the orthogonal group standing in for `K/M`, and `dμ` the invariant
    measure `|det x|^{-(m+1)/2} ∏_{i ≤ j} dx_{ij}`.
    
    This is the higher-rank companion of `fs_hyperbolicHelgasonInversion`: the rank of `ℙ_m` is `m`, so
    the frequency is a vector, and `fs_spd_reconstruction_of_inversion` turns this target into the
    article's reconstruction formula with the Jacobian exponent `m`.
    
    `ϱ` is *not* existential: `SpdSpace.HasInversion` fixes it to `SpdSpace.spdRho m`, the article's
    `(-½,…,-½,(m-1)/4)`, which is the contour `Re s = -ρ` of A. Terras, *Harmonic Analysis on Symmetric
    Spaces*, Thm 1.3.1(1), read in the coordinates this model uses — the leading principal minors, the
    ones her power function `p_s(Y) = ∏_j |Y_j|^{s_j}` is written in. `|W|` and `c` stay existential:
    Terras gives both explicitly, but her contour measure has to be converted to Lebesgue measure on
    `𝔞*` first, and that conversion is part of proving this. 
Theorem3.1.15
Statement uses 3
Statement dependency previews
Preview
Theorem 3.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Definition 3.1.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Reconstruction formula on G/K (Theorem 5.2), conditional on inversion. The instance of the abstract scheme in which the input domain is G/K, the direction space is the boundary \partial X, the scale space is \mathfrak a^*\cong\mathbb R^r, the weight is e^{\varrho\langle x,u\rangle} and the inversion density is |W|^{-1}|c(\lambda)|^{-2}. The Helgason--Fourier inversion formula is the hypothesis, entering here and only here as an explicit hypothesis of a theorem — never an axiom, a structure field or a sorry. Proving it, first for the hyperbolic space and the manifold of positive definite matrices, is the separate long-term milestone M10. The hypothesis was written out by hand when the theorem was stated, before the Helgason--Fourier theory existed; the last three declarations identify it with SymmetricSpace.HasHelgasonInversion — the layer's plane wave times its horospherical weight is the horospherical character, and the article's density is the Plancherel density — so what remains to be supplied for a concrete space is exactly the inversion formula and nothing else.

Lean code for Theorem3.1.155 theorems
  • 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) (  :   )
      (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 
          (LeanRidgelet.separationOfVariables Ff
            (LeanRidgelet.harishChandraDensity W cfun) )
          x =
        LeanRidgelet.fourierSlicePairing (↑r)   * 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)
      (  :   )
      (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 
          (LeanRidgelet.separationOfVariables
            Ff
            (LeanRidgelet.harishChandraDensity
              W cfun)
            )
          x =
        LeanRidgelet.fourierSlicePairing (↑r)
              *
          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. 
  • complete
    theorem LeanRidgelet.fs_symmetricFourierExpression_euclidean {r : }
      ( :   ) (Γ : LeanRidgelet.InputSpace r  Unit    )
      (x : LeanRidgelet.InputSpace r) :
      LeanRidgelet.symmetricFourierExpression
          (MeasureTheory.Measure.dirac ()) 0 (fun y x  y)  Γ x =
        LeanRidgelet.fourierExpressionSynthesis MeasureTheory.volume
          (MeasureTheory.Measure.dirac ())  Γ (fun y x  y)
          (fun x x_1  1) x
    theorem LeanRidgelet.fs_symmetricFourierExpression_euclidean
      {r : } ( :   )
      (Γ :
        LeanRidgelet.InputSpace r 
          Unit    )
      (x : LeanRidgelet.InputSpace r) :
      LeanRidgelet.symmetricFourierExpression
          (MeasureTheory.Measure.dirac ()) 0
          (fun y x  y)  Γ x =
        LeanRidgelet.fourierExpressionSynthesis
          MeasureTheory.volume
          (MeasureTheory.Measure.dirac ()) 
          Γ (fun y x  y) (fun x x_1  1) x
    The shape is inhabited: with a one-point boundary, `ϱ = 0` and the identity as composite
    distance, the symmetric-space Fourier expression is the Euclidean one of `FS.Euclidean`, whose
    reconstruction formula `fs_reconstruction_euclidean` is the same instance of the same theorem. So
    the conditional theorem above is not vacuous in shape — only the Helgason--Fourier inversion
    formula itself is out of reach. 
  • complete
    theorem LeanRidgelet.fs_fourierSlicePhase_mul_horosphericalWeight.{u_1, u_2}
      {r : } {X : Type u_1} {U : Type u_2}
      (ϱ lam : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r) (x : X) (u : U) :
      LeanRidgelet.fourierSlicePhase (inner  lam (cd x u)) *
          LeanRidgelet.horosphericalWeight ϱ cd x u =
        SymmetricSpace.horosphericalCharacter ϱ lam (cd x u)
    theorem LeanRidgelet.fs_fourierSlicePhase_mul_horosphericalWeight.{u_1,
        u_2}
      {r : } {X : Type u_1} {U : Type u_2}
      (ϱ lam : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r)
      (x : X) (u : U) :
      LeanRidgelet.fourierSlicePhase
            (inner  lam (cd x u)) *
          LeanRidgelet.horosphericalWeight ϱ
            cd x u =
        SymmetricSpace.horosphericalCharacter
          ϱ lam (cd x u)
    The layer's plane wave times its horospherical weight is the horospherical character
    `e^{(iλ+ϱ)⟪x,u⟫}` of the Helgason--Fourier theory. 
  • complete
    theorem LeanRidgelet.fs_harishChandraDensity_eq {r : } (W : )
      (cfun : LeanRidgelet.InputSpace r  ) :
      LeanRidgelet.harishChandraDensity W cfun =
        SymmetricSpace.plancherelDensity W cfun
    theorem LeanRidgelet.fs_harishChandraDensity_eq
      {r : } (W : )
      (cfun : LeanRidgelet.InputSpace r  ) :
      LeanRidgelet.harishChandraDensity W
          cfun =
        SymmetricSpace.plancherelDensity W
          cfun
    The article's density `|W|⁻¹|c(λ)|⁻²` is the Plancherel density of the inversion formula. 
  • complete
    theorem LeanRidgelet.fs_symmetric_reconstruction_of_helgasonInversion.{u_1, u_2}
      {r : } {X : Type u_1} {U : Type u_2} [MeasurableSpace U]
      [MeasurableSpace X] (μX : MeasureTheory.Measure X)
      (ν : MeasureTheory.Measure U) (ϱ : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r) (  :   ) (W : )
      (cfun : LeanRidgelet.InputSpace r  ) (f : X  )
      (hinv :
        SymmetricSpace.HasHelgasonInversion μX MeasureTheory.volume ν cd ϱ W
          cfun f)
      (x : X) :
      LeanRidgelet.symmetricFourierExpression ν ϱ cd 
          (LeanRidgelet.separationOfVariables
            (SymmetricSpace.helgasonFourier μX cd ϱ f)
            (LeanRidgelet.harishChandraDensity W cfun) )
          x =
        LeanRidgelet.fourierSlicePairing (↑r)   * f x
    theorem LeanRidgelet.fs_symmetric_reconstruction_of_helgasonInversion.{u_1,
        u_2}
      {r : } {X : Type u_1} {U : Type u_2}
      [MeasurableSpace U] [MeasurableSpace X]
      (μX : MeasureTheory.Measure X)
      (ν : MeasureTheory.Measure U)
      (ϱ : LeanRidgelet.InputSpace r)
      (cd : X  U  LeanRidgelet.InputSpace r)
      (  :   ) (W : )
      (cfun : LeanRidgelet.InputSpace r  )
      (f : X  )
      (hinv :
        SymmetricSpace.HasHelgasonInversion μX
          MeasureTheory.volume ν cd ϱ W cfun
          f)
      (x : X) :
      LeanRidgelet.symmetricFourierExpression
          ν ϱ cd 
          (LeanRidgelet.separationOfVariables
            (SymmetricSpace.helgasonFourier μX
              cd ϱ f)
            (LeanRidgelet.harishChandraDensity
              W cfun)
            )
          x =
        LeanRidgelet.fourierSlicePairing (↑r)
              *
          f x
    **The reconstruction formula on `G/K`, with the Helgason--Fourier inversion formula as the
    hypothesis in its own terms.** This is `fs_symmetric_reconstruction_of_inversion` with the
    hand-written hypothesis replaced by `SymmetricSpace.HasHelgasonInversion`, and the Fourier data
    replaced by the Helgason--Fourier transform itself rather than left as an arbitrary function.
    
    Proving the hypothesis for a concrete `X` — first the hyperbolic space, then the manifold of
    positive definite matrices — is the separate long-term milestone; what is settled here is that
    there is nothing else left to supply. 

The shape is inhabited: a one-point boundary with \varrho=0 and the identity as composite distance returns the Euclidean instance, so the conditional theorem is not vacuous in shape. The article's scalar \frac{|W|}{2\pi}\int\sigma^\sharp\overline{\rho^\sharp}|\omega|^{-r} is the Fourier slice pairing with |W| moved into the density of the inversion formula, where it belongs.

Section 6: the d-plane layer and pooling

Definition3.1.16
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 3.1.17
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

The d-plane transform and the d-plane layer. P_d[f](U,\boldsymbol b)=\int_{\ker U}f(U\boldsymbol b+y)\,\mathrm dy and S[\gamma](\boldsymbol x)=\int\gamma(U,\boldsymbol b)\sigma(U^\top\boldsymbol x-\boldsymbol b), with a multivariate activation \sigma:\mathbb R^k\to\mathbb C modelling a pooling layer. The Stiefel manifold is the type of linear isometries \mathbb R^k\to E, which is what an orthonormal k-frame is. At codimension one that type is the unit sphere, and the layer is written over the sphere directly; the layers over the full-column-rank matrices and over the similitude group are not yet defined.

Lean code for Definition3.1.166 definitions
  • def MeasureTheory.dPlaneTransform.{u_1, u_2} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
      [NormedAddCommGroup F] [NormedSpace  F] (f : E  F)
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (b : EuclideanSpace  (Fin k)) : F
    def MeasureTheory.dPlaneTransform.{u_1, u_2}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {F : Type u_2} [NormedAddCommGroup F]
      [NormedSpace  F] (f : E  F)
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (b : EuclideanSpace  (Fin k)) : F
    Implementation after :=
    :=
      ∫ y : ((LinearMap.range L.toLinearMap)ᗮ : Submodule ℝ E), f (L b + (y : E))
    The `d`-plane transform `P_d[f](L, b) = ∫_{(range L)ᗮ} f (L b + y) dy`, the integral of `f`
    over the `d`-plane through `L b` parallel to the orthogonal complement of the frame. 
  • def MeasureTheory.planeOrthogonalSplit.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E) :
      EuclideanSpace  (Fin k) × L.range ≃ᵐ E
    def MeasureTheory.planeOrthogonalSplit.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (L :
        EuclideanSpace  (Fin k) →ₗᵢ[] E) :
      EuclideanSpace  (Fin k) × L.range ≃ᵐ
        E
    Implementation after :=
    :=
      (MeasurableEquiv.toLp 2 (EuclideanSpace ℝ (Fin k) ×
          ((LinearMap.range L.toLinearMap)ᗮ : Submodule ℝ E))).trans
        (((LinearIsometryEquiv.withLpProdCongr 2 L.equivRange
            (LinearIsometryEquiv.refl ℝ ((LinearMap.range L.toLinearMap)ᗮ : Submodule ℝ E))).trans
          (LinearMap.range L.toLinearMap).orthogonalDecomposition.symm).toMeasurableEquiv)
    The parametrization `(b, y) ↦ L b + y` of `E` by the range of the frame `L` and its orthogonal
    complement, as a measurable equivalence. For `k = 1` this is
    `MeasureTheory.lineOrthogonalSplit`. 
  • 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. 
  • 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`. 
  • 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. 
  • complete
    def LeanRidgelet.sphereFourierExpression {m : } ( :   )
      (Γ : (Metric.sphere 0 1)    ) (x : LeanRidgelet.InputSpace m) : 
    def LeanRidgelet.sphereFourierExpression
      {m : } ( :   )
      (Γ : (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`. 
Theorem3.1.17
Statement uses 2
Statement dependency previews
Preview
Definition 3.1.16
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Over the Stiefel manifold the ridgelet transform degenerates to a Radon transform. If g is a fractional derivative of f of order s, the bias spectrum of P_d[g](U,\cdot) is \|\boldsymbol\omega\|^s\widehat f(U\boldsymbol\omega). The article's ansatz over the Stiefel manifold is \gamma^\sharp(U,\boldsymbol\omega)=\widehat f(U\boldsymbol\omega)|U\boldsymbol\omega|^{d-t}, which is that right-hand side with s=d-t, so the coefficient function the method produces is the d-plane transform of a fractional derivative of the target. The fractional Laplacian is not in Mathlib, so its multiplier property is the hypothesis rather than a definition.

Lean code for Theorem3.1.171 theorem
  • 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. 
Lemma3.1.18
uses 1used by 1L∃∀N

The matrix polar integration formula at codimension one (Lemma C.2, k=1). c_{m,k}\int_{\mathbb R^m}F=\int_{V_{m,k}\times\mathbb R^k}F(U\boldsymbol b)|U\boldsymbol b|^{m-k} becomes, at k=1, the two-sided polar formula: the Stiefel manifold is the unit sphere, the weight |U b|^{m-1} is |b|^{m-1}, and the constant c_{m,1}=\int_{\mathbb S^0\times V_{m,0}}=2 is the double cover (b,\boldsymbol u)\mapsto b\boldsymbol u of \mathbb R^m\setminus\{0\}. So codimension one needs no measure theory on the Stiefel manifold at all, which is why it is the case within reach.

Lean code for Lemma3.1.182 theorems
  • 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}`. 
  • 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. 
Lemma3.1.19
Statement uses 3
Statement dependency previews
Preview
Theorem 3.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

Inversion of the d-plane transform (Lemma 6.2). f(x)=(2\pi)^{-m}\int_{V_{m,k}\times\mathbb R^k}\widehat f(U\boldsymbol\omega)|U\boldsymbol\omega|^{m-k}e^{iU\boldsymbol\omega\cdot x}\,\mathrm d\boldsymbol\omega\,\mathrm dU. The article proves this first and derives the reconstruction formulas from it; here it falls out of the same two ingredients they do — the matrix polar integration formula and Fourier inversion — so it is a corollary rather than a lemma. It is worth stating separately because it is where the constant can be compared, and the comparison finds a third difference: the printed formula has no c_{m,k}, while the article's own Lemma C.2 puts one into the change of variables its proof performs. The correct form is f(x)=(c_{m,k}(2\pi)^m)^{-1}\int\cdots.

Lean code for Lemma3.1.191 theorem
  • complete
    theorem LeanRidgelet.fs_dPlaneInversion.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E) (Ff f : E  ) (x : E)
      (hFfm : MeasureTheory.StronglyMeasurable Ff)
      (hF :
        MeasureTheory.Integrable
          (fun ξ  Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E), Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x) =
          ((2 * Real.pi) ^ Module.finrank  E) * f x) :
      (MeasureTheory.volume.toSphere.real Set.univ) *
           (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
             (ω : EuclideanSpace  (Fin k)),
              (L ω ^ (Module.finrank  E - k)) *
                (Ff (L ω) *
                  LeanRidgelet.fourierSlicePhase
                    (inner  (L ω)
                      x)) ContinuousLinearMap.stiefelMeasure L₀ =
        (MeasureTheory.volume.toSphere.real Set.univ) *
            (2 * Real.pi) ^ Module.finrank  E *
          f x
    theorem LeanRidgelet.fs_dPlaneInversion.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (Ff f : E  ) (x : E)
      (hFfm :
        MeasureTheory.StronglyMeasurable Ff)
      (hF :
        MeasureTheory.Integrable
          (fun ξ 
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E),
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x) =
          ((2 * Real.pi) ^
                Module.finrank  E) *
            f x) :
      (MeasureTheory.volume.toSphere.real
              Set.univ) *
           (L :
            EuclideanSpace  (Fin k) →ₗᵢ[]
              E),
             (ω : EuclideanSpace  (Fin k)),
              (L ω ^
                    (Module.finrank  E -
                      k)) *
                (Ff (L ω) *
                  LeanRidgelet.fourierSlicePhase
                    (inner  (L ω)
                      x)) ContinuousLinearMap.stiefelMeasure
              L₀ =
        (MeasureTheory.volume.toSphere.real
                Set.univ) *
            (2 * Real.pi) ^
              Module.finrank  E *
          f x
    **The inversion formula for the `d`-plane transform**, the article's Lemma 6.2: the Fourier data
    of the target, read along the frames and weighted by `‖Uω‖^{m-k}`, recovers the target.
    
    The article proves this first and derives the reconstruction formulas from it; here it comes out of
    the same two ingredients they do — the matrix polar integration formula and Fourier inversion — so
    it is a corollary rather than a lemma. Stating it separately is worth doing because it is where the
    article's constant can be compared.
    
    *Deviation.* The article writes `f(x) = (2π)^{-m} ∫_{V×ℝ^k} f̂(Uω)|Uω|^{m-k} e^{i⟪Uω,x⟫} dω dU`,
    with no `c_{m,k}`. Its own Lemma C.2 reads `c_{m,k} ∫_{ℝ^m} g = ∫_{V×ℝ^k} g(Ub)|Ub|^{m-k}`, so the
    change of variables in its proof carries a factor `c_{m,k}` that the statement drops: the correct
    form is `f(x) = (c_{m,k}(2π)^m)^{-1} ∫ ⋯`. That is what is proved here, in the normalization of
    `ToMathlib.LieGroup.MatrixPolar`, where `c_{m,k}` appears as the ratio `|𝕊^{k-1}|/|𝕊^{m-1}|` and the
    statement is multiplied out so that no division occurs. 
Theorem3.1.20
Statement uses 4
Statement dependency previews
Preview
Theorem 3.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 3.1.21
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Reconstruction on the Stiefel manifold at codimension one (Theorem 6.3, k=1). For an activation of spectrum \sigma^\sharp(\omega)=|\omega|^t and the coefficient function R[f](\boldsymbol u,b)=\triangle_b^{(d-t)/2}P_d[f](\boldsymbol u,b), d=m-1, the layer over the sphere satisfies S[R[f]](\boldsymbol x)=c_{m,1}(2\pi)^{d}f(\boldsymbol x). The derivation is the master identity: Step 1 turns the layer into its Fourier expression, the separation-of-variables condition makes the integrand |\omega|^{m-1}\widehat f(\omega\boldsymbol u) up to a constant, polar coordinates evaluate the direction integral against c_{m,1}=2, and Fourier inversion evaluates what is left against (2\pi)^m. There is no Step 2: the Stiefel case has no scale parameter to rescale.

Lean code for Theorem3.1.205 theorems
  • complete
    theorem LeanRidgelet.fs_sphere_fourierExpression_of_bias {m : } (σ  :   )
      (γ Γ : (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 ω *  ω *
                  LeanRidgelet.fourierSlicePhase (ω * inner  (↑u) x)) :
      LeanRidgelet.sphereSynthesis σ γ x =
        LeanRidgelet.sphereFourierExpression  Γ x
    theorem LeanRidgelet.fs_sphere_fourierExpression_of_bias
      {m : } (σ  :   )
      (γ Γ : (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 ω *  ω *
                  LeanRidgelet.fourierSlicePhase
                    (ω * inner  (↑u) x)) :
      LeanRidgelet.sphereSynthesis σ γ x =
        LeanRidgelet.sphereFourierExpression
           Γ 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. 
  • complete
    theorem LeanRidgelet.fs_sphere_reconstruction_of_inversion {m : }
      [Nontrivial (LeanRidgelet.InputSpace m)] (c : ) ( :   )
      (Γ : (Metric.sphere 0 1)    )
      (Ff f : LeanRidgelet.InputSpace m  ) (x : LeanRidgelet.InputSpace m)
      (hansatz :
         (u : (Metric.sphere 0 1)),
          ∀ᵐ (ω : ), Γ u ω *  ω = 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  Γ x =
        c * 2 * ((2 * Real.pi) ^ (m - 1)) * f x
    theorem LeanRidgelet.fs_sphere_reconstruction_of_inversion
      {m : }
      [Nontrivial (LeanRidgelet.InputSpace m)]
      (c : ) ( :   )
      (Γ : (Metric.sphere 0 1)    )
      (Ff f : LeanRidgelet.InputSpace m  )
      (x : LeanRidgelet.InputSpace m)
      (hansatz :
         (u : (Metric.sphere 0 1)),
          ∀ᵐ (ω : ),
            Γ u ω *  ω =
              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 
          Γ 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. 
  • 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. 
  • 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. 
  • 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. 

The master identity constrains only the product \gamma^\sharp(\boldsymbol u,\omega)\sigma^\sharp(\omega), so the activation spectrum need not be even; that is what makes the classical Radon formula an instance rather than a limiting case.

Theorem3.1.21
Statement uses 5
Statement dependency previews
Preview
Theorem 3.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 3.1.22
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
L∃∀N

Reconstruction on the Stiefel manifold in general codimension (Theorem 6.3). The same three moves as at codimension one, with the sphere replaced by the Stiefel manifold: Step 1 turns the layer into its Fourier expression, the separation-of-variables condition makes the integrand \widehat f(U\boldsymbol\omega)|U\boldsymbol\omega|^{d} up to a constant, the matrix polar integration formula evaluates the frame integral, and Fourier inversion evaluates what is left. There is still no Step 2. What makes the neuron a plane wave in U\boldsymbol\omega is that the coordinate map is the transpose of the frame, \langle\boldsymbol\omega,U^\top\boldsymbol x\rangle=\langle U\boldsymbol\omega,\boldsymbol x\rangle.

Lean code for Theorem3.1.219 declarations
  • complete
    theorem LeanRidgelet.inner_dPlaneCoord.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E]
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E) (x : E)
      (ω : EuclideanSpace  (Fin k)) :
      inner  ω (LeanRidgelet.dPlaneCoord L x) = inner  (L ω) x
    theorem LeanRidgelet.inner_dPlaneCoord.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (x : E) (ω : EuclideanSpace  (Fin k)) :
      inner  ω
          (LeanRidgelet.dPlaneCoord L x) =
        inner  (L ω) x
    **The coordinate map is the transpose of the frame.** Pairing a bias frequency against the
    coordinate vector `Uᵀ x` is pairing the frequency pushed into the input space against `x`, which is
    what makes the `d`-plane neuron a plane wave in `U ω`. 
  • complete
    def LeanRidgelet.stiefelFourierExpression.{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.stiefelFourierExpression.{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 :=
    :=
      ((2 * (Real.pi : ℂ)) ^ k)⁻¹ *
        ∫ L, (∫ ω : EuclideanSpace ℝ (Fin k),
          Γ L ω * Fσ ω * fourierSlicePhase (inner ℝ ω (dPlaneCoord L x))) ∂ν
    The Fourier expression of the `d`-plane layer over the Stiefel manifold, the output of Step 1:
    `S[γ](x) = (2π)^{-k} ∫_{V_{m,k}} ∫_{ℝ^k} γ♯(U,ω) σ♯(ω) e^{i⟪ω, Uᵀx⟫} dω dU`. 
  • complete
    theorem LeanRidgelet.fs_stiefel_fourierExpression_of_bias.{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)
      (hbias :
         (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
           (b : EuclideanSpace  (Fin k)),
              γ L b * σ (LeanRidgelet.dPlaneCoord L x - b) =
            ((2 * Real.pi) ^ k)⁻¹ *
               (ω : EuclideanSpace  (Fin k)),
                Γ L ω *  ω *
                  LeanRidgelet.fourierSlicePhase
                    (inner  ω (LeanRidgelet.dPlaneCoord L x))) :
      LeanRidgelet.stiefelSynthesis ν σ γ x =
        LeanRidgelet.stiefelFourierExpression ν  Γ x
    theorem LeanRidgelet.fs_stiefel_fourierExpression_of_bias.{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)
      (hbias :
        
          (L :
            EuclideanSpace  (Fin k) →ₗᵢ[]
              E),
           (b : EuclideanSpace  (Fin k)),
              γ L b *
                σ
                  (LeanRidgelet.dPlaneCoord L
                      x -
                    b) =
            ((2 * Real.pi) ^ k)⁻¹ *
               (ω :
                EuclideanSpace  (Fin k)),
                Γ L ω *  ω *
                  LeanRidgelet.fourierSlicePhase
                    (inner  ω
                      (LeanRidgelet.dPlaneCoord
                        L x))) :
      LeanRidgelet.stiefelSynthesis ν σ γ x =
        LeanRidgelet.stiefelFourierExpression
          ν  Γ x
    **Step 1 over the Stiefel manifold**: the layer equals its Fourier expression. As at codimension
    one the analytic input is the bias identity at each frame, now `k`-dimensional, and no Fubini
    rearrangement is needed because with no scale parameter the bias frequency may stay inside the frame
    integral. 
  • complete
    theorem LeanRidgelet.fs_stiefel_reconstruction_of_inversion.{u_1} {k : }
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E] [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E) (c : )
      ( : EuclideanSpace  (Fin k)  )
      (Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E)  EuclideanSpace  (Fin k)  )
      (Ff f : E  ) (x : E)
      (hansatz :
         (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
          ∀ᵐ (ω : EuclideanSpace  (Fin k)),
            Γ L ω *  ω =
              c * (L ω ^ (Module.finrank  E - k)) * Ff (L ω))
      (hFfm : MeasureTheory.StronglyMeasurable Ff)
      (hF :
        MeasureTheory.Integrable
          (fun ξ  Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E), Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x) =
          ((2 * Real.pi) ^ Module.finrank  E) * f x) :
      (MeasureTheory.volume.toSphere.real Set.univ) *
          LeanRidgelet.stiefelFourierExpression
            (ContinuousLinearMap.stiefelMeasure L₀)  Γ x =
        c * (MeasureTheory.volume.toSphere.real Set.univ) *
            (2 * Real.pi) ^ (Module.finrank  E - k) *
          f x
    theorem LeanRidgelet.fs_stiefel_reconstruction_of_inversion.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (c : )
      ( : EuclideanSpace  (Fin k)  )
      (Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k)  )
      (Ff f : E  ) (x : E)
      (hansatz :
        
          (L :
            EuclideanSpace  (Fin k) →ₗᵢ[]
              E),
          ∀ᵐ (ω : EuclideanSpace  (Fin k)),
            Γ L ω *  ω =
              c *
                  (L ω ^
                      (Module.finrank  E -
                        k)) *
                Ff (L ω))
      (hFfm :
        MeasureTheory.StronglyMeasurable Ff)
      (hF :
        MeasureTheory.Integrable
          (fun ξ 
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E),
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x) =
          ((2 * Real.pi) ^
                Module.finrank  E) *
            f x) :
      (MeasureTheory.volume.toSphere.real
              Set.univ) *
          LeanRidgelet.stiefelFourierExpression
            (ContinuousLinearMap.stiefelMeasure
              L₀)
             Γ x =
        c *
              (MeasureTheory.volume.toSphere.real
                  Set.univ) *
            (2 * Real.pi) ^
              (Module.finrank  E - k) *
          f x
    **The reconstruction formula of the Fourier slice method over the Stiefel manifold.** 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ω)|Uω|^{d}`,
    `d = m - k` — 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,k} (2π)^{d}`, with
    `c_{m,k} = |𝕊^{k-1}|/|𝕊^{m-1}|` for the probability normalization of the invariant measure used
    here.
    
    The proof is the codimension-one one with the sphere replaced by the Stiefel manifold: the frame
    integral is evaluated by the matrix polar integration formula, and the remaining Euclidean integral
    by the inversion formula. The three integrability hypotheses are the ones the matrix polar formula
    carries, which is the article's standing assumption of Section 2. 
  • complete
    theorem LeanRidgelet.fs_ae_ne_zero_frame {k : }
      [Nontrivial (EuclideanSpace  (Fin k))] :
      ∀ᵐ (ω : EuclideanSpace  (Fin k)), ω  0
    theorem LeanRidgelet.fs_ae_ne_zero_frame {k : }
      [Nontrivial
          (EuclideanSpace  (Fin k))] :
      ∀ᵐ (ω : EuclideanSpace  (Fin k)), ω  0
    Over the frame space the singular frequency is negligible, as it is over `ℝ`. 
  • complete
    theorem LeanRidgelet.fs_angularFourier_slice_dPlaneTransform.{u_1} {k : }
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] {f : E  }
      (hf : MeasureTheory.Integrable f MeasureTheory.volume)
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (ω : EuclideanSpace  (Fin k)) :
      LeanRidgelet.Fourier.angularFourierIntegralInner
          (MeasureTheory.dPlaneTransform f L) ω =
        LeanRidgelet.Fourier.angularFourierIntegralInner f (L ω)
    theorem LeanRidgelet.fs_angularFourier_slice_dPlaneTransform.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      {f : E  }
      (hf :
        MeasureTheory.Integrable f
          MeasureTheory.volume)
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (ω : EuclideanSpace  (Fin k)) :
      LeanRidgelet.Fourier.angularFourierIntegralInner
          (MeasureTheory.dPlaneTransform f L)
          ω =
        LeanRidgelet.Fourier.angularFourierIntegralInner
          f (L ω)
    **The Fourier slice theorem in the article's angular convention**, in general codimension: the
    bias spectrum of the `d`-plane transform of `f` along a frame is the angular Fourier data of `f` on
    the range of that frame. Rescaling the frequency does not disturb the slice theorem. 
  • complete
    theorem LeanRidgelet.fs_angularFourier_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),
          LeanRidgelet.Fourier.angularFourierIntegralInner g ξ =
            (ξ ^ s) *
              LeanRidgelet.Fourier.angularFourierIntegralInner f ξ)
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (ω : EuclideanSpace  (Fin k)) :
      LeanRidgelet.Fourier.angularFourierIntegralInner
          (MeasureTheory.dPlaneTransform g L) ω =
        (ω ^ s) *
          LeanRidgelet.Fourier.angularFourierIntegralInner f (L ω)
    theorem LeanRidgelet.fs_angularFourier_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),
          LeanRidgelet.Fourier.angularFourierIntegralInner
              g ξ =
            (ξ ^ s) *
              LeanRidgelet.Fourier.angularFourierIntegralInner
                f ξ)
      (L : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (ω : EuclideanSpace  (Fin k)) :
      LeanRidgelet.Fourier.angularFourierIntegralInner
          (MeasureTheory.dPlaneTransform g L)
          ω =
        (ω ^ s) *
          LeanRidgelet.Fourier.angularFourierIntegralInner
            f (L ω)
    **The coefficient function is the `d`-plane transform of a fractional derivative**, in the
    convention the reconstruction formula is stated in. 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 the frame.
    
    This is the angular-convention counterpart of `fs_fourier_dPlaneTransform_fractional`. The two
    conventions do not agree here: a multiplier `‖ξ‖^s` becomes `(2π)^s ‖ξ‖^s` under the rescaling of
    the frequency, so the reconstruction formula needs this form and not that one. The fractional
    Laplacian
    is not in Mathlib, so its multiplier property is the hypothesis rather than a definition. 
  • complete
    theorem LeanRidgelet.fs_stiefel_reconstruction.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E) (t : )
      (σ : EuclideanSpace  (Fin k)  ) (f g : E  ) (x : E)
      (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 :
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner g ξ =
            (ξ ^ ((Module.finrank  E - k) - t)) *
              LeanRidgelet.Fourier.angularFourierIntegralInner f ξ)
      (hbias :
         (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
           (b : EuclideanSpace  (Fin k)),
              MeasureTheory.dPlaneTransform g L b *
                σ (LeanRidgelet.dPlaneCoord L x - b) =
            ((2 * Real.pi) ^ k)⁻¹ *
               (ω : EuclideanSpace  (Fin k)),
                LeanRidgelet.Fourier.angularFourierIntegralInner
                      (MeasureTheory.dPlaneTransform g L) ω *
                    (ω ^ t) *
                  LeanRidgelet.fourierSlicePhase
                    (inner  ω (LeanRidgelet.dPlaneCoord L x))) :
      (MeasureTheory.volume.toSphere.real Set.univ) *
          LeanRidgelet.stiefelSynthesis
            (ContinuousLinearMap.stiefelMeasure L₀) σ
            (fun L  MeasureTheory.dPlaneTransform g L) x =
        (MeasureTheory.volume.toSphere.real Set.univ) *
            (2 * Real.pi) ^ (Module.finrank  E - k) *
          f x
    theorem LeanRidgelet.fs_stiefel_reconstruction.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (t : )
      (σ : EuclideanSpace  (Fin k)  )
      (f g : E  ) (x : E)
      (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 :
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner
              g ξ =
            (ξ ^
                  ((Module.finrank  E - k) -
                    t)) *
              LeanRidgelet.Fourier.angularFourierIntegralInner
                f ξ)
      (hbias :
        
          (L :
            EuclideanSpace  (Fin k) →ₗᵢ[]
              E),
           (b : EuclideanSpace  (Fin k)),
              MeasureTheory.dPlaneTransform g
                  L b *
                σ
                  (LeanRidgelet.dPlaneCoord L
                      x -
                    b) =
            ((2 * Real.pi) ^ k)⁻¹ *
               (ω :
                EuclideanSpace  (Fin k)),
                LeanRidgelet.Fourier.angularFourierIntegralInner
                      (MeasureTheory.dPlaneTransform
                        g L)
                      ω *
                    (ω ^ t) *
                  LeanRidgelet.fourierSlicePhase
                    (inner  ω
                      (LeanRidgelet.dPlaneCoord
                        L x))) :
      (MeasureTheory.volume.toSphere.real
              Set.univ) *
          LeanRidgelet.stiefelSynthesis
            (ContinuousLinearMap.stiefelMeasure
              L₀)
            σ
            (fun L 
              MeasureTheory.dPlaneTransform g
                L)
            x =
        (MeasureTheory.volume.toSphere.real
                Set.univ) *
            (2 * Real.pi) ^
              (Module.finrank  E - k) *
          f x
    **The reconstruction formula over the Stiefel manifold in general codimension** — the article's
    `thm:stiefel`. The activation has spectrum `σ♯(ω) = ‖ω‖^t`, and the coefficient function is the
    `d`-plane transform of the fractional derivative `g = △^{(d-t)/2} f` of the target, `d = m - k`:
    this is the article's `R[f](U,b) = P_d[△^{(d-t)/2}f](U,b)`, whose bias spectrum
    `fs_angularFourier_dPlaneTransform_fractional` computes. The conclusion is
    `S[R[f]](x) = c_{m,k} (2π)^{d} f(x)`.
    
    *The constant is the reciprocal of the article's, and the value of `c_{m,k}` differs*; see the
    *Deviations from the article* section of this module. Here `c_{m,k} = |𝕊^{k-1}|/|𝕊^{m-1}|`, the
    invariant measure on the Stiefel manifold being a probability measure, and the statement is written
    multiplied out so that no division appears. 
  • complete
    theorem LeanRidgelet.fs_stiefelSynthesis_codimOne {m : }
      [Nontrivial (LeanRidgelet.InputSpace m)]
      (L₀ : EuclideanSpace  (Fin 1) →ₗᵢ[] LeanRidgelet.InputSpace m)
      (σ :   ) (γ : (Metric.sphere 0 1)    )
      (x : LeanRidgelet.InputSpace m) :
      LeanRidgelet.stiefelSynthesis (ContinuousLinearMap.stiefelMeasure L₀)
          (fun b  σ (b.ofLp 0))
          (fun L b 
            γ
              (MeasureTheory.frameDirection L
                MeasureTheory.unitVectorFinOne)
              (b.ofLp 0))
          x =
        (MeasureTheory.volume.toSphere.real Set.univ)⁻¹ 
          LeanRidgelet.sphereSynthesis σ γ x
    theorem LeanRidgelet.fs_stiefelSynthesis_codimOne
      {m : }
      [Nontrivial (LeanRidgelet.InputSpace m)]
      (L₀ :
        EuclideanSpace  (Fin 1) →ₗᵢ[]
          LeanRidgelet.InputSpace m)
      (σ :   )
      (γ : (Metric.sphere 0 1)    )
      (x : LeanRidgelet.InputSpace m) :
      LeanRidgelet.stiefelSynthesis
          (ContinuousLinearMap.stiefelMeasure
            L₀)
          (fun b  σ (b.ofLp 0))
          (fun L b 
            γ
              (MeasureTheory.frameDirection L
                MeasureTheory.unitVectorFinOne)
              (b.ofLp 0))
          x =
        (MeasureTheory.volume.toSphere.real
              Set.univ)⁻¹ 
          LeanRidgelet.sphereSynthesis σ γ x
    **The general-codimension layer is the codimension-one layer at `k = 1`.** The frame is its unit
    vector, the bias `b : ℝ^1` is the scalar `b 0`, and the frame coordinate is the inner product with
    the unit vector, by `inner_dPlaneCoord`. The scalar is the total mass of the surface measure because
    `stiefelMeasure` is normalized to a probability measure and `Measure.toSphere` is not. 

The constant is c_{m,k}(2\pi)^d, the reciprocal of the one in the article, and the value of c_{m,k} differs as well: the invariant measure used here is a probability measure, so it comes out as |\mathbb S^{k-1}|/|\mathbb S^{m-1}|, which in the classical normalization reads |\mathbb S^{k-1}|\cdot\sigma_{m-1,k-1} — the article's c_{m,k} with frames of the orthogonal complement of the direction rather than of the whole space. The article's inversion formula for the d-plane transform likewise omits a factor c_{m,k}. The article's own form of the theorem — activation spectrum |\boldsymbol\omega|^t, coefficient function R[f](U,\boldsymbol b)=\triangle_{\boldsymbol b}^{(d-t)/2}P_d[f](U,\boldsymbol b) — is the specialization at c=1, and the bias spectrum of that coefficient function is computed by the Fourier slice theorem in the angular convention together with the multiplier hypothesis standing in for the fractional Laplacian. Note that the two Fourier conventions genuinely differ here: a multiplier \|\xi\|^s in the Mathlib convention is (2\pi)^s\|\xi\|^s in the angular one, so the reconstruction formula needs the angular form and not the one recorded in fs_dplane_fractional.

The article's standing absolute-convergence assumption is not needed: the two hypotheses the matrix polar formula carries are discharged in mathlib_matrix_polar for a strongly measurable integrand, so the master identity asks for that instead, and the article's own form of the theorem asks for nothing beyond integrability of the target and of its Fourier transform — the Fourier transform of an integrable function being continuous, hence measurable.

That the general codimension really does specialize to codimension one is a theorem here and not a remark: at k=1 the two layers agree up to the total mass of the surface measure, the invariant measure on the Stiefel manifold being normalized to a probability measure and Mathlib's surface measure not. The two parameter spaces are identified by mathlib_stiefel_codim_one, the two bias spaces by the coordinate of \mathbb R^1, and the frame coordinate by the transpose identity above.

Theorem3.1.22
Statement uses 3
Statement dependency previews
Preview
Definition 3.1.16
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Reconstruction on the similitude group (Theorem 6.2). With the weight matrix restricted to A=aU and the parameter measure a^{m-s-1}\,\mathrm da\,\mathrm dU, the ridgelet transform is R_s[f;\rho](aU,\boldsymbol b)=a^{m-s-1}\int\triangle^{s/2}[f]\overline{\rho(A^\top\boldsymbol x-\boldsymbol b)} for any real s. This extends the d-plane ridgelet transforms of Donoho and of Rubin. Formalized for an arbitrary real s.

Lean code for Theorem3.1.226 declarations
  • complete
    theorem LeanRidgelet.rpow_similitude_split {M s a r : } (ha : 0 < a)
      (hr : 0 < r) :
      a ^ (M - s - 1) * (a * r) ^ s = r ^ (-(M - s - 1)) * (a * r) ^ (M - 1)
    theorem LeanRidgelet.rpow_similitude_split
      {M s a r : } (ha : 0 < a)
      (hr : 0 < r) :
      a ^ (M - s - 1) * (a * r) ^ s =
        r ^ (-(M - s - 1)) * (a * r) ^ (M - 1)
    **The scale–frequency exponent identity of the similitude case.** At a positive scale and
    radius, the parameter density `a^{m-s-1}` and the ansatz factor `(a r)^s` combine, in the product
    variable `y = a r`, into the Jacobian `y^{m-1}` of polar coordinates on the input space, times a
    power of the radius alone. This is why the ansatz closes for every real `s`: the exponent `s`
    cancels out of the `y`-dependence. 
  • complete
    theorem LeanRidgelet.rpow_similitude_radial {kk M s r : } (hr : 0 < r) :
      r ^ (kk - 1) * r ^ (-(M - s - 1)) * r⁻¹ = r ^ (s - M + kk - 1)
    theorem LeanRidgelet.rpow_similitude_radial
      {kk M s r : } (hr : 0 < r) :
      r ^ (kk - 1) * r ^ (-(M - s - 1)) *
          r⁻¹ =
        r ^ (s - M + kk - 1)
    **The radial weight the similitude case leaves behind.** The Jacobian `r^{k-1}` of polar
    coordinates on the frequency space, the factor `r^{-(m-s-1)}` left by the scale density, and the
    Jacobian `r⁻¹` of the substitution `y = a r` combine into `r^{s-m+k-1} = r^{-(d-s+1)}`, `d = m - k`.
    That is the weight the article's scalar `⦅σ,ρ⦆_s` integrates the two spectra against. 
  • def LeanRidgelet.similitudeSynthesis.{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.similitudeSynthesis.{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, (∫ a in Set.Ioi (0 : ℝ), ((α a : ℝ) : ℂ) *
        ∫ b : EuclideanSpace ℝ (Fin k), γ a L b * σ (a • dPlaneCoord L x - b)) ∂ν
    The `d`-plane layer over the similitude group,
    `S[γ](x) = ∫ γ(a,U,b) σ(a Uᵀx - b) α(a) da dU db`. 
  • def LeanRidgelet.similitudeFourierExpression.{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.similitudeFourierExpression.{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 :=
    :=
      ((2 * (Real.pi : ℂ)) ^ k)⁻¹ *
        ∫ L, (∫ ω : EuclideanSpace ℝ (Fin k), ∫ a in Set.Ioi (0 : ℝ), ((α a : ℝ) : ℂ) *
          (Γ a L ω * Fσ ω * fourierSlicePhase (inner ℝ ω (a • dPlaneCoord L x)))) ∂ν
    The Fourier expression of the similitude layer, the output of Step 1. The bias frequency sits
    outside the scale integral, which is where the derivation needs it, and moving it there is the
    article's standing assumption on exchanging the order of integration. 
  • complete
    theorem LeanRidgelet.fs_similitude_fourierExpression_of_bias.{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)
      (hbias :
         (a : ),
          0 < a 
             (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
               (b : EuclideanSpace  (Fin k)),
                  γ a L b * σ (a  LeanRidgelet.dPlaneCoord L x - b) =
                ((2 * Real.pi) ^ k)⁻¹ *
                   (ω : EuclideanSpace  (Fin k)),
                    Γ a L ω *  ω *
                      LeanRidgelet.fourierSlicePhase
                        (inner  ω (a  LeanRidgelet.dPlaneCoord L x)))
      (hswap :
         (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
          MeasureTheory.Integrable
            (fun p 
              (α p.1) *
                (Γ p.1 L p.2 *  p.2 *
                  LeanRidgelet.fourierSlicePhase
                    (inner  p.2 (p.1  LeanRidgelet.dPlaneCoord L x))))
            ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod
              MeasureTheory.volume)) :
      LeanRidgelet.similitudeSynthesis ν α σ γ x =
        LeanRidgelet.similitudeFourierExpression ν α  Γ x
    theorem LeanRidgelet.fs_similitude_fourierExpression_of_bias.{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)
      (hbias :
         (a : ),
          0 < a 
            
              (L :
                EuclideanSpace 
                    (Fin k) →ₗᵢ[]
                  E),
               (b :
                  EuclideanSpace  (Fin k)),
                  γ a L b *
                    σ
                      (a 
                          LeanRidgelet.dPlaneCoord
                            L x -
                        b) =
                ((2 * Real.pi) ^ k)⁻¹ *
                   (ω :
                    EuclideanSpace  (Fin k)),
                    Γ a L ω *  ω *
                      LeanRidgelet.fourierSlicePhase
                        (inner  ω
                          (a 
                            LeanRidgelet.dPlaneCoord
                              L x)))
      (hswap :
        
          (L :
            EuclideanSpace  (Fin k) →ₗᵢ[]
              E),
          MeasureTheory.Integrable
            (fun p 
              (α p.1) *
                (Γ p.1 L p.2 *  p.2 *
                  LeanRidgelet.fourierSlicePhase
                    (inner  p.2
                      (p.1 
                        LeanRidgelet.dPlaneCoord
                          L x))))
            ((MeasureTheory.volume.restrict
                  (Set.Ioi 0)).prod
              MeasureTheory.volume)) :
      LeanRidgelet.similitudeSynthesis ν α σ γ
          x =
        LeanRidgelet.similitudeFourierExpression
          ν α  Γ x
    **Step 1 over the similitude group**: the layer equals its Fourier expression. The analytic
    input is the `k`-dimensional bias identity at each scale and frame, and — unlike the Stiefel case —
    one Fubini exchange, moving the bias frequency outside the scale integral. That exchange is the
    article's standing assumption that the iterated integral converges absolutely. 
  • complete
    theorem LeanRidgelet.fs_similitude_reconstruction_of_inversion.{u_1} {k : }
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E] [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E) (s : ) (cphi : )
      ( Fρbar : EuclideanSpace  (Fin k)  ) (Ff f : E  ) (x : E)
      (hradial :
         (v : (Metric.sphere 0 1)),
           (r : ) in Set.Ioi 0,
              (r ^ (s - (Module.finrank  E) + k - 1)) *
                ( (r  v) * Fρbar (r  v)) =
            cphi)
      (hpolar :
         (L : EuclideanSpace  (Fin k) →ₗᵢ[] E),
          MeasureTheory.Integrable
            (fun ω 
               (a : ) in Set.Ioi 0,
                (a ^ ((Module.finrank  E) - s - 1)) *
                  (Ff (a  L ω) * ((a * ω) ^ s) * Fρbar ω *  ω *
                    LeanRidgelet.fourierSlicePhase
                      (inner  ω (a  LeanRidgelet.dPlaneCoord L x))))
            MeasureTheory.volume)
      (hFfm : MeasureTheory.StronglyMeasurable Ff)
      (hF :
        MeasureTheory.Integrable
          (fun ξ  Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E), Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x) =
          ((2 * Real.pi) ^ Module.finrank  E) * f x) :
      (MeasureTheory.volume.toSphere.real Set.univ) *
          LeanRidgelet.similitudeFourierExpression
            (ContinuousLinearMap.stiefelMeasure L₀)
            (fun a  a ^ ((Module.finrank  E) - s - 1)) 
            (fun a L ω  Ff (a  L ω) * ((a * ω) ^ s) * Fρbar ω) x =
        cphi * (MeasureTheory.volume.toSphere.real Set.univ) *
            (2 * Real.pi) ^ (Module.finrank  E - k) *
          f x
    theorem LeanRidgelet.fs_similitude_reconstruction_of_inversion.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (s : ) (cphi : )
      ( Fρbar :
        EuclideanSpace  (Fin k)  )
      (Ff f : E  ) (x : E)
      (hradial :
         (v : (Metric.sphere 0 1)),
           (r : ) in Set.Ioi 0,
              (r ^
                    (s -
                          (Module.finrank 
                              E) +
                        k -
                      1)) *
                ( (r  v) *
                  Fρbar (r  v)) =
            cphi)
      (hpolar :
        
          (L :
            EuclideanSpace  (Fin k) →ₗᵢ[]
              E),
          MeasureTheory.Integrable
            (fun ω 
               (a : ) in Set.Ioi 0,
                (a ^
                      ((Module.finrank  E) -
                          s -
                        1)) *
                  (Ff (a  L ω) *
                          ((a * ω) ^ s) *
                        Fρbar ω *
                       ω *
                    LeanRidgelet.fourierSlicePhase
                      (inner  ω
                        (a 
                          LeanRidgelet.dPlaneCoord
                            L x))))
            MeasureTheory.volume)
      (hFfm :
        MeasureTheory.StronglyMeasurable Ff)
      (hF :
        MeasureTheory.Integrable
          (fun ξ 
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E),
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x) =
          ((2 * Real.pi) ^
                Module.finrank  E) *
            f x) :
      (MeasureTheory.volume.toSphere.real
              Set.univ) *
          LeanRidgelet.similitudeFourierExpression
            (ContinuousLinearMap.stiefelMeasure
              L₀)
            (fun a 
              a ^
                ((Module.finrank  E) - s -
                  1))
            
            (fun a L ω 
              Ff (a  L ω) *
                  ((a * ω) ^ s) *
                Fρbar ω)
            x =
        cphi *
              (MeasureTheory.volume.toSphere.real
                  Set.univ) *
            (2 * Real.pi) ^
              (Module.finrank  E - k) *
          f x
    **The reconstruction formula over the similitude group** — the article's `thm:similitude`. The
    separation-of-variables ansatz is `γ♯(aU,ω) = f̂(aUω)(a‖ω‖)^s conj(ρ♯(ω))` with parameter density
    `α(a) = a^{m-s-1}`, for an arbitrary real `s`. What has to be constant is not the product of the two
    spectra, as in the Stiefel case, but its *radial* integral against `r^{-(d-s+1)}`; that is the
    hypothesis `hradial`, and the constant is the article's `⦅σ,ρ⦆_s` up to normalization.
    
    The scale and the radial variable of the bias frequency couple through `y = a r`. After polar
    coordinates in the frequency, the substitution `y = a r` turns `a^{m-s-1}(ar)^s` into `y^{m-1}`, the
    Jacobian of polar coordinates on the input space, and leaves behind exactly the radial weight
    `r^{-(d-s+1)}` — these are `rpow_similitude_split` and `rpow_similitude_radial`. What is left is the
    direction average, so the conclusion has the same shape as the Stiefel one with the radial constant
    in place of the auxiliary factor. 

Unlike the Stiefel case this one has a scale, and the scale is not a passenger: it couples to the radial variable of the bias frequency through y=ar. In particular the similitude network is not a scale mixture of Stiefel networks — at a fixed scale no power of \sigma^\sharp\overline{\rho^\sharp} satisfies the Stiefel separation-of-variables condition, and that coupling is the substance of this case. The derivation is polar coordinates in the bias frequency, the one-dimensional substitution y=ar in the scale, and then the direction average, whose weight y^{m-1} is exactly what the substitution produces; the Fubini exchange that moves the bias frequency outside the scale integral goes into Step 1, where the article puts it.

The two exponent identities are what make the substitution come out: a^{m-s-1}(ar)^s=r^{-(m-s-1)}(ar)^{m-1}, so that the exponent s cancels out of the y-dependence, and r^{k-1}\cdot r^{-(m-s-1)}\cdot r^{-1}=r^{-(d-s+1)}, which is the weight the article's scalar (\!(\sigma,\rho)\!)_s integrates the two spectra against. That scalar is written in the article's theorem statement as an integral over \mathbb R^k, but what the derivation produces — and what is proved here — is the radial integral \int_{\mathbb S^{k-1}}\int_{r>0}r^{-(d-s+1)}\sigma^\sharp(rv)\overline{\rho^\sharp(rv)}\,\mathrm dr\,\mathrm dv, the same expression without the Jacobian r^{k-1} of polar coordinates. The article's own appendix writes the constant as a radial integral at the point where it is produced, so the \mathbb R^k form of the statement is where the Jacobian slips in; the two agree at k=1.

Theorem3.1.23
Statement uses 5
Statement dependency previews
Preview
Definition 3.1.16
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1L∃∀N

Reconstruction on the full-column-rank matrices (Theorem 6.1). The densest of the three solutions, over all injective weight matrices, with the singular-value density \delta(A) in the ridgelet transform. The derivation runs through the singular value decomposition A=UDV^\top: the frame U is a point of the Stiefel manifold, V a rotation of the frequency space, and D the k singular values, which act on a frequency coordinatewise. Formalized in those coordinates. In the article's statement the first product in \delta(A) runs to d; it runs to k, the number of singular values, as in the article's own appendix.

Lean code for Theorem3.1.2310 declarations
  • complete
    def LeanRidgelet.svdDiag {k : } (d ω : EuclideanSpace  (Fin k)) :
      EuclideanSpace  (Fin k)
    def LeanRidgelet.svdDiag {k : }
      (d ω : EuclideanSpace  (Fin k)) :
      EuclideanSpace  (Fin k)
    Implementation after :=
    :=
      MeasureTheory.diagScale (WithLp.ofLp d) ω
    The diagonal factor of a singular value decomposition, acting on a vector of the frequency space
    coordinatewise: `(D ω)ᵢ = dᵢ ωᵢ`. 
  • complete
    theorem LeanRidgelet.svdDiag_apply {k : } (d ω : EuclideanSpace  (Fin k))
      (i : Fin k) : (LeanRidgelet.svdDiag d ω).ofLp i = d.ofLp i * ω.ofLp i
    theorem LeanRidgelet.svdDiag_apply {k : }
      (d ω : EuclideanSpace  (Fin k))
      (i : Fin k) :
      (LeanRidgelet.svdDiag d ω).ofLp i =
        d.ofLp i * ω.ofLp i
  • complete
    theorem LeanRidgelet.svdDiag_comm {k : } (d ω : EuclideanSpace  (Fin k)) :
      LeanRidgelet.svdDiag d ω = LeanRidgelet.svdDiag ω d
    theorem LeanRidgelet.svdDiag_comm {k : }
      (d ω : EuclideanSpace  (Fin k)) :
      LeanRidgelet.svdDiag d ω =
        LeanRidgelet.svdDiag ω d
    The diagonal action is symmetric in its two arguments, both being coordinatewise
    multiplication. 
  • complete
    theorem LeanRidgelet.inner_svdDiag {k : } (d a b : EuclideanSpace  (Fin k)) :
      inner  a (LeanRidgelet.svdDiag d b) =
        inner  (LeanRidgelet.svdDiag d a) b
    theorem LeanRidgelet.inner_svdDiag {k : }
      (d a b : EuclideanSpace  (Fin k)) :
      inner  a (LeanRidgelet.svdDiag d b) =
        inner  (LeanRidgelet.svdDiag d a) b
    A diagonal matrix is symmetric. 
  • complete
    theorem LeanRidgelet.fs_ae_forall_coord_ne_zero {k : } :
      ∀ᵐ (ω : EuclideanSpace  (Fin k)),  (i : Fin k), ω.ofLp i  0
    theorem LeanRidgelet.fs_ae_forall_coord_ne_zero
      {k : } :
      ∀ᵐ (ω : EuclideanSpace  (Fin k)),
         (i : Fin k), ω.ofLp i  0
    **The coordinate hyperplanes are null.** Almost every frequency has all coordinates nonzero,
    which is what the coordinatewise change of variables of the affine case needs. 
  • complete
    def LeanRidgelet.affineSynthesis.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E]
      (ν : MeasureTheory.Measure (EuclideanSpace  (Fin k) →ₗᵢ[] E))
      (w : EuclideanSpace  (Fin k)  ) (σ : EuclideanSpace  (Fin k)  )
      (γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace  (Fin k) →L[]
                    EuclideanSpace  (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (x : E) : 
    def LeanRidgelet.affineSynthesis.{u_1} {k : }
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (ν :
        MeasureTheory.Measure
          (EuclideanSpace  (Fin k) →ₗᵢ[] E))
      (w : EuclideanSpace  (Fin k)  )
      (σ : EuclideanSpace  (Fin k)  )
      (γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace 
                      (Fin k) →L[]
                    EuclideanSpace 
                      (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (x : E) : 
    Implementation after :=
    :=
      ∫ U, (∫ V, (∫ d : EuclideanSpace ℝ (Fin k), ((w d : ℝ) : ℂ) *
          ∫ b : EuclideanSpace ℝ (Fin k), γ U d V b *
            σ (Unitary.linearIsometryEquiv V (svdDiag d (dPlaneCoord U x)) - b))
        ∂ContinuousLinearMap.orthogonalHaar) ∂ν
    The `d`-plane layer over all full-column-rank matrices, in the singular value coordinates
    `A = U D Vᵀ`:
    `S[γ](x) = ∫ w(D) γ(U,D,V,b) σ(V D Uᵀ x - b) dD dV dU db`.
    The weight `w` stands for the Jacobian `δ` of the singular value decomposition, which is left as a
    parameter because Lemma C.3 is not formalized. 
  • complete
    def LeanRidgelet.affineFourierExpression.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E]
      (ν : MeasureTheory.Measure (EuclideanSpace  (Fin k) →ₗᵢ[] E))
      (w : EuclideanSpace  (Fin k)  ) ( : EuclideanSpace  (Fin k)  )
      (Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace  (Fin k) →L[]
                    EuclideanSpace  (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (x : E) : 
    def LeanRidgelet.affineFourierExpression.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (ν :
        MeasureTheory.Measure
          (EuclideanSpace  (Fin k) →ₗᵢ[] E))
      (w : EuclideanSpace  (Fin k)  )
      ( : EuclideanSpace  (Fin k)  )
      (Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace 
                      (Fin k) →L[]
                    EuclideanSpace 
                      (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (x : E) : 
    Implementation after :=
    :=
      ((2 * (Real.pi : ℂ)) ^ k)⁻¹ *
        ∫ U, (∫ V, (∫ ω : EuclideanSpace ℝ (Fin k), ∫ d : EuclideanSpace ℝ (Fin k),
            ((w d : ℝ) : ℂ) * (Γ U d V ω * Fσ ω *
              fourierSlicePhase (inner ℝ ω
                (Unitary.linearIsometryEquiv V (svdDiag d (dPlaneCoord U x))))))
          ∂ContinuousLinearMap.orthogonalHaar) ∂ν
    The Fourier expression of the affine layer, the output of Step 1. The bias frequency sits
    outside the singular value integral, which is where the derivation needs it. 
  • complete
    theorem LeanRidgelet.fs_affine_fourierExpression_of_bias.{u_1} {k : }
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      (ν : MeasureTheory.Measure (EuclideanSpace  (Fin k) →ₗᵢ[] E))
      (w : EuclideanSpace  (Fin k)  )
      (σ  : EuclideanSpace  (Fin k)  )
      (γ Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace  (Fin k) →L[]
                    EuclideanSpace  (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (x : E)
      (hbias :
         (U : EuclideanSpace  (Fin k) →ₗᵢ[] E)
          (d : EuclideanSpace  (Fin k))
          (V :
            (unitary
                (EuclideanSpace  (Fin k) →L[] EuclideanSpace  (Fin k)))),
           (b : EuclideanSpace  (Fin k)),
              γ U d V b *
                σ
                  ((Unitary.linearIsometryEquiv V)
                      (LeanRidgelet.svdDiag d
                        (LeanRidgelet.dPlaneCoord U x)) -
                    b) =
            ((2 * Real.pi) ^ k)⁻¹ *
               (ω : EuclideanSpace  (Fin k)),
                Γ U d V ω *  ω *
                  LeanRidgelet.fourierSlicePhase
                    (inner  ω
                      ((Unitary.linearIsometryEquiv V)
                        (LeanRidgelet.svdDiag d
                          (LeanRidgelet.dPlaneCoord U x)))))
      (hswap :
         (U : EuclideanSpace  (Fin k) →ₗᵢ[] E)
          (V :
            (unitary
                (EuclideanSpace  (Fin k) →L[] EuclideanSpace  (Fin k)))),
          MeasureTheory.Integrable
            (fun p 
              (w p.1) *
                (Γ U p.1 V p.2 *  p.2 *
                  LeanRidgelet.fourierSlicePhase
                    (inner  p.2
                      ((Unitary.linearIsometryEquiv V)
                        (LeanRidgelet.svdDiag p.1
                          (LeanRidgelet.dPlaneCoord U x))))))
            (MeasureTheory.volume.prod MeasureTheory.volume)) :
      LeanRidgelet.affineSynthesis ν w σ γ x =
        LeanRidgelet.affineFourierExpression ν w  Γ x
    theorem LeanRidgelet.fs_affine_fourierExpression_of_bias.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      (ν :
        MeasureTheory.Measure
          (EuclideanSpace  (Fin k) →ₗᵢ[] E))
      (w : EuclideanSpace  (Fin k)  )
      (σ  : EuclideanSpace  (Fin k)  )
      (γ Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace 
                      (Fin k) →L[]
                    EuclideanSpace 
                      (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (x : E)
      (hbias :
        
          (U :
            EuclideanSpace  (Fin k) →ₗᵢ[] E)
          (d : EuclideanSpace  (Fin k))
          (V :
            (unitary
                (EuclideanSpace 
                    (Fin k) →L[]
                  EuclideanSpace  (Fin k)))),
           (b : EuclideanSpace  (Fin k)),
              γ U d V b *
                σ
                  ((Unitary.linearIsometryEquiv
                        V)
                      (LeanRidgelet.svdDiag d
                        (LeanRidgelet.dPlaneCoord
                          U x)) -
                    b) =
            ((2 * Real.pi) ^ k)⁻¹ *
               (ω :
                EuclideanSpace  (Fin k)),
                Γ U d V ω *  ω *
                  LeanRidgelet.fourierSlicePhase
                    (inner  ω
                      ((Unitary.linearIsometryEquiv
                          V)
                        (LeanRidgelet.svdDiag
                          d
                          (LeanRidgelet.dPlaneCoord
                            U x)))))
      (hswap :
        
          (U :
            EuclideanSpace  (Fin k) →ₗᵢ[] E)
          (V :
            (unitary
                (EuclideanSpace 
                    (Fin k) →L[]
                  EuclideanSpace  (Fin k)))),
          MeasureTheory.Integrable
            (fun p 
              (w p.1) *
                (Γ U p.1 V p.2 *  p.2 *
                  LeanRidgelet.fourierSlicePhase
                    (inner  p.2
                      ((Unitary.linearIsometryEquiv
                          V)
                        (LeanRidgelet.svdDiag
                          p.1
                          (LeanRidgelet.dPlaneCoord
                            U x))))))
            (MeasureTheory.volume.prod
              MeasureTheory.volume)) :
      LeanRidgelet.affineSynthesis ν w σ γ x =
        LeanRidgelet.affineFourierExpression ν
          w  Γ x
    **Step 1 over the full-column-rank matrices**: the layer equals its Fourier expression. As in
    the similitude case the analytic input is the `k`-dimensional bias identity at each matrix, together
    with one Fubini exchange moving the bias frequency outside the singular value integral. 
  • complete
    theorem LeanRidgelet.fs_affine_reconstruction_of_inversion.{u_1} {k : }
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E] [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E) (c cphi : )
      (w : EuclideanSpace  (Fin k)  ) ( : EuclideanSpace  (Fin k)  )
      (Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace  (Fin k) →L[]
                    EuclideanSpace  (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (Φ :
        (unitary
              (EuclideanSpace  (Fin k) →L[] EuclideanSpace  (Fin k))) 
          EuclideanSpace  (Fin k)  )
      (Ff f : E  ) (x : E) (hFfm : MeasureTheory.StronglyMeasurable Ff)
      (hansatz :
         (U : EuclideanSpace  (Fin k) →ₗᵢ[] E)
          (V :
            (unitary
                (EuclideanSpace  (Fin k) →L[] EuclideanSpace  (Fin k))))
          (ω : EuclideanSpace  (Fin k)),
          (∀ (i : Fin k), ω.ofLp i  0) 
             (d : EuclideanSpace  (Fin k)),
              (w d) *
                    (Γ U d V ((Unitary.linearIsometryEquiv V) ω) *
                       ((Unitary.linearIsometryEquiv V) ω)) *
                  (∏ i, |ω.ofLp i|)⁻¹ =
                c *
                      (U (LeanRidgelet.svdDiag ω d) ^
                          (Module.finrank  E -
                            Module.finrank  (EuclideanSpace  (Fin k)))) *
                    Ff (U (LeanRidgelet.svdDiag ω d)) *
                  Φ V ω)
      (hconst :
        
          (V :
            (unitary
                (EuclideanSpace  (Fin k) →L[] EuclideanSpace  (Fin k)))),
           (ω : EuclideanSpace  (Fin k)), Φ V ω = cphi)
      (hF :
        MeasureTheory.Integrable
          (fun ξ  Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E), Ff ξ * LeanRidgelet.fourierSlicePhase (inner  ξ x) =
          ((2 * Real.pi) ^ Module.finrank  E) * f x) :
      (MeasureTheory.volume.toSphere.real Set.univ) *
          LeanRidgelet.affineFourierExpression
            (ContinuousLinearMap.stiefelMeasure L₀) w  Γ x =
        c * cphi * (MeasureTheory.volume.toSphere.real Set.univ) *
            (2 * Real.pi) ^ (Module.finrank  E - k) *
          f x
    theorem LeanRidgelet.fs_affine_reconstruction_of_inversion.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      [Nontrivial E]
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] E)
      (c cphi : )
      (w : EuclideanSpace  (Fin k)  )
      ( : EuclideanSpace  (Fin k)  )
      (Γ :
        (EuclideanSpace  (Fin k) →ₗᵢ[] E) 
          EuclideanSpace  (Fin k) 
            (unitary
                  (EuclideanSpace 
                      (Fin k) →L[]
                    EuclideanSpace 
                      (Fin k))) 
              EuclideanSpace  (Fin k)  )
      (Φ :
        (unitary
              (EuclideanSpace  (Fin k) →L[]
                EuclideanSpace  (Fin k))) 
          EuclideanSpace  (Fin k)  )
      (Ff f : E  ) (x : E)
      (hFfm :
        MeasureTheory.StronglyMeasurable Ff)
      (hansatz :
        
          (U :
            EuclideanSpace  (Fin k) →ₗᵢ[] E)
          (V :
            (unitary
                (EuclideanSpace 
                    (Fin k) →L[]
                  EuclideanSpace  (Fin k))))
          (ω : EuclideanSpace  (Fin k)),
          (∀ (i : Fin k), ω.ofLp i  0) 
             (d : EuclideanSpace  (Fin k)),
              (w d) *
                    (Γ U d V
                        ((Unitary.linearIsometryEquiv
                            V)
                          ω) *
                      
                        ((Unitary.linearIsometryEquiv
                            V)
                          ω)) *
                  (∏ i, |ω.ofLp i|)⁻¹ =
                c *
                      (U
                              (LeanRidgelet.svdDiag
                                ω d) ^
                          (Module.finrank 
                              E -
                            Module.finrank 
                              (EuclideanSpace
                                 (Fin k)))) *
                    Ff
                      (U
                        (LeanRidgelet.svdDiag
                          ω d)) *
                  Φ V ω)
      (hconst :
        
          (V :
            (unitary
                (EuclideanSpace 
                    (Fin k) →L[]
                  EuclideanSpace  (Fin k)))),
           (ω : EuclideanSpace  (Fin k)),
              Φ V ω =
            cphi)
      (hF :
        MeasureTheory.Integrable
          (fun ξ 
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x))
          MeasureTheory.volume)
      (hinv :
         (ξ : E),
            Ff ξ *
              LeanRidgelet.fourierSlicePhase
                (inner  ξ x) =
          ((2 * Real.pi) ^
                Module.finrank  E) *
            f x) :
      (MeasureTheory.volume.toSphere.real
              Set.univ) *
          LeanRidgelet.affineFourierExpression
            (ContinuousLinearMap.stiefelMeasure
              L₀)
            w  Γ x =
        c * cphi *
              (MeasureTheory.volume.toSphere.real
                  Set.univ) *
            (2 * Real.pi) ^
              (Module.finrank  E - k) *
          f x
    **The reconstruction formula over all full-column-rank matrices** — the article's `thm:affine`,
    in the singular value coordinates. The separation-of-variables ansatz is the article's `eq:sov`:
    after the frequency has been rotated to `ω = V ω'`, the product of the weight, the Jacobian
    `∏ |ω'ᵢ|⁻¹` of the coordinatewise substitution, and the two spectra must be the Fourier data of the
    target along the frame times a factor `Φ` of the rotation and the rotated frequency alone. Then the
    `Φ`-integral is the article's scalar `⦅σ,ρ⦆` and the rest is the matrix polar integration formula.
    
    `hconst` asks the `Φ`-integral to be the same at every rotation. The article's own computation of
    `⦅σ,ρ⦆` needs exactly that: it drops `∫_{O(k)} dV` against the total mass `1`, which is legitimate
    only when the inner integral does not depend on `V`. With `Φ(V,ω') = σ♯(Vω') conj(ρ♯(Vω')) ∏|ω'ᵢ|⁻¹`
    that independence is not automatic — the coordinatewise weight is not rotation invariant — so it is
    a hypothesis here rather than a step of the proof.
    
    No convergence hypothesis is needed beyond integrability of the Fourier data: both changes of
    variables are along equivalences, and the two convergence hypotheses of the matrix polar formula are
    discharged from strong measurability. 
  • complete
    theorem LeanRidgelet.fs_exists_svd_frame.{u_1} {k : } {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      (A : EuclideanSpace  (Fin k) →ₗ[] E) (hA : Function.Injective A) :
       U d V,
        (∀ (i : Fin k), 0 < d.ofLp i) 
           (ω : EuclideanSpace  (Fin k)) (x : E),
            inner  ω
                ((Unitary.linearIsometryEquiv V)
                  (LeanRidgelet.svdDiag d (LeanRidgelet.dPlaneCoord U x))) =
              inner  (A ω) x
    theorem LeanRidgelet.fs_exists_svd_frame.{u_1}
      {k : } {E : Type u_1}
      [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      (A : EuclideanSpace  (Fin k) →ₗ[] E)
      (hA : Function.Injective A) :
       U d V,
        (∀ (i : Fin k), 0 < d.ofLp i) 
           (ω : EuclideanSpace  (Fin k))
            (x : E),
            inner  ω
                ((Unitary.linearIsometryEquiv
                    V)
                  (LeanRidgelet.svdDiag d
                    (LeanRidgelet.dPlaneCoord
                      U x))) =
              inner  (A ω) x
    **The singular value coordinates reach every full-column-rank weight.** For an injective
    `A : ℝ^k → E` there are a frame `U`, positive singular values `d` and a rotation `V` whose neuron
    has the same plane-wave frequency as `A` at every frequency and input,
    `⟪ω, V D Uᵀx⟫ = ⟪Aω, x⟫`. So the layer defined in the singular value coordinates has the same
    neurons as the article's layer over the full-column-rank matrices; what the unformalized Lemma C.3
    adds is the relation between the two parameter *measures*, not between the two families of
    neurons. 

The parametrization is part of the definition. The article's parameter measure is Lebesgue measure \mathrm dA on the matrix space, and converting it to the singular value coordinates is its Lemma C.3, the Jacobian \mathrm dA=\delta(D)\,\mathrm dD\,\mathrm dU\,\mathrm dV, whose published proof goes through exterior differential forms. Mathlib is far from it: it has singular values but not the decomposition, and neither the Jacobian of the matrix polar decomposition nor Weyl's integration formula for real symmetric matrices, which that Jacobian factors through. So the layer is defined in the singular value coordinates with the Jacobian left as a parameter.

That costs less than it appears to, for two reasons. The weight enters the separation-of-variables condition only as a factor of the coefficient function, and the article's coefficient function carries 1/\delta(A), so the two cancel and the reconstruction formula holds for every weight. And the two layers have the same neurons: the decomposition itself, as opposed to its Jacobian, is mathlib_svd, and it gives every injective weight matrix a set of singular value coordinates with the same plane-wave frequency. So the Jacobian is needed only to relate the two parameter measures — for the reading of the theorem, not for its proof.

What the derivation does need is two changes of variables and then the matrix polar integration formula, the same one the Stiefel case ends with. The frequency is rotated by V, which is an isometry hence measure preserving; the singular values are then traded for the rotated frequency coordinatewise, \boldsymbol y=D\boldsymbol\omega', whose Jacobian is \prod_i|\omega'_i| — that is mathlib_diagonal_scaling, and it is where the \prod_i|\omega_i|^{-1} of the article's scalar comes from, rather than a power of |\boldsymbol\omega|. After both, the parameter integral is the weighted frame section the matrix polar formula evaluates. So the affine case is the Stiefel case with two substitutions in front of it.

The comparison of scalars gives one more difference. The article's (\!(\sigma,\rho)\!) is \int_{\mathbb R^k}\sigma^\sharp\overline{\rho^\sharp}\prod_i|\omega_i|^{-1}, obtained from the derivation's \int_{O(k)}\int_{\mathbb R^k}\sigma^\sharp(V\boldsymbol\omega')\overline{\rho^\sharp(V\boldsymbol\omega')}\prod_i|\omega'_i|^{-1} by dropping \int_{O(k)}\mathrm dV against the total mass 1. That is legitimate only if the inner integral does not depend on V, and it does: substituting \boldsymbol\omega=V\boldsymbol\omega' turns the weight into \prod_i|(V^{-1}\boldsymbol\omega)_i|^{-1}, which is not rotation invariant, and whose average over O(k) diverges for k\geq2. So the printed scalar is the derivation's integrand at V=1 rather than its average. Here that independence is a hypothesis, which is exactly what the article's step needs; the derivation itself is proved without it. At k=1 the group is \{\pm1\} and the two agree.

Three deviations from the article are recorded in Section 6. The constant of the Stiefel reconstruction formula is the reciprocal of the article's: the coefficient function of the theorem has \rho^\sharp\equiv1, hence auxiliary factor \phi^\sharp\equiv1, whereas the quoted constant ((2\pi)^dc_{m,k})^{-1} is the one belonging to the normalization \phi^\sharp=c_{m,k}^{-1}(2\pi)^{-d} that makes the formula reproduce f exactly. The article's identification of the activation with the exponent t reads off the step function at t=-1, but the step function's spectrum is \pi\delta(\omega)+(i\omega)^{-1}, whose homogeneous part is -i\,\mathrm{sgn}(\omega)|\omega|^{-1} rather than |\omega|^{-1}. And the scalar of the affine formula is an O(k)-average, as above.

Section 7: the classical Radon formula

Theorem3.1.24
uses 1used by 0L∃∀N

The Fourier formula of Irie and Funahashi (Section 7). f(x)=((2\pi)^m\sigma^\sharp(1))^{-1}\int_{\mathbb R^m\times\mathbb R}\widehat f(a)\sigma(a\cdot x-b)e^{ib}\,\mathrm da\,\mathrm db. The Fourier slice method with the bias frequency pinned at 1 instead of integrated over, which is why it needs no admissibility condition on the activation: there is no |\omega|^{-m} to make integrable. One substitution does it — \int\sigma(a\cdot x-b)e^{ib}\,\mathrm db=e^{ia\cdot x}\sigma^\sharp(1) by b\mapsto a\cdot x-b — after which Fourier inversion finishes. Stated as an iterated integral, so there is no Fubini exchange either, and Fourier inversion at the point is the only hypothesis.

Lean code for Theorem3.1.241 theorem
  • complete
    theorem LeanRidgelet.fs_fourierFormula_irieFunahashi (m : ) (σ :   )
      (Ff f : LeanRidgelet.InputSpace m  ) (x : LeanRidgelet.InputSpace m)
      (hinv :
         (a : LeanRidgelet.InputSpace m),
            Ff a * LeanRidgelet.fourierSlicePhase (inner  a x) =
          ((2 * Real.pi) ^ m) * f x) :
       (a : LeanRidgelet.InputSpace m) (b : ),
          Ff a * σ (inner  a x - b) * LeanRidgelet.fourierSlicePhase b =
        LeanRidgelet.Fourier.angularFourierIntegralInner σ 1 *
            ((2 * Real.pi) ^ m) *
          f x
    theorem LeanRidgelet.fs_fourierFormula_irieFunahashi
      (m : ) (σ :   )
      (Ff f : LeanRidgelet.InputSpace m  )
      (x : LeanRidgelet.InputSpace m)
      (hinv :
         (a : LeanRidgelet.InputSpace m),
            Ff a *
              LeanRidgelet.fourierSlicePhase
                (inner  a x) =
          ((2 * Real.pi) ^ m) * f x) :
       (a : LeanRidgelet.InputSpace m) (b :
          ),
          Ff a * σ (inner  a x - b) *
            LeanRidgelet.fourierSlicePhase b =
        LeanRidgelet.Fourier.angularFourierIntegralInner
              σ 1 *
            ((2 * Real.pi) ^ m) *
          f x
    **The Fourier formula of Irie and Funahashi**, quoted in Section 7 of the article:
    `f(x) = ((2π)^m σ♯(1))^{-1} ∫_{ℝ^m×ℝ} f̂(a) σ(a·x - b) e^{ib} da db`.
    
    The statement is the iterated integral, and is multiplied out so that no division appears and no
    hypothesis `σ♯(1) ≠ 0` is needed. The only hypothesis is Fourier inversion at the point, the same
    one the abstract scheme asks for. There is no Fubini exchange and no absolute-convergence
    assumption: at a fixed weight the bias integral is `∫ σ(a·x - b)e^{ib} db = e^{i a·x} σ♯(1)` by the
    substitution `b ↦ a·x - b`, which leaves the weight integral to Fourier inversion. Nor is there an
    admissibility condition on `σ`, which is the difference from every other reconstruction formula
    here: the bias frequency is pinned rather than integrated, so there is no `|ω|^{-m}` to make
    integrable. 
Theorem3.1.25
uses 1used by 1L∃∀N

The Radon formula of Carroll--Dickinson and Ito (Theorem 7.2). f(\boldsymbol x)=\frac{1}{2(2\pi)^{m-1}}\int_{\mathbb S^{m-1}\times\mathbb R}\partial_b(-\triangle_b)^{(m-1)/2}P[f](\boldsymbol u,b)\,\sigma(\boldsymbol u\cdot\boldsymbol x-b), for \sigma the step function. This is an instance of the codimension-one master identity at the step function's actual spectrum (i\omega)^{-1}, whose coefficient function accordingly carries the multiplier i\omega|\omega|^{m-1} rather than |\omega|^m. Its constant (2(2\pi)^{m-1})^{-1} is the reciprocal of the one proved above, as it must be since the classical formula is solved for f, so this is an independent confirmation of the correction to the constant of the Stiefel formula.

Lean code for Theorem3.1.252 theorems
  • 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. 
  • 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)
      ( :
         (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)
      ( :
         (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. 
Theorem3.1.26
uses 1used by 0XL∃∀N

Rubin's continuous d-plane ridgelet transform (Theorem 7.3). Quoted by the article from the literature, with the remark that it is the case of fs_dplane_similitude in which both the activation and the ridgelet function are radial — the Euclidean distance from a point to a d-plane being |U^\top\boldsymbol x-\boldsymbol b|. Not stated in Lean: the normalization of the transform cannot be checked against its source, which is not among the reference texts of this project, and a sorry on a statement that cannot be checked is worth less than none.

What remains

Theorem3.1.27
Statement uses 2
Statement dependency previews
Preview
Theorem 3.1.21
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

The fractional derivative exists. Multiplying the Fourier transform of a Schwartz function by |\xi|^s again comes from a Schwartz function, provided that transform vanishes near the origin. This is the one hypothesis fs_dplane_stiefel still carries, and discharging it is what makes the article's own form of thm:stiefel unconditional.

Two ingredients are general. The angular Fourier transform is onto the Schwartz space, because Mathlib's is invertible there and the two conventions differ by a dilation, which the Schwartz space is invariant under; so it is enough to produce the intended transform. And |\xi|^s is smooth away from the origin, which is where the hypothesis on the transform's support does its work.

The band-limited case is proved outright. If the transform is in addition compactly supported — that is, if the target is band-limited to an annulus — the product is smooth by gluing, being smooth off the origin and identically zero on the ball, it inherits the compact support, and a smooth compactly supported function is Schwartz. No multiplier theory is needed.

The general case is proved too. What it needs is a function of temperate growth agreeing with |\xi|^s outside a ball, and the way to get one is to correct the multiplier inside the ball, where it is not needed: |\xi|^s itself is not of temperate growth — for non-even s it is not smooth at the origin, and for negative s not even bounded there — but (\|\xi\|^2+r^2\beta(\xi))^{s/2}, with \beta a bump equal to 1 near the origin and supported in the ball of radius r, is: the inner function is a norm square plus a smooth compactly supported function, hence temperate and bounded away from zero, and it equals \|\xi\|^2 outside the ball.

That last step is mathlib_temperate_growth_rpow, and it is where the Japanese bracket comes in. The bracket is not a substitute for |\xi|^s: (1+|\xi|^2)^{s/2} is the Bessel potential multiplier (1-\triangle)^{s/2} whereas |\xi|^s is the Riesz one (-\triangle)^{s/2}, and Section 6 needs the homogeneous one — the separation-of-variables condition asks the product \gamma^\sharp\sigma^\sharp to be \widehat f(U\boldsymbol\omega)|U\boldsymbol\omega|^d, and it is exactly that homogeneity which matches the weight |U\boldsymbol b|^{m-k} of the matrix polar formula. But Mathlib's temperate growth of the bracket is the right proof, because there the inner function already avoids the origin; generalizing it to an arbitrary inner function bounded away from zero is what lets the inner function be chosen as above.

Lean code for Theorem3.1.277 declarations
  • complete
    def LeanRidgelet.dilateCLE.{u_1} {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] {c : } (hc : c  0) : E ≃L[] E
    def LeanRidgelet.dilateCLE.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] {c : }
      (hc : c  0) : E ≃L[] E
    Implementation after :=
    :=
      { LinearEquiv.smulOfNeZero ℝ E c hc with
        continuous_toFun := continuous_const_smul c
        continuous_invFun := continuous_const_smul c⁻¹ }
    The dilation of `E` by a nonzero scalar, as a continuous linear equivalence. This is what
    carries the angular Fourier convention to Mathlib's: the two differ by the rescaling
    `ξ ↦ (2π)⁻¹ ξ`. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    complete
    theorem LeanRidgelet.fs_exists_angularFourier_eq.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (Ψ : SchwartzMap E ) :
       ψ,
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner (⇑ψ) ξ = Ψ ξ
    theorem LeanRidgelet.fs_exists_angularFourier_eq.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (Ψ : SchwartzMap E ) :
       ψ,
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner
              (⇑ψ) ξ =
            Ψ ξ
    **The angular Fourier transform is onto the Schwartz space.** Every Schwartz function is the
    angular Fourier transform of one, because Mathlib's transform is invertible there and the two
    conventions differ by a dilation, which the Schwartz space is invariant under. 
  • complete
    def LeanRidgelet.angularFourierSchwartz.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (φ : SchwartzMap E ) :
      SchwartzMap E 
    def LeanRidgelet.angularFourierSchwartz.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (φ : SchwartzMap E ) : SchwartzMap E 
    Implementation after :=
    :=
      SchwartzMap.compCLMOfContinuousLinearEquiv ℂ
        (dilateCLE (E := E) (c := (2 * Real.pi)⁻¹) (by positivity))
        (𝓕 φ)
    The angular Fourier transform of a Schwartz function, as a Schwartz function. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    complete
    theorem LeanRidgelet.contDiffAt_norm_rpow.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] (s : ) {ξ : E}
      ( : ξ  0) : ContDiffAt  (↑) (fun η  (η ^ s)) ξ
    theorem LeanRidgelet.contDiffAt_norm_rpow.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E] (s : ) {ξ : E}
      ( : ξ  0) :
      ContDiffAt  (↑) (fun η  (η ^ s)) ξ
    The multiplier `‖ξ‖^s` is smooth away from the origin. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    complete
    theorem LeanRidgelet.fs_exists_fractionalDerivative_of_compactSupport.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] [MeasurableSpace E] [BorelSpace E] (s : )
      (φ : SchwartzMap E )
      (hsupp :
        HasCompactSupport
          (LeanRidgelet.Fourier.angularFourierIntegralInner φ))
      (hband :
         r > 0,
           (ξ : E),
            ξ < r 
              LeanRidgelet.Fourier.angularFourierIntegralInner (⇑φ) ξ = 0) :
       ψ,
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner (⇑ψ) ξ =
            (ξ ^ s) *
              LeanRidgelet.Fourier.angularFourierIntegralInner (⇑φ) ξ
    theorem LeanRidgelet.fs_exists_fractionalDerivative_of_compactSupport.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (s : ) (φ : SchwartzMap E )
      (hsupp :
        HasCompactSupport
          (LeanRidgelet.Fourier.angularFourierIntegralInner
            φ))
      (hband :
         r > 0,
           (ξ : E),
            ξ < r 
              LeanRidgelet.Fourier.angularFourierIntegralInner
                  (⇑φ) ξ =
                0) :
       ψ,
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner
              (⇑ψ) ξ =
            (ξ ^ s) *
              LeanRidgelet.Fourier.angularFourierIntegralInner
                (⇑φ) ξ
    **The fractional derivative of a band-limited Schwartz function exists.** If the angular Fourier
    transform of `φ` has compact support and vanishes on a ball about the origin — that is, if `φ` is
    band-limited to an annulus — then multiplying that transform by `‖ξ‖^s` again comes from a Schwartz
    function.
    
    This is the elementary case, and it needs no multiplier theory: away from the origin `‖ξ‖^s` is
    smooth, on the ball the transform vanishes, so the product is smooth by gluing, it inherits the
    compact support, and a smooth compactly supported function is Schwartz. The general case is
    `fs_exists_fractionalDerivative`, where the support hypothesis is dropped and the growth of the
    multiplier has to be controlled instead. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    complete
    theorem LeanRidgelet.fs_exists_hasTemperateGrowth_eq_norm_rpow.{u_1}
      {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace  E]
      [FiniteDimensional  E] (s : ) {r : } (hr : 0 < r) :
       h,
        Function.HasTemperateGrowth h   (ξ : E), r  ξ  h ξ = ξ ^ s
    theorem LeanRidgelet.fs_exists_hasTemperateGrowth_eq_norm_rpow.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E] (s : ) {r : }
      (hr : 0 < r) :
       h,
        Function.HasTemperateGrowth h 
           (ξ : E), r  ξ  h ξ = ξ ^ s
    **A smooth cut-off of `‖ξ‖^s` has temperate growth.** For every `s` and every `r > 0` there is a
    function of temperate growth agreeing with `‖ξ‖^s` outside the ball of radius `r`. That is all the
    general fractional derivative needs.
    
    `‖ξ‖^s` itself is not of temperate growth: for non-even `s` it is not smooth at the origin, and for
    negative `s` it is not even bounded there. Away from the origin it is harmless, so what is needed is
    a smooth modification inside the ball, and the modification is put on `‖ξ‖²` rather than on `‖ξ‖^s`:
    with `β` a bump equal to `1` on the ball of radius `r/2` and supported in the ball of radius `r`,
    the function
    `q ξ = ‖ξ‖² + r² β ξ`
    is of temperate growth — a sum of `‖ξ‖²` and a smooth compactly supported function — is bounded
    below, and equals `‖ξ‖²` outside the ball. So `(q ξ)^{s/2}` is what is wanted, by
    `Function.HasTemperateGrowth.rpow_of_le`.
    
    That last step is where the Japanese bracket comes in. It is *not* a substitute for `‖ξ‖^s` — the
    bracket `(1 + ‖ξ‖²)^{s/2}` is the Bessel potential multiplier `(1 - △)^{s/2}` whereas `‖ξ‖^s` is the
    Riesz one `(-△)^{s/2}`, and Section 6 needs the homogeneous one, since the separation-of-variables
    condition asks the product `γ♯σ♯` to be `f̂(Uω)|Uω|^d` and it is exactly that homogeneity which
    matches the weight `|Ub|^{m-k}` of the matrix polar formula. But Mathlib's temperate growth of the
    bracket is the right *proof*, because there the inner function `1 + ‖ξ‖²` already avoids the origin;
    `ToMathlib.TemperateGrowth` generalizes it to an arbitrary inner function bounded away from zero,
    which is what lets the inner function be chosen as above. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    complete
    theorem LeanRidgelet.fs_exists_fractionalDerivative.{u_1} {E : Type u_1}
      [NormedAddCommGroup E] [InnerProductSpace  E] [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E] (s : ) (φ : SchwartzMap E )
      (hband :
         r > 0,
           (ξ : E),
            ξ < r 
              LeanRidgelet.Fourier.angularFourierIntegralInner (⇑φ) ξ = 0) :
       ψ,
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner (⇑ψ) ξ =
            (ξ ^ s) *
              LeanRidgelet.Fourier.angularFourierIntegralInner (⇑φ) ξ
    theorem LeanRidgelet.fs_exists_fractionalDerivative.{u_1}
      {E : Type u_1} [NormedAddCommGroup E]
      [InnerProductSpace  E]
      [FiniteDimensional  E]
      [MeasurableSpace E] [BorelSpace E]
      (s : ) (φ : SchwartzMap E )
      (hband :
         r > 0,
           (ξ : E),
            ξ < r 
              LeanRidgelet.Fourier.angularFourierIntegralInner
                  (⇑φ) ξ =
                0) :
       ψ,
         (ξ : E),
          LeanRidgelet.Fourier.angularFourierIntegralInner
              (⇑ψ) ξ =
            (ξ ^ s) *
              LeanRidgelet.Fourier.angularFourierIntegralInner
                (⇑φ) ξ
    **The fractional derivative of order `s` exists.** For a Schwartz function whose Fourier
    transform vanishes on a neighbourhood of the origin, multiplying that transform by `‖ξ‖^s` again
    comes from a Schwartz function. That is the article's `△^{s/2}`, read through its multiplier, and it
    is what discharges the hypothesis `hfrac` of `fs_stiefel_reconstruction`.
    
    The hypothesis on the support is what makes `‖ξ‖^s` harmless: it is smooth away from the origin with
    polynomially bounded derivatives there, so the product is Schwartz, but at the origin it is not
    smooth for non-even `s`. Extending to the natural classes — the Lizorkin space, or the Sobolev space
    `H^d` the article works in — is the follow-on, and is what a Riesz potential in `ToMathlib` would
    provide.
    
    The proof multiplies inside the Schwartz space, by
    `SchwartzMap.smulLeftCLM` applied to a smooth cut-off of the multiplier; that cut-off is
    `fs_exists_hasTemperateGrowth_eq_norm_rpow`, which is where the remaining `sorry` sits. Nothing else
    about this theorem is open, and the band-limited case
    `fs_exists_fractionalDerivative_of_compactSupport` is proved outright. 
Lemma3.1.28
Statement uses 2
Statement dependency previews
Preview
Theorem 3.1.23
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0L∃∀N

The Jacobian of the singular value decomposition (Lemma C.3). \mathrm dA=\delta(D)\,\mathrm dD\,\mathrm dU\,\mathrm dV with \delta(D)=2^{-k}|\det D|^{m-k}\prod_{i<j}(d_i^2-d_j^2). Stated with a sorry, for the lower Lebesgue integral so that no convergence hypothesis is needed, and with the constant left existential — the invariant measures used here are normalized to probability measures whereas the article's are the classical ones, so the statement should not fix it. No proof in this development depends on it: the reconstruction formula over full-column-rank matrices is proved in the singular value coordinates, and mathlib_svd shows those coordinates reach every such matrix, so what is missing is only the relation between the two parameter measures. Determining the constant is what would settle the two open questions about the article's constants — whether c_{m,k} is a Stiefel manifold of the orthogonal complement of the direction, and whether dropping the ordering of the singular values costs a k!.

Lean code for Lemma3.1.284 declarations, 1 incomplete
  • complete
    def LeanRidgelet.svdChart (k : ) : Set (EuclideanSpace  (Fin k))
    def LeanRidgelet.svdChart (k : ) :
      Set (EuclideanSpace  (Fin k))
    Implementation after :=
    :=
      {d | (∀ i, 0 < d i) ∧ ∀ i j : Fin k, i < j → d j < d i}
    The chart of the singular value decomposition: strictly decreasing positive singular values. 
  • complete
    def LeanRidgelet.svdMatrix {k m : }
      (U : EuclideanSpace  (Fin k) →ₗᵢ[] LeanRidgelet.InputSpace m)
      (d : EuclideanSpace  (Fin k))
      (V :
        (unitary
            (EuclideanSpace  (Fin k) →L[] EuclideanSpace  (Fin k)))) :
      Fin k  LeanRidgelet.InputSpace m
    def LeanRidgelet.svdMatrix {k m : }
      (U :
        EuclideanSpace  (Fin k) →ₗᵢ[]
          LeanRidgelet.InputSpace m)
      (d : EuclideanSpace  (Fin k))
      (V :
        (unitary
            (EuclideanSpace  (Fin k) →L[]
              EuclideanSpace  (Fin k)))) :
      Fin k  LeanRidgelet.InputSpace m
    Implementation after :=
    :=
      fun i => U (svdDiag d ((Unitary.linearIsometryEquiv V).symm (EuclideanSpace.single i (1 : ℝ))))
    The matrix `U D Vᵀ` of a point of the singular value chart, as its tuple of columns. 
  • complete
    def LeanRidgelet.svdJacobian (m k : ) (d : EuclideanSpace  (Fin k)) : 
    def LeanRidgelet.svdJacobian (m k : )
      (d : EuclideanSpace  (Fin k)) : 
    Implementation after :=
    :=
      (2 : ℝ) ^ (-(k : ℤ)) * (∏ i, d i) ^ (m - k) *
        ∏ i : Fin k, ∏ j ∈ Finset.univ.filter fun j => i < j, (d i ^ 2 - d j ^ 2)
    The article's `δ(D) = 2^{-k}|det D|^{m-k}∏_{i<j}(dᵢ² - dⱼ²)`, the density of the singular value
    decomposition. The first product runs to `k`, the number of singular values; the statement of
    `thm:affine` writes `d` there, which its own appendix contradicts. 
  • theoremdefined in LeanRidgelet/FS/Targets.lean
    contains sorry
    theorem LeanRidgelet.fs_svdJacobian {k m : }
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ : EuclideanSpace  (Fin k) →ₗᵢ[] LeanRidgelet.InputSpace m) :
       c,
        c  0 
          c   
             (G : (Fin k  LeanRidgelet.InputSpace m)  ENNReal),
              Measurable G 
                ∫⁻ (A : Fin k  LeanRidgelet.InputSpace m), G A =
                  c *
                    ∫⁻ (U :
                      EuclideanSpace  (Fin k) →ₗᵢ[]
                        LeanRidgelet.InputSpace m),
                      ∫⁻ (V :
                        (unitary
                            (EuclideanSpace  (Fin k) →L[]
                              EuclideanSpace  (Fin k)))),
                        ∫⁻ (d : EuclideanSpace  (Fin k)) in
                          LeanRidgelet.svdChart k,
                          ENNReal.ofReal (LeanRidgelet.svdJacobian m k d) *
                            G
                              (LeanRidgelet.svdMatrix U d
                                V) ContinuousLinearMap.orthogonalHaar ContinuousLinearMap.stiefelMeasure
                        L₀
    theorem LeanRidgelet.fs_svdJacobian {k m : }
      [Nontrivial (EuclideanSpace  (Fin k))]
      (L₀ :
        EuclideanSpace  (Fin k) →ₗᵢ[]
          LeanRidgelet.InputSpace m) :
       c,
        c  0 
          c   
            
              (G :
                (Fin k 
                    LeanRidgelet.InputSpace
                      m) 
                  ENNReal),
              Measurable G 
                ∫⁻ (A :
                    Fin k 
                      LeanRidgelet.InputSpace
                        m),
                    G A =
                  c *
                    ∫⁻ (U :
                      EuclideanSpace 
                          (Fin k) →ₗᵢ[]
                        LeanRidgelet.InputSpace
                          m),
                      ∫⁻ (V :
                        (unitary
                            (EuclideanSpace 
                                (Fin k) →L[]
                              EuclideanSpace 
                                (Fin k)))),
                        ∫⁻ (d :
                          EuclideanSpace 
                            (Fin k)) in
                          LeanRidgelet.svdChart
                            k,
                          ENNReal.ofReal
                              (LeanRidgelet.svdJacobian
                                m k d) *
                            G
                              (LeanRidgelet.svdMatrix
                                U d
                                V) ContinuousLinearMap.orthogonalHaar ContinuousLinearMap.stiefelMeasure
                        L₀
    **The Jacobian of the singular value decomposition**, the article's Lemma C.3: Lebesgue measure
    on the space of `m × k` matrices, read in the coordinates `A = U D Vᵀ`, has density `δ(D)` against
    the invariant measures of the Stiefel manifold and the orthogonal group and Lebesgue measure on the
    singular values.
    
    Stated for the lower Lebesgue integral, so that no convergence hypothesis is needed, and with the
    constant left existential: `stiefelMeasure` and `orthogonalHaar` are normalized to probability
    measures whereas the article's `dU` and `dV` are the classical invariant measures, so the constant
    depends on a normalization the statement should not fix. Determining it is what would settle the two
    open questions about the article's constants — whether `c_{m,k}` is a Stiefel manifold of the
    orthogonal complement, and whether dropping the ordering of the singular values costs a `k!`.
    
    The decomposition itself is `MeasureTheory.exists_svd`; what is missing is only this measure
    identity. Of the routes to it, the one that avoids differential forms reduces it to Weyl's
    integration formula for real symmetric matrices, which Mathlib also lacks.