1. L2 theory: arXiv:2106.04770v2 implementation map🔗

This chapter follows the publication order and single shared theorem-like counter of arXiv:2106.04770v2. The paper first derives the separated Fourier expression in the Introduction, isolates its abstract unitary operator theory in Section 2, and only then constructs the concrete activation, coefficient, and parameter spaces. Later sections treat adjoint ridgelet functions, finite-width consequences, numerics, and parameter perturbations as distinct developments.

The Lean project completely implements the abstract unitary layer and its transported-coordinate specialization. A few concrete analytic identifications still stop at the coefficient-vector level; these boundaries are stated below rather than hidden behind assumptions. A declaration containing sorry records a later manuscript result whose proof is still pending and is checked by the assumption audit.

The Fourier expression method in Section 1.2 proposes \gamma^\sharp(\xi/\omega,\omega)=\widehat f(\xi)\overline{\rho^\sharp(\omega)} and separates one particular direction from homogeneous directions. Lean currently validates the resulting unitary-coordinate and Hilbert-basis theory. It also reconstructs a ridgelet distribution continuously from every completed coefficient vector, with the expected weighted spectrum on the dense Schwartz core. On the Schwartz compatibility domain, the synthesis and ridgelet operators now agree with the classical network and ridgelet integrals; the remaining classical boundaries are the explicit Fourier formulas (32)--(33) and per-activation realization formulas.

Section 2: Abstract Reconstruction Formula and Solution Geometry

Definition1

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 2

Loading preview

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

✓L∃∀N

Let (X,\mu) be a measure space, let \mathcal H and \mathcal G be complex Hilbert spaces, let T:\mathcal G\simeq L^2(X,\mu;\mathcal H) be unitary, and let L:\mathcal H\to\mathbb C be continuous and linear. Define S:=\widetilde L\,T:\mathcal G\to L^2(X,\mu),\qquad R_h:=T^*J_h:L^2(X,\mu)\to\mathcal G,\qquad J_h[f](x):=f(x)h.

Lean code for Definition1●2 definitions

defdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

def LeanRidgelet.unitarySynthesis.{u_1, u_2, u_3} {α : Type u_1}
  {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [NormedAddCommGroup G] [InnerProductSpace ℂ G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  G →L[ℂ] ↥(LeanRidgelet.L2 α μ)

def LeanRidgelet.unitarySynthesis.{u_1, u_2,
    u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) :
  G →L[ℂ] ↥(LeanRidgelet.L2 α μ)

Implementation after :=

:=
  fiberSynthesis μ L ∘L (T : G →L[ℂ] BochnerL2 α H μ)

The abstract synthesis operator `S = \widetilde L T`.

defdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

def LeanRidgelet.unitaryRidgelet.{u_1, u_2, u_3} {α : Type u_1}
  {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [NormedAddCommGroup G] [InnerProductSpace ℂ G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (h : H) :
  ↥(LeanRidgelet.L2 α μ) →L[ℂ] G

def LeanRidgelet.unitaryRidgelet.{u_1, u_2,
    u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (h : H) : ↥(LeanRidgelet.L2 α μ) →L[ℂ] G

Implementation after :=

:=
  (T.symm : BochnerL2 α H μ →L[ℂ] G) ∘L fiberRidgelet μ h

The abstract ridgelet map `R_h = T* J_h`.  For a unitary equivalence, `T* = T⁻¹`.

Theorem2

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 3

Loading preview

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

✓L∃∀N

Under Definition 1, let h\in\mathcal H, let h_L be the Riesz vector determined by L[h]=\langle h,h_L\rangle, and put c_L:=\|h_L\|^2=\|L\|^2. Then S\circ R_h=L[h]I,\qquad S^*=R_{h_L},\qquad S\circ S^*=c_LI, \qquad \|S^*[f]\|^2=c_L\|f\|^2\quad(f\in L^2(X,\mu)). No hypothesis L\ne0 is required.

Lean code for Theorem2●4 theorems

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.unitarySynthesis_comp_unitaryRidgelet.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [NormedAddCommGroup G] [InnerProductSpace ℂ G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ)
  (h : H) :
  LeanRidgelet.unitarySynthesis μ T L ∘SL
      LeanRidgelet.unitaryRidgelet μ T h =
    L h • ContinuousLinearMap.id ℂ ↥(LeanRidgelet.L2 α μ)

theorem LeanRidgelet.unitarySynthesis_comp_unitaryRidgelet.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) (h : H) :
  LeanRidgelet.unitarySynthesis μ T L ∘SL
      LeanRidgelet.unitaryRidgelet μ T h =
    L h •
      ContinuousLinearMap.id ℂ
        ↥(LeanRidgelet.L2 α μ)

Abstract reconstruction: `S R_h = L[h] I`.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.adjoint_unitarySynthesis.{u_1, u_2, u_3} {α : Type u_1}
  {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  ContinuousLinearMap.adjoint (LeanRidgelet.unitarySynthesis μ T L) =
    LeanRidgelet.unitaryRidgelet μ T (LeanRidgelet.rieszRepresenter L)

theorem LeanRidgelet.adjoint_unitarySynthesis.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) :
  ContinuousLinearMap.adjoint
      (LeanRidgelet.unitarySynthesis μ T
        L) =
    LeanRidgelet.unitaryRidgelet μ T
      (LeanRidgelet.rieszRepresenter L)

The adjoint of synthesis is the ridgelet map associated with the Riesz representer.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.unitarySynthesis_comp_adjoint.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  LeanRidgelet.unitarySynthesis μ T L ∘SL
      ContinuousLinearMap.adjoint
        (LeanRidgelet.unitarySynthesis μ T L) =
    ↑(LeanRidgelet.fiberNormalization L) •
      ContinuousLinearMap.id ℂ ↥(LeanRidgelet.L2 α μ)

theorem LeanRidgelet.unitarySynthesis_comp_adjoint.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) :
  LeanRidgelet.unitarySynthesis μ T L ∘SL
      ContinuousLinearMap.adjoint
        (LeanRidgelet.unitarySynthesis μ T
          L) =
    ↑(LeanRidgelet.fiberNormalization L) •
      ContinuousLinearMap.id ℂ
        ↥(LeanRidgelet.L2 α μ)

Synthesis composed with its adjoint is scalar multiplication by `c_L`.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.norm_adjoint_unitarySynthesis_sq.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ)
  (f : ↥(LeanRidgelet.L2 α μ)) :
  ‖(ContinuousLinearMap.adjoint (LeanRidgelet.unitarySynthesis μ T L))
          f‖ ^
      2 =
    LeanRidgelet.fiberNormalization L * ‖f‖ ^ 2

theorem LeanRidgelet.norm_adjoint_unitarySynthesis_sq.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ)
  (f : ↥(LeanRidgelet.L2 α μ)) :
  ‖(ContinuousLinearMap.adjoint
            (LeanRidgelet.unitarySynthesis
              μ T L))
          f‖ ^
      2 =
    LeanRidgelet.fiberNormalization L *
      ‖f‖ ^ 2

Exact norm identity for the abstract synthesis adjoint.

Theorem3

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4

Loading preview

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

✓L∃∀N

Assume the data of Definition 1 and L\ne0. Define S^\dagger:=c_L^{-1}S^*,\qquad P:=S^\dagger S. Then SS^\dagger=I, P^2=P=P^*, and \ker P=\ker S,\qquad \operatorname{ran}P=(\ker S)^\perp, \qquad T[\ker S]=L^2(X,\mu;\ker L). Moreover, for f\in L^2(X,\mu) and \gamma\in\mathcal G, S[\gamma]=f\iff\gamma-S^\dagger[f]\in\ker S, and every such solution satisfies \|\gamma\|^2=\|S^\dagger[f]\|^2+\|\gamma-S^\dagger[f]\|^2. Thus S^\dagger[f] is the unique minimum-norm solution.

Lean code for Theorem3●11 declarations

defdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

def LeanRidgelet.unitaryMoorePenroseInverse.{u_1, u_2, u_3} {α : Type u_1}
  {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  ↥(LeanRidgelet.L2 α μ) →L[ℂ] G

def LeanRidgelet.unitaryMoorePenroseInverse.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) :
  ↥(LeanRidgelet.L2 α μ) →L[ℂ] G

Implementation after :=

:=
  ((fiberNormalization L : ℂ)⁻¹) • (unitarySynthesis μ T L)†

The abstract Moore--Penrose inverse `S† = c_L⁻¹ S*` for nonzero `L`.

Here the name `moorePenroseInverse` distinguishes it from Lean's postfix `†`, which denotes only
the Hilbert adjoint.

defdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

def LeanRidgelet.unitaryParameterProjection.{u_1, u_2, u_3} {α : Type u_1}
  {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  G →L[ℂ] G

def LeanRidgelet.unitaryParameterProjection.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) : G →L[ℂ] G

Implementation after :=

:=
  unitaryMoorePenroseInverse μ T L ∘L unitarySynthesis μ T L

The canonical parameter projection `P = S† S`.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.unitaryMoorePenroseInverse_rightInverse.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) :
  Function.RightInverse ⇑(LeanRidgelet.unitaryMoorePenroseInverse μ T L)
    ⇑(LeanRidgelet.unitarySynthesis μ T L)

theorem LeanRidgelet.unitaryMoorePenroseInverse_rightInverse.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0) :
  Function.RightInverse
    ⇑(LeanRidgelet.unitaryMoorePenroseInverse
        μ T L)
    ⇑(LeanRidgelet.unitarySynthesis μ T L)

For nonzero `L`, the Moore--Penrose inverse is a right inverse of synthesis.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.isIdempotentElem_unitaryParameterProjection.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) :
  IsIdempotentElem (LeanRidgelet.unitaryParameterProjection μ T L)

theorem LeanRidgelet.isIdempotentElem_unitaryParameterProjection.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0) :
  IsIdempotentElem
    (LeanRidgelet.unitaryParameterProjection
      μ T L)

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.isSelfAdjoint_unitaryParameterProjection.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  IsSelfAdjoint (LeanRidgelet.unitaryParameterProjection μ T L)

theorem LeanRidgelet.isSelfAdjoint_unitaryParameterProjection.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) :
  IsSelfAdjoint
    (LeanRidgelet.unitaryParameterProjection
      μ T L)

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.ker_unitaryParameterProjection.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) :
  (↑(LeanRidgelet.unitaryParameterProjection μ T L)).ker =
    (↑(LeanRidgelet.unitarySynthesis μ T L)).ker

theorem LeanRidgelet.ker_unitaryParameterProjection.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0) :
  (↑(LeanRidgelet.unitaryParameterProjection
          μ T L)).ker =
    (↑(LeanRidgelet.unitarySynthesis μ T
          L)).ker

The kernel of the canonical parameter projection is the synthesis kernel.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.range_unitaryParameterProjection.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) :
  (↑(LeanRidgelet.unitaryParameterProjection μ T L)).range =
    (↑(LeanRidgelet.unitarySynthesis μ T L)).kerᗮ

theorem LeanRidgelet.range_unitaryParameterProjection.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0) :
  (↑(LeanRidgelet.unitaryParameterProjection
          μ T L)).range =
    (↑(LeanRidgelet.unitarySynthesis μ T
            L)).kerᗮ

The range of the canonical projection is the orthogonal complement of the synthesis kernel.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.map_ker_unitarySynthesis.{u_1, u_2, u_3} {α : Type u_1}
  {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [NormedAddCommGroup G] [InnerProductSpace ℂ G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ) :
  Submodule.map (↑T.toLinearEquiv)
      (↑(LeanRidgelet.unitarySynthesis μ T L)).ker =
    (↑(LeanRidgelet.fiberSynthesis μ L)).ker

theorem LeanRidgelet.map_ker_unitarySynthesis.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ) :
  Submodule.map (↑T.toLinearEquiv)
      (↑(LeanRidgelet.unitarySynthesis μ T
            L)).ker =
    (↑(LeanRidgelet.fiberSynthesis μ
          L)).ker

Unitary coordinates identify the synthesis kernel with the coordinate-side pointwise kernel.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.unitarySolution_iff_kernel_translate.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) (f : ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  (LeanRidgelet.unitarySynthesis μ T L) γ = f ↔
    γ - (LeanRidgelet.unitaryMoorePenroseInverse μ T L) f ∈
      (↑(LeanRidgelet.unitarySynthesis μ T L)).ker

theorem LeanRidgelet.unitarySolution_iff_kernel_translate.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0)
  (f : ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  (LeanRidgelet.unitarySynthesis μ T L)
        γ =
      f ↔
    γ -
        (LeanRidgelet.unitaryMoorePenroseInverse
            μ T L)
          f ∈
      (↑(LeanRidgelet.unitarySynthesis μ T
            L)).ker

Every solution is the canonical solution plus an element of the synthesis kernel.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.unitaryMoorePenroseInverse_pythagorean.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) (f : ↥(LeanRidgelet.L2 α μ)) (γ : G)
  (hγ : (LeanRidgelet.unitarySynthesis μ T L) γ = f) :
  ‖γ‖ ^ 2 =
    ‖(LeanRidgelet.unitaryMoorePenroseInverse μ T L) f‖ ^ 2 +
      ‖γ - (LeanRidgelet.unitaryMoorePenroseInverse μ T L) f‖ ^ 2

theorem LeanRidgelet.unitaryMoorePenroseInverse_pythagorean.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0)
  (f : ↥(LeanRidgelet.L2 α μ)) (γ : G)
  (hγ :
    (LeanRidgelet.unitarySynthesis μ T L)
        γ =
      f) :
  ‖γ‖ ^ 2 =
    ‖(LeanRidgelet.unitaryMoorePenroseInverse
              μ T L)
            f‖ ^
        2 +
      ‖γ -
            (LeanRidgelet.unitaryMoorePenroseInverse
                μ T L)
              f‖ ^
        2

Pythagoras identity for the abstract parameter-space solution decomposition.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.unitaryMoorePenroseInverse_unique_minimal.{u_1, u_2, u_3}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] [CompleteSpace G]
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) {L : H →L[ℂ] ℂ}
  (hL : L ≠ 0) (f : ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  (LeanRidgelet.unitarySynthesis μ T L) γ = f →
    ‖(LeanRidgelet.unitaryMoorePenroseInverse μ T L) f‖ ≤ ‖γ‖ ∧
      (‖(LeanRidgelet.unitaryMoorePenroseInverse μ T L) f‖ = ‖γ‖ →
        (LeanRidgelet.unitaryMoorePenroseInverse μ T L) f = γ)

theorem LeanRidgelet.unitaryMoorePenroseInverse_unique_minimal.{u_1,
    u_2, u_3}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G]
  [CompleteSpace G]
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  {L : H →L[ℂ] ℂ} (hL : L ≠ 0)
  (f : ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  (LeanRidgelet.unitarySynthesis μ T L)
        γ =
      f →
    ‖(LeanRidgelet.unitaryMoorePenroseInverse
              μ T L)
            f‖ ≤
        ‖γ‖ ∧
      (‖(LeanRidgelet.unitaryMoorePenroseInverse
                μ T L)
              f‖ =
          ‖γ‖ →
        (LeanRidgelet.unitaryMoorePenroseInverse
              μ T L)
            f =
          γ)

The abstract Moore--Penrose solution is the unique minimum-norm solution.

Theorem4

uses 1used by 1✓L∃∀N

Assume Definition 1 and let (e_i)_{i\in I} be a Hilbert basis of L^2(X,\mu). For \gamma\in\mathcal G, define h_i[\gamma]\in\mathcal H by the partial inner product of T[\gamma] against e_i. Then \gamma=\sum_{i\in I}R_{h_i[\gamma]}[e_i],\qquad \sum_{i\in I}\|h_i[\gamma]\|^2=\|\gamma\|^2, and these coefficient vectors are unique. Furthermore, \gamma\in\ker S\iff(\forall i\in I)\;h_i[\gamma]\in\ker L. If (k_j)_{j\in J} is a Hilbert basis of \ker L, every \gamma\in\ker S also has the unconditionally convergent expansion \gamma=\sum_{(i,j)\in I\times J}c_{ij}\,R_{k_j}[e_i], \qquad(c_{ij})\in\ell^2(I\times J).

Lean code for Theorem4●6 declarations

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.hasSum_unitaryRidgelet_coefficients.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ))
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  HasSum
    (fun i ↦
      (LeanRidgelet.unitaryRidgelet μ T
          (LeanRidgelet.unitaryCoefficient μ T (b i) γ))
        (b i))
    γ

theorem LeanRidgelet.hasSum_unitaryRidgelet_coefficients.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (γ : G) :
  HasSum
    (fun i ↦
      (LeanRidgelet.unitaryRidgelet μ T
          (LeanRidgelet.unitaryCoefficient
            μ T (b i) γ))
        (b i))
    γ

Hilbert-basis expansion in the abstract parameter space.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.eq_unitaryCoefficient_of_hasSum_unitaryRidgelet.{u_1, u_2,
    u_3, u_4}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ))
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ)) (h : ι → H) (γ : G)
  (hq :
    HasSum (fun i ↦ (LeanRidgelet.unitaryRidgelet μ T (h i)) (b i)) γ)
  (i : ι) : h i = LeanRidgelet.unitaryCoefficient μ T (b i) γ

theorem LeanRidgelet.eq_unitaryCoefficient_of_hasSum_unitaryRidgelet.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (h : ι → H) (γ : G)
  (hq :
    HasSum
      (fun i ↦
        (LeanRidgelet.unitaryRidgelet μ T
            (h i))
          (b i))
      γ)
  (i : ι) :
  h i =
    LeanRidgelet.unitaryCoefficient μ T
      (b i) γ

Coefficient vectors in the unitary ridgelet expansion are unique.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.hasSum_norm_sq_unitaryCoefficient.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ))
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  HasSum (fun i ↦ ‖LeanRidgelet.unitaryCoefficient μ T (b i) γ‖ ^ 2)
    (‖γ‖ ^ 2)

theorem LeanRidgelet.hasSum_norm_sq_unitaryCoefficient.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (γ : G) :
  HasSum
    (fun i ↦
      ‖LeanRidgelet.unitaryCoefficient μ T
            (b i) γ‖ ^
        2)
    (‖γ‖ ^ 2)

Parseval identity for coefficient vectors in the abstract parameter space.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.mem_ker_unitarySynthesis_iff_coefficients.{u_1, u_2, u_3,
    u_4}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ)) (γ : G) :
  γ ∈ (↑(LeanRidgelet.unitarySynthesis μ T L)).ker ↔
    ∀ (i : ι), L (LeanRidgelet.unitaryCoefficient μ T (b i) γ) = 0

theorem LeanRidgelet.mem_ker_unitarySynthesis_iff_coefficients.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (γ : G) :
  γ ∈
      (↑(LeanRidgelet.unitarySynthesis μ T
            L)).ker ↔
    ∀ (i : ι),
      L
          (LeanRidgelet.unitaryCoefficient
            μ T (b i) γ) =
        0

A parameter is null exactly when every Hilbert-basis coefficient lies in `ker L`.

defdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

def LeanRidgelet.unitaryNullDoubleCoefficients.{u_1, u_2, u_3, u_4, u_5}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4} {κ : Type u_5}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ))
  (d : HilbertBasis κ ℂ ↥(↑L).ker) (γ : G)
  (hγ : γ ∈ (↑(LeanRidgelet.unitarySynthesis μ T L)).ker) :
  ↥(lp (fun x ↦ ℂ) 2)

def LeanRidgelet.unitaryNullDoubleCoefficients.{u_1,
    u_2, u_3, u_4, u_5}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  {κ : Type u_5}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (d : HilbertBasis κ ℂ ↥(↑L).ker) (γ : G)
  (hγ :
    γ ∈
      (↑(LeanRidgelet.unitarySynthesis μ T
            L)).ker) :
  ↥(lp (fun x ↦ ℂ) 2)

Implementation after :=

:=
  fiberNullDoubleCoefficients μ L b d (T γ) (by
    change fiberSynthesis μ L (T γ) = 0
    exact hγ)

The flattened null coefficients of an abstract parameter as an element of `ℓ²(I × J)`.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.hasSum_unitaryRidgelet_kernelBasis.{u_1, u_2, u_3, u_4,
    u_5}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4} {κ : Type u_5}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ))
  (d : HilbertBasis κ ℂ ↥(↑L).ker) (γ : G)
  (hγ : γ ∈ (↑(LeanRidgelet.unitarySynthesis μ T L)).ker) :
  HasSum
    (fun p ↦
      ↑(LeanRidgelet.unitaryNullDoubleCoefficients μ T L b d γ hγ) p •
        (LeanRidgelet.unitaryRidgelet μ T ↑(d p.2)) (b p.1))
    γ

theorem LeanRidgelet.hasSum_unitaryRidgelet_kernelBasis.{u_1,
    u_2, u_3, u_4, u_5}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  {κ : Type u_5}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (d : HilbertBasis κ ℂ ↥(↑L).ker) (γ : G)
  (hγ :
    γ ∈
      (↑(LeanRidgelet.unitarySynthesis μ T
            L)).ker) :
  HasSum
    (fun p ↦
      ↑(LeanRidgelet.unitaryNullDoubleCoefficients
              μ T L b d γ hγ)
          p •
        (LeanRidgelet.unitaryRidgelet μ T
            ↑(d p.2))
          (b p.1))
    γ

Every abstract null parameter has the unconditional `I × J` ridgelet expansion associated
with Hilbert bases of `L²(X)` and `ker L`.

Section 3: Neural-Network Specialization: Hilbert Spaces and Boundedness

Definition5

uses 0

Used by 2

Reverse dependency previews

Preview

Proposition 6

Loading preview

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

✓L∃∀N

For s,t\in\mathbb R, define the activation space \mathcal A_{s,t}:=\langle\cdot\rangle^tH^s(\mathbb R), represented by its Fourier--Bessel coordinate u\in L^2(\mathbb R). In Lean, the coordinate Hilbert space determines the associated tempered distribution \sigma=\langle\cdot\rangle^t\langle\partial\rangle^{-s}[u].

Lean code for Definition5●2 definitions

abbrevdefined in LeanRidgelet/Space/Activation.lean

complete

abbrev LeanRidgelet.ActivationSpace (_s _t : ℝ) :
  AddSubgroup (ℝ →ₘ[MeasureTheory.volume] ℂ)

abbrev LeanRidgelet.ActivationSpace (_s _t : ℝ) :
  AddSubgroup
    (ℝ →ₘ[MeasureTheory.volume] ℂ)

Implementation after :=

:= L2 ℝ volume

The Hilbert coordinate model of the activation space `A_{s,t}`.

defdefined in LeanRidgelet/Space/Activation.lean

complete

def LeanRidgelet.activationDistribution (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s t) →L[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.activationDistribution
  (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s
        t) →L[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:=
  temperedWeightMultiplier t ∘L
    paperBesselPotential (-s) ∘L
      Lp.toTemperedDistributionCLM ℂ volume 2

Realize an activation coordinate as an element of `⟨·⟩^t H^s(ℝ) ⊆ 𝓢'(ℝ)`.

Proposition6

uses 1used by 0✓L∃∀N

For every s,t\in\mathbb R, the coordinate map of Definition 5 is a linear isometric equivalence \mathcal A_{s,t}\simeq L^2(\mathbb R). Consequently \mathcal A_{s,t} is a complex Hilbert space.

Lean code for Proposition6●1 theorem

theoremdefined in LeanRidgelet/OverviewL2.lean

complete

theorem LeanRidgelet.l2_proposition_one_activation_hilbert_structure (s t : ℝ) :
  Nonempty
    (↥(LeanRidgelet.ActivationSpace s t) ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.L2 ℝ MeasureTheory.volume))

theorem LeanRidgelet.l2_proposition_one_activation_hilbert_structure
  (s t : ℝ) :
  Nonempty
    (↥(LeanRidgelet.ActivationSpace s
          t) ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.L2 ℝ
          MeasureTheory.volume))

Manuscript Proposition 6: the activation coordinate map is an
isometric isomorphism onto `L²(ℝ)`.

Definition7

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 8

Loading preview

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

✓L∃∀N

Let m\ge1 and s,t\in\mathbb R. For h\in\mathcal S(\mathbb R), define \|h\|_{\mathcal H_{s,t}}^2:=C_m\int_{\mathbb R}|h(\omega)|^2|\omega|^m\,d\omega +\int_{\mathbb R}|\langle\partial_\omega\rangle^t[h](\omega)|^2 \langle\omega\rangle^{-2s}\,d\omega. The coefficient space \mathcal H_{s,t} is the Hilbert completion of this normed core. Every completed h\in\mathcal H_{s,t} has a tempered-distribution realization that equals the original Schwartz function on the dense core.

Lean code for Definition7●4 declarations

defdefined in LeanRidgelet/Space/Fiber.lean

complete

def LeanRidgelet.fiberNormSq (m : ℕ) (s t : ℝ) (h : SchwartzMap ℝ ℂ) : ℝ

def LeanRidgelet.fiberNormSq (m : ℕ) (s t : ℝ)
  (h : SchwartzMap ℝ ℂ) : ℝ

Implementation after :=

:=
  fiberBaseNormSq m h + fiberSobolevNormSq s t h

The squared norm on the Schwartz core of `H_{s,t}`, before Hilbert completion.

abbrevdefined in LeanRidgelet/Space/Fiber.lean

complete

abbrev LeanRidgelet.FiberSpace (m : ℕ) [NeZero m] (s t : ℝ) : Type

abbrev LeanRidgelet.FiberSpace (m : ℕ) [NeZero m]
  (s t : ℝ) : Type

Implementation after :=

:=
  UniformSpace.Completion (FiberCore m s t)

The fiber Hilbert space `H_{s,t}`, defined as the completion of its Schwartz core.

defdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

def LeanRidgelet.fiberDistribution (m : ℕ) [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.fiberDistribution (m : ℕ)
  [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:=
  paperBesselPotential (-t) ∘L
    temperedWeightMultiplier s ∘L
      Lp.toTemperedDistributionCLM ℂ volume 2 ∘L
        fiberDualCoordinate m s t

Realize a completed coefficient vector as a tempered distribution by undoing its weighted
Bessel coordinate.  This is the distributional realization needed before constructing the
manuscript ridgelet function `ρ` from its coefficient vector `hρ`.

theoremdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

theorem LeanRidgelet.fiberDistribution_coe (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.fiberDistribution m s t) ↑h =
    (SchwartzMap.toTemperedDistributionCLM ℝ ℂ MeasureTheory.volume)
      h.toSchwartz

theorem LeanRidgelet.fiberDistribution_coe (m : ℕ)
  [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.fiberDistribution m s t)
      ↑h =
    (SchwartzMap.toTemperedDistributionCLM
        ℝ ℂ MeasureTheory.volume)
      h.toSchwartz

On the dense Schwartz core, the completed coefficient-distribution realization recovers the
original Schwartz function as a tempered distribution.

Definition8

Statement uses 2

Statement dependency previews

Preview

Definition 5

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Definition 13

Loading preview

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

✓L∃∀N

Let m\ge1, s,t\in\mathbb R, and \sigma\in\mathcal A_{s,t}. Define the spectrum \sigma^\sharp:=\texttt{activationSpectrum}(\sigma) and its inverse-Fourier realization \sigma_{\mathrm{cl}}:=\mathcal F^{-1}[\sigma^\sharp]. Then the pairing extends uniquely to a continuous linear functional L_\sigma:\mathcal H_{s,t}\to\mathbb C with \|L_\sigma\|\le(2\pi)^{m-1}\|\sigma\|_{\mathcal A_{s,t}},\qquad L_\sigma[h]=(2\pi)^{m-1}\sigma^\sharp[h] for every Schwartz-core coefficient h.

Lean code for Definition8●5 declarations

defdefined in LeanRidgelet/Space/Duality.lean

complete

def LeanRidgelet.activationFiberFunctional (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.FiberSpace m s t →L[ℂ] ℂ

def LeanRidgelet.activationFiberFunctional
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.FiberSpace m s t →L[ℂ] ℂ

Implementation after :=

:=
  ((2 * Real.pi : ℂ) ^ (m - 1)) •
    ((innerSL ℂ (star σ)).comp (fiberDualCoordinate m s t))

The activation-induced functional `L_σ` on the coefficient Hilbert space.

defdefined in LeanRidgelet/Space/Activation.lean

complete

def LeanRidgelet.activationSpectrum (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s t) →L[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.activationSpectrum
  (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s
        t) →L[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:=
  paperBesselPotential t ∘L
    temperedWeightMultiplier (-s) ∘L
      Lp.toTemperedDistributionCLM ℂ volume 2

The manuscript activation spectrum `σ♯ = ⟨∂ω⟩^t[⟨ω⟩^{-s} σ]`, reconstructed from the
`L²` activation coordinate `σ = ⟨ω⟩^s ⟨∂ω⟩^{-t}[σ♯]`.

defdefined in LeanRidgelet/Space/Activation.lean

complete

def LeanRidgelet.activationRealization (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s t) →L[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.activationRealization
  (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s
        t) →L[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:=
  paperFourierInvDistribution ∘L activationSpectrum s t

The classical activation `σ = 𝓕⁻¹_paper[σ♯]`, realized as a tempered distribution from the
activation coordinate.  This is the activation whose network the synthesis operator actually
computes; compare `activationDistribution`, which realizes the same coordinate through the
real-domain weighted Sobolev isometry instead.

theoremdefined in LeanRidgelet/Space/ActivationRealization.lean

complete

theorem LeanRidgelet.activationSpectrum_apply (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) (h : SchwartzMap ℝ ℂ) :
  ((LeanRidgelet.activationSpectrum s t) σ) h =
    inner ℂ (star σ) (LeanRidgelet.fiberDualCoordinateCoreValue s t h)

theorem LeanRidgelet.activationSpectrum_apply
  (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (h : SchwartzMap ℝ ℂ) :
  ((LeanRidgelet.activationSpectrum s t)
        σ)
      h =
    inner ℂ (star σ)
      (LeanRidgelet.fiberDualCoordinateCoreValue
        s t h)

The activation spectrum acts on a Schwartz coefficient vector by the weighted dual pairing.
This identity is the content of the manuscript's self-adjoint rewrite of `∫ h σ♯`.

theoremdefined in LeanRidgelet/Space/ActivationRealization.lean

complete

theorem LeanRidgelet.activationFiberFunctional_eq_spectrum (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.activationFiberFunctional m s t σ) ↑h =
    (2 * ↑Real.pi) ^ (m - 1) *
      ((LeanRidgelet.activationSpectrum s t) σ) h.toSchwartz

theorem LeanRidgelet.activationFiberFunctional_eq_spectrum
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.activationFiberFunctional
        m s t σ)
      ↑h =
    (2 * ↑Real.pi) ^ (m - 1) *
      ((LeanRidgelet.activationSpectrum s
            t)
          σ)
        h.toSchwartz

On the Schwartz fiber core, the activation functional is `(2π)^{m-1}` times the
distributional action of the manuscript spectrum `σ♯`.  This proves the Blueprint formula
`L_σ[h] = (2π)^{m-1} ∫ h(ω) σ♯(ω) dω` for the transported coordinate model.

Definition9

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 10

Loading preview

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

✓L∃∀N

Let m\ge1, s,t\in\mathbb R, and \gamma\in\mathcal S(\mathbb R^m\times\mathbb R). Define T_{\mathrm{pt}}[\gamma](x,\omega):=(2\pi)^{-m} \int_{\mathbb R^m\times\mathbb R}\gamma(a,b)e^{i\omega(a\cdot x-b)}\,da\,db. For each x, the function \omega\mapsto T_{\mathrm{pt}}[\gamma](x,\omega) is bundled as a coefficient-core vector. If this fiber-valued map belongs to Bochner L^2, it determines an element of the completed coordinate and parameter spaces.

Lean code for Definition9●4 definitions

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.fourierDilationTransformCore {m : ℕ}
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) (ω : ℝ) : ℂ

def LeanRidgelet.fourierDilationTransformCore
  {m : ℕ}
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ω : ℝ) : ℂ

Implementation after :=

:=
  ((2 * Real.pi : ℂ) ^ m)⁻¹ *
    ∫ p : InputSpace m × ℝ, γ p * fourierDilationKernel x ω p

The Fourier construction of `T` on Schwartz parameter distributions, before Hilbert-space
extension.

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.fourierDilationTransformFiberCore {m : ℕ} [NeZero m]
  (s t : ℝ) (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) : LeanRidgelet.FiberCore m s t

def LeanRidgelet.fourierDilationTransformFiberCore
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.FiberCore m s t

Implementation after :=

:=
  ((2 * Real.pi : ℂ) ^ m)⁻¹ •
    SchwartzMap.compCLMOfAntilipschitz ℂ (by fun_prop)
      antilipschitzWith_paperFrequencyScale (parameterFourierRestriction γ x)

The integral Fourier--dilation formula, bundled as an element of the Schwartz fiber core.

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.fourierDilationTransformCoreL2 {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
      (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume)

def LeanRidgelet.fourierDilationTransformCoreL2
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↥(LeanRidgelet.BochnerL2
      (LeanRidgelet.InputSpace m)
      (LeanRidgelet.FiberSpace m s t)
      MeasureTheory.volume)

Implementation after :=

:=
  hγ.toLp (fourierDilationTransformFiber s t γ)

Bundle the fiber-valued core formula as a Bochner `L²` coordinate once its analytic
membership has been established.

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.parameterSchwartzRealization {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↥(LeanRidgelet.ParameterSpace m s t)

def LeanRidgelet.parameterSchwartzRealization
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↥(LeanRidgelet.ParameterSpace m s t)

Implementation after :=

:=
  inverseFourierDilationTransform m s t (fourierDilationTransformCoreL2 s t γ hγ)

The parameter-space element represented by a concrete Schwartz core formula whose
fiber-valued transform belongs to Bochner `L²`. This uses the inverse transported unitary rather
than storing membership as a field of a new assumption object.

Lemma10

uses 1used by 1✓L∃∀N

Let m\ge1 and let g:\mathbb R^m\times\mathbb R\to[0,\infty] be Borel measurable. Then \int g(a,\omega)\,da\,d\omega=\int g(-\omega x,\omega)|\omega|^m\,dx\,d\omega. The exceptional slice \omega=0 is handled measure-theoretically rather than by claiming a globally invertible change of variables.

Lean code for Lemma10●1 theorem

theoremdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

theorem LeanRidgelet.integral_fourierDilationCoordinate_mul {m : ℕ} [NeZero m]
  (f : LeanRidgelet.InputSpace m × ℝ → ℝ)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf_cont : Continuous f) :
  ∫ (z : LeanRidgelet.InputSpace m × ℝ), f z =
    ∫ (z : LeanRidgelet.InputSpace m × ℝ),
      f (LeanRidgelet.fourierDilationCoordinate z.1 z.2) * |z.2| ^ m

theorem LeanRidgelet.integral_fourierDilationCoordinate_mul
  {m : ℕ} [NeZero m]
  (f : LeanRidgelet.InputSpace m × ℝ → ℝ)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf_cont : Continuous f) :
  ∫ (z : LeanRidgelet.InputSpace m × ℝ),
      f z =
    ∫ (z : LeanRidgelet.InputSpace m × ℝ),
      f
          (LeanRidgelet.fourierDilationCoordinate
            z.1 z.2) *
        |z.2| ^ m

Weighted dilation change of variables in integral form. This is the identity obtained by
pushing `|ω|^m dx dω` forward along `(x, ω) ↦ (-ωx, ω)`. It does not require global
injectivity: the exceptional fiber `ω = 0` is null, and the remaining fibers use Haar-measure
scaling.

Definition11

Statement uses 3

Statement dependency previews

Preview

Definition 7

Loading preview

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

used by 1✓L∃∀N

Let m\ge1 and s,t\in\mathbb R. Define the parameter Hilbert space and its coordinate map by \mathcal G_{s,t}:=L^2(\mathbb R^m;\mathcal H_{s,t}),\qquad T:\mathcal G_{s,t}\simeq L^2(\mathbb R^m;\mathcal H_{s,t}). The Lean parameter space is this transported coordinate model. Its identification with the manuscript's concrete graph domain is treated separately on the compatibility domain.

Lean code for Definition11●4 definitions

abbrevdefined in LeanRidgelet/Space/Parameter.lean

complete

abbrev LeanRidgelet.ParameterSpace (m : ℕ) [NeZero m] (s t : ℝ) :
  AddSubgroup
    (LeanRidgelet.InputSpace m →ₘ[MeasureTheory.volume]
      LeanRidgelet.FiberSpace m s t)

abbrev LeanRidgelet.ParameterSpace (m : ℕ)
  [NeZero m] (s t : ℝ) :
  AddSubgroup
    (LeanRidgelet.InputSpace
        m →ₘ[MeasureTheory.volume]
      LeanRidgelet.FiberSpace m s t)

Implementation after :=

:=
  BochnerL2 (InputSpace m) (FiberSpace m s t) volume

The coordinate model `L²(ℝᵐ; H_{s,t})` of the parameter Hilbert space.

defdefined in LeanRidgelet/Space/Parameter.lean

complete

def LeanRidgelet.parameterCoordinateEquiv (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume)

def LeanRidgelet.parameterCoordinateEquiv
  (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2
        (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t)
        MeasureTheory.volume)

Implementation after :=

:=
  LinearIsometryEquiv.refl ℂ _

The parameter-space unitary, with the source defined by transport to its Bochner `L²` model.

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.fourierDilationTransform (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume)

def LeanRidgelet.fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2
        (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t)
        MeasureTheory.volume)

Implementation after :=

:=
  parameterCoordinateEquiv m s t

The unitary coordinate transform `T` in the transported coordinate model.

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.inverseFourierDilationTransform (m : ℕ) [NeZero m]
  (s t : ℝ) :
  ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

def LeanRidgelet.inverseFourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.BochnerL2
        (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t)
        MeasureTheory.volume) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

Implementation after :=

:=
  (fourierDilationTransform m s t).symm

The Hilbert-space inverse `T⁻¹ = T*`; the test-function Fourier expression is given below.

Proposition12

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 13

Loading preview

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

✓L∃∀N

Let m\ge1, s,t\in\mathbb R, and let T be Definition 11. Then T is unitary and T^{-1}T=I. If \gamma\in\mathcal S(\mathbb R^m\times\mathbb R) satisfies T_{\mathrm{pt}}[\gamma]\in L^2(\mathbb R^m;\mathcal H_{s,t}), then T[\gamma]=T_{\mathrm{pt}}[\gamma]\quad\text{a.e.} after embedding \gamma in \mathcal G_{s,t}. The inverse core is T^{-1}_{\mathrm{pt}}[u](a,b)=\frac1{2\pi}\int u(x,\omega) e^{-i\omega(a\cdot x-b)}|\omega|^m\,dx\,d\omega. Equality of the last integral with the transported inverse is not yet asserted.

Lean code for Proposition12●6 declarations

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.fourierDilationTransform (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume)

def LeanRidgelet.fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2
        (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t)
        MeasureTheory.volume)

Implementation after :=

:=
  parameterCoordinateEquiv m s t

The unitary coordinate transform `T` in the transported coordinate model.

theoremdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

theorem LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ)
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.inverseFourierDilationTransform m s t)
      ((LeanRidgelet.fourierDilationTransform m s t) γ) =
    γ

theorem LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ)
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.inverseFourierDilationTransform
        m s t)
      ((LeanRidgelet.fourierDilationTransform
          m s t)
        γ) =
    γ

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.fourierDilationCompatibilityDomain {m : ℕ} [NeZero m]
  (s t : ℝ) : Set (SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)

def LeanRidgelet.fourierDilationCompatibilityDomain
  {m : ℕ} [NeZero m] (s t : ℝ) :
  Set
    (SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)

Implementation after :=

:=
  {γ | AEStronglyMeasurable (fourierDilationTransformFiber s t γ) volume ∧
    Integrable (fun x : InputSpace m =>
      fiberSobolevNormSq s t (fourierDilationTransformFiberCore s t γ x))}

The manuscript compatibility domain `S^T_{s,t}(Θ)` for Schwartz parameter data.

The two clauses keep the analytic responsibilities visible: strong measurability of the
completion-valued core and integrability of its Sobolev graph term.  This is a set predicate,
not a structure carrying unproved analytic assumptions.

theoremdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

theorem LeanRidgelet.mem_fourierDilationCompatibilityDomain_iff_memLp {m : ℕ}
  [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  γ ∈ LeanRidgelet.fourierDilationCompatibilityDomain s t ↔
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume

theorem LeanRidgelet.mem_fourierDilationCompatibilityDomain_iff_memLp
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  γ ∈
      LeanRidgelet.fourierDilationCompatibilityDomain
        s t ↔
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume

Membership in the concrete compatibility domain is exactly Bochner `L²` membership of the
Fourier--dilation core.  The base part is automatically integrable, so only measurability and the
Sobolev graph term remain in the set definition.

theoremdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

theorem LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↑↑((LeanRidgelet.fourierDilationTransform m s t)
          (LeanRidgelet.parameterSchwartzRealization s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.fourierDilationTransformFiber s t γ

theorem LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↑↑((LeanRidgelet.fourierDilationTransform
            m s t)
          (LeanRidgelet.parameterSchwartzRealization
            s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.fourierDilationTransformFiber
      s t γ

defdefined in LeanRidgelet/Transform/FourierDilation.lean

complete

def LeanRidgelet.inverseFourierDilationTransformCore {m : ℕ}
  (u : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) : ℂ

def LeanRidgelet.inverseFourierDilationTransformCore
  {m : ℕ}
  (u :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) : ℂ

Implementation after :=

:=
  (2 * Real.pi : ℂ)⁻¹ *
    ∫ z : InputSpace m × ℝ, u z * inverseFourierDilationKernel p z

The Fourier expression for the inverse coordinate transform on a Schwartz test function.

Definition13

Statement uses 3

Statement dependency previews

Preview

Definition 1

Loading preview

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

used by 1✓L∃∀N

Let m\ge1, s,t\in\mathbb R, \sigma\in\mathcal A_{s,t}, and let T and L_\sigma be Definitions 11 and 8. Define S_\sigma:=\widetilde L_\sigma T:\mathcal G_{s,t}\to L^2(\mathbb R^m),\qquad S_\sigma[\gamma](x):=L_\sigma[T[\gamma](x,\cdot)].

Lean code for Definition13●5 declarations

defdefined in LeanRidgelet/Operator/Synthesis.lean

complete

def LeanRidgelet.networkSynthesis (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.ParameterSpace m s t) →L[ℂ]
    ↥(LeanRidgelet.TargetSpace m)

def LeanRidgelet.networkSynthesis (m : ℕ)
  [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) →L[ℂ]
    ↥(LeanRidgelet.TargetSpace m)

Implementation after :=

:=
  networkSynthesisMap m s t σ

Synthesis associated with an activation coordinate in the transported `T`-coordinate model.

theoremdefined in LeanRidgelet/Operator/Synthesis.lean

complete

theorem LeanRidgelet.networkSynthesis_eq_unitarySynthesis (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.networkSynthesis m s t σ =
    LeanRidgelet.unitarySynthesis MeasureTheory.volume
      (LeanRidgelet.parameterCoordinateEquiv m s t)
      (LeanRidgelet.activationFiberFunctional m s t σ)

theorem LeanRidgelet.networkSynthesis_eq_unitarySynthesis
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.networkSynthesis m s t σ =
    LeanRidgelet.unitarySynthesis
      MeasureTheory.volume
      (LeanRidgelet.parameterCoordinateEquiv
        m s t)
      (LeanRidgelet.activationFiberFunctional
        m s t σ)

The concrete synthesis is the specialization of the abstract unitary factorization to the
transported coordinate model `T = I`.

theoremdefined in LeanRidgelet/Operator/Synthesis.lean

complete

theorem LeanRidgelet.networkSynthesis_apply_fourierDilation_ae (m : ℕ)
  [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  ↑↑((LeanRidgelet.networkSynthesis m s t σ) γ) =ᵐ[MeasureTheory.volume]
    fun x ↦
    (LeanRidgelet.activationFiberFunctional m s t σ)
      (↑↑((LeanRidgelet.fourierDilationTransform m s t) γ) x)

theorem LeanRidgelet.networkSynthesis_apply_fourierDilation_ae
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  ↑↑((LeanRidgelet.networkSynthesis m s t
            σ)
          γ) =ᵐ[MeasureTheory.volume]
    fun x ↦
    (LeanRidgelet.activationFiberFunctional
        m s t σ)
      (↑↑((LeanRidgelet.fourierDilationTransform
                m s t)
              γ)
        x)

Pointwise manuscript factorization `S[γ](x) = L_σ[T[γ](x, ·)]`.

Although the transported coordinate model makes `T` definitionally the identity, this theorem
keeps the unitary transform explicit and is therefore the interface used by the concrete Fourier
construction.

theoremdefined in LeanRidgelet/Operator/Synthesis.lean

complete

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_apply_ae
  {m : ℕ} [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t σ)
          (LeanRidgelet.parameterSchwartzRealization s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    fun x ↦
    (LeanRidgelet.activationFiberFunctional m s t σ)
      (LeanRidgelet.fourierDilationTransformFiber s t γ x)

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_apply_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t
            σ)
          (LeanRidgelet.parameterSchwartzRealization
            s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    fun x ↦
    (LeanRidgelet.activationFiberFunctional
        m s t σ)
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ x)

On the Schwartz compatibility domain, synthesis is represented by the concrete
Fourier--dilation core.  This is the Hilbert-space formula (29) before expanding the activation
functional into its weighted Fourier pairing.

theoremdefined in LeanRidgelet/Operator/Synthesis.lean

complete

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_fourierPairing_ae
  {m : ℕ} [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t σ)
          (LeanRidgelet.parameterSchwartzRealization s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    fun x ↦
    (2 * ↑Real.pi) ^ (m - 1) *
      inner ℂ (star σ)
        (LeanRidgelet.fiberDualCoordinateCoreValue s t
          (LeanRidgelet.fourierDilationTransformFiberCore s t γ x))

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_fourierPairing_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t
            σ)
          (LeanRidgelet.parameterSchwartzRealization
            s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    fun x ↦
    (2 * ↑Real.pi) ^ (m - 1) *
      inner ℂ (star σ)
        (LeanRidgelet.fiberDualCoordinateCoreValue
          s t
          (LeanRidgelet.fourierDilationTransformFiberCore
            s t γ x))

Weighted-Fourier pairing form of synthesis on the Schwartz compatibility domain.

Theorem14

uses 1used by 1✓L∃∀N

Let m\ge1, s,t\in\mathbb R, \sigma\in\mathcal A_{s,t}, and \gamma\in\mathcal G_{s,t}. Then \|S[\gamma]\|_2\le (2\pi)^{m-1}\|\sigma\|_{\mathcal A_{s,t}}\|\gamma\|_{\mathcal G_{s,t}}. In addition, if \gamma lies in the Schwartz compatibility domain, the classical integral is absolutely defined, and the realized activation acts by integration against a function \sigma_{\mathrm{cl}}, then S_\sigma[\gamma](x)=\int\gamma(a,b)\sigma_{\mathrm{cl}}(a\cdot x-b)\,da\,db \quad\text{for a.e. }x.

Lean code for Theorem14●4 declarations

theoremdefined in LeanRidgelet/OverviewL2.lean

complete

theorem LeanRidgelet.l2_theorem_one_bounded_synthesis (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (↑↑((LeanRidgelet.networkSynthesis m s t σ)
            γ) =ᵐ[MeasureTheory.volume]
      fun x ↦
      (LeanRidgelet.activationFiberFunctional m s t σ) (↑↑γ x)) ∧
    ‖(LeanRidgelet.networkSynthesis m s t σ) γ‖ ≤
      (2 * Real.pi) ^ (m - 1) * ‖σ‖ * ‖γ‖

theorem LeanRidgelet.l2_theorem_one_bounded_synthesis
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (↑↑((LeanRidgelet.networkSynthesis m s t
              σ)
            γ) =ᵐ[MeasureTheory.volume]
      fun x ↦
      (LeanRidgelet.activationFiberFunctional
          m s t σ)
        (↑↑γ x)) ∧
    ‖(LeanRidgelet.networkSynthesis m s t
            σ)
          γ‖ ≤
      (2 * Real.pi) ^ (m - 1) * ‖σ‖ * ‖γ‖

Manuscript Theorem 14: coordinate synthesis is pointwise
evaluation and satisfies the concrete bound.

theoremdefined in LeanRidgelet/Operator/Synthesis.lean

complete

theorem LeanRidgelet.norm_networkSynthesis_le (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ‖LeanRidgelet.networkSynthesis m s t σ‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖

theorem LeanRidgelet.norm_networkSynthesis_le
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ‖LeanRidgelet.networkSynthesis m s t
        σ‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖

The concrete operator-norm estimate for synthesis.

defdefined in LeanRidgelet/Operator/ClassicalSynthesis.lean

complete

def LeanRidgelet.classicalSynthesisIntegral {m : ℕ}
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) (σcl : ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m) : ℂ

def LeanRidgelet.classicalSynthesisIntegral
  {m : ℕ}
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (σcl : ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m) : ℂ

Implementation after :=

:=
  ∫ p : InputSpace m × ℝ, γ p * σcl (inner ℝ p.1 x - p.2)

The classical network synthesis integral `x ↦ ∫ γ(a,b) σcl(⟨a,x⟩-b) da db`.

theoremdefined in LeanRidgelet/Operator/ClassicalSynthesis.lean

complete

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_classical_ae
  {m : ℕ} [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  {σcl : ℝ → ℂ}
  (hσcl :
    ∀ (φ : SchwartzMap ℝ ℂ),
      ((LeanRidgelet.activationRealization s t) σ) φ =
        ∫ (z : ℝ), φ z * σcl z)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume)
  (hint :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable (fun p ↦ γ p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t σ)
          (LeanRidgelet.parameterSchwartzRealization s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.classicalSynthesisIntegral γ σcl

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_classical_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  {σcl : ℝ → ℂ}
  (hσcl :
    ∀ (φ : SchwartzMap ℝ ℂ),
      ((LeanRidgelet.activationRealization
              s t)
            σ)
          φ =
        ∫ (z : ℝ), φ z * σcl z)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume)
  (hint :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable
        (fun p ↦
          γ p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t
            σ)
          (LeanRidgelet.parameterSchwartzRealization
            s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.classicalSynthesisIntegral
      γ σcl

**Agreement with the classical synthesis integral** (manuscript Theorem 14, `thm:bdd.S`,
classical part).  Let `σ` be an activation coordinate whose realized classical activation
`σ = 𝓕⁻¹_paper[σ♯]` acts on test functions by integration against `σcl`, and let `γ` be a
Schwartz parameter distribution in the compatibility domain.  If the classical integral is
defined at every input, then the Hilbert-space synthesis operator is represented almost
everywhere by the classical network integral `∫ γ(a,b) σcl(⟨a,x⟩-b) da db`.

Section 4: Neural-Network Specialization: Ridgelet Reconstruction from the Fourier Expression

Definition15

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 16

Loading preview

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

✓L∃∀N

Let m\ge1, s,t\in\mathbb R, h\in\mathcal H_{s,t}, and f\in L^2(\mathbb R^m). Define R_h[f]:=T^*[f\otimes h],\qquad \rho_h^\sharp:=|\omega|^m\overline h, \qquad \rho_h:=\mathcal F^{-1}[\rho_h^\sharp]. The spectrum identity holds pointwise on the Schwartz core and distributionally on the completion. For Schwartz h, the distribution \rho_h is represented by a function, and its classical ridgelet transform is R[f;\rho_h](a,b):=\int f(x)\overline{\rho_h(a\cdot x-b)}\,dx.

Lean code for Definition15●10 declarations

defdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

def LeanRidgelet.ridgeletOperator (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t) :
  ↥(LeanRidgelet.TargetSpace m) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

def LeanRidgelet.ridgeletOperator (m : ℕ)
  [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t) :
  ↥(LeanRidgelet.TargetSpace m) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

Implementation after :=

:=
  fiberRidgelet volume h

The simple-tensor operator `J_h` in the transported unitary-coordinate model.

The name `ridgeletOperator` is retained for API compatibility; on the original parameter space
the corresponding operator is `R_h = T* J_h`.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.ridgeletOperator_eq_unitaryRidgelet (m : ℕ) [NeZero m]
  (s t : ℝ) (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.ridgeletOperator m s t h =
    LeanRidgelet.unitaryRidgelet MeasureTheory.volume
      (LeanRidgelet.parameterCoordinateEquiv m s t) h

theorem LeanRidgelet.ridgeletOperator_eq_unitaryRidgelet
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.ridgeletOperator m s t h =
    LeanRidgelet.unitaryRidgelet
      MeasureTheory.volume
      (LeanRidgelet.parameterCoordinateEquiv
        m s t)
      h

The concrete ridgelet operator is the abstract `R_h = T* J_h` specialized to the transported
coordinate model `T = I`.

defdefined in LeanRidgelet/Space/Duality.lean

complete

def LeanRidgelet.fiberBaseCoordinate (m : ℕ) [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L[ℂ]
    ↥(LeanRidgelet.L2 ℝ MeasureTheory.volume)

def LeanRidgelet.fiberBaseCoordinate (m : ℕ)
  [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L[ℂ]
    ↥(LeanRidgelet.L2 ℝ
        MeasureTheory.volume)

Implementation after :=

:=
  (fiberBaseCoordinateCoreL m s t).extend
    (UniformSpace.Completion.toComplL : FiberCore m s t →L[ℂ] FiberSpace m s t)

The square-root weighted coordinate, extended to the completed fiber Hilbert space.

defdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

def LeanRidgelet.ridgeletSpectrum (m : ℕ) [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L⋆[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.ridgeletSpectrum (m : ℕ)
  [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L⋆[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:= ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ)
    (SchwartzMap ℝ ℂ) ℂ
      ((innerSL ℂ (fiberBaseCoordinate m s t h)).comp
        (fiberBaseCoordinateSchwartz m))
  map_add' h r := by
    ext φ
    change inner ℂ
        (fiberBaseCoordinate m s t (h + r))
        (fiberBaseCoordinateSchwartz m φ) =
      inner ℂ (fiberBaseCoordinate m s t h) (fiberBaseCoordinateSchwartz m φ) +
        inner ℂ (fiberBaseCoordinate m s t r) (fiberBaseCoordinateSchwartz m φ)
    rw [map_add, inner_add_left]
  map_smul' c h := by
    ext φ
    simp
  cont := by
    apply PointwiseConvergenceCLM.continuous_of_continuous_eval
    intro φ
    exact (innerSLFlip ℂ (fiberBaseCoordinateSchwartz m φ)).continuous.comp
      (fiberBaseCoordinate m s t).continuous

The manuscript spectrum `ρ♯ = |ω|ᵐ conj h` for a completed coefficient vector.

The formula is realized through the `L²` pairing of square-root weighted coordinates.  This avoids
the invalid intermediate operation of multiplying an arbitrary tempered distribution by the
nonsmooth function `|ω|ᵐ` in odd dimensions.  The dependence on `h` is conjugate-linear, as in the
manuscript formula.

theoremdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

theorem LeanRidgelet.ridgeletSpectrum_coe (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.ridgeletSpectrum m s t) ↑h =
    LeanRidgelet.ridgeletSpectrumCore m h.toSchwartz

theorem LeanRidgelet.ridgeletSpectrum_coe (m : ℕ)
  [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.ridgeletSpectrum m s t)
      ↑h =
    LeanRidgelet.ridgeletSpectrumCore m
      h.toSchwartz

The completed spectrum agrees with the pointwise `|ω|ᵐ conj h` formula on the dense Schwartz
core.

defdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

def LeanRidgelet.ridgeletFunction (m : ℕ) [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L⋆[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.ridgeletFunction (m : ℕ)
  [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L⋆[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:= paperFourierInvDistribution (ridgeletSpectrum m s t h)
  map_add' h r := by simp
  map_smul' c h := by simp
  cont := paperFourierInvDistribution.continuous.comp (ridgeletSpectrum m s t).continuous

Reconstruct the ridgelet function `ρ` from a completed coefficient vector `h` by applying the
manuscript inverse Fourier transform to `ρ♯`.

theoremdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

theorem LeanRidgelet.paperFourierDistribution_ridgeletFunction (m : ℕ)
  [NeZero m] (s t : ℝ) (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.Fourier.paperFourierDistribution
      ((LeanRidgelet.ridgeletFunction m s t) h) =
    (LeanRidgelet.ridgeletSpectrum m s t) h

theorem LeanRidgelet.paperFourierDistribution_ridgeletFunction
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.Fourier.paperFourierDistribution
      ((LeanRidgelet.ridgeletFunction m s
          t)
        h) =
    (LeanRidgelet.ridgeletSpectrum m s t)
      h

The reconstructed completed ridgelet function has spectrum `ρ♯`.

defdefined in LeanRidgelet/Operator/ClassicalRidgelet.lean

complete

def LeanRidgelet.classicalRidgeletFunction (m : ℕ) (h : SchwartzMap ℝ ℂ)
  (z : ℝ) : ℂ

def LeanRidgelet.classicalRidgeletFunction
  (m : ℕ) (h : SchwartzMap ℝ ℂ) (z : ℝ) :
  ℂ

Implementation after :=

:=
  (2 * Real.pi : ℂ)⁻¹ *
    ∫ ω : ℝ, ridgeletSpectrumCoreFn m h ω * Complex.exp (Complex.I * (z * ω))

The classical ridgelet function `ρ = 𝓕⁻¹_paper[ρ♯]` of a Schwartz coefficient vector,
with manuscript spectrum `ρ♯(ω) = |ω|^m conj h(ω)`.

defdefined in LeanRidgelet/Operator/ClassicalRidgelet.lean

complete

def LeanRidgelet.classicalRidgeletIntegral {m : ℕ}
  (f : LeanRidgelet.InputSpace m → ℂ) (ρ : ℝ → ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) : ℂ

def LeanRidgelet.classicalRidgeletIntegral
  {m : ℕ}
  (f : LeanRidgelet.InputSpace m → ℂ)
  (ρ : ℝ → ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) : ℂ

Implementation after :=

:=
  ∫ x : InputSpace m, f x * conj (ρ (inner ℝ p.1 x - p.2))

The classical ridgelet transform `R[f;ρ](a,b) = ∫ f(x) conj(ρ(⟨a,x⟩-b)) dx`.

theoremdefined in LeanRidgelet/Operator/ClassicalRidgelet.lean

complete

theorem LeanRidgelet.ridgeletFunctionCore_apply_classical (m : ℕ)
  (h φ : SchwartzMap ℝ ℂ) :
  (LeanRidgelet.ridgeletFunctionCore m h) φ =
    ∫ (z : ℝ), φ z * LeanRidgelet.classicalRidgeletFunction m h z

theorem LeanRidgelet.ridgeletFunctionCore_apply_classical
  (m : ℕ) (h φ : SchwartzMap ℝ ℂ) :
  (LeanRidgelet.ridgeletFunctionCore m h)
      φ =
    ∫ (z : ℝ),
      φ z *
        LeanRidgelet.classicalRidgeletFunction
          m h z

The repository ridgelet distribution `ρ = 𝓕⁻¹_paper[ρ♯]` acts on test functions by
integration against the classical ridgelet function.  This identifies
`classicalRidgeletFunction` as the pointwise realization of `ridgeletFunctionCore`.

Lemma16

Statement uses 5

Statement dependency previews

Preview

Theorem 14

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 17

Loading preview

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

✓L∃∀N

Let m\ge1, s,t\in\mathbb R, h\in\mathcal H_{s,t}, and f\in L^2(\mathbb R^m). Then T[R_h[f]](x)=f(x)h\quad\text{for a.e. }x. If f and h are Schwartz and the classical ridgelet integral of Definition 15 is integrable, then for every (a,b) it equals \frac1{2\pi}\int f(x)h(\omega)e^{-i\omega(a\cdot x-b)}|\omega|^m\,dx\,d\omega. The separate bias/input Fourier formulas (32)--(33) are not asserted here.

Lean code for Lemma16●4 theorems

theoremdefined in LeanRidgelet/OverviewL2.lean

complete

theorem LeanRidgelet.l2_lemma_one_ridgelet_fiber_representation (m : ℕ)
  [NeZero m] (s t : ℝ) (h : LeanRidgelet.FiberSpace m s t)
  (f : ↥(LeanRidgelet.TargetSpace m)) :
  ↑↑((LeanRidgelet.ridgeletOperator m s t h) f) =ᵐ[MeasureTheory.volume]
    fun x ↦ ↑↑f x • h

theorem LeanRidgelet.l2_lemma_one_ridgelet_fiber_representation
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t)
  (f : ↥(LeanRidgelet.TargetSpace m)) :
  ↑↑((LeanRidgelet.ridgeletOperator m s t
            h)
          f) =ᵐ[MeasureTheory.volume]
    fun x ↦ ↑↑f x • h

Manuscript Lemma 16: the formalized coordinate representation is a
simple tensor.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae (m : ℕ)
  [NeZero m] (s t : ℝ) (h : LeanRidgelet.FiberSpace m s t)
  (f : ↥(LeanRidgelet.TargetSpace m)) :
  ↑↑((LeanRidgelet.fourierDilationTransform m s t)
          ((LeanRidgelet.ridgeletOperator m s t h)
            f)) =ᵐ[MeasureTheory.volume]
    fun x ↦ ↑↑f x • h

theorem LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t)
  (f : ↥(LeanRidgelet.TargetSpace m)) :
  ↑↑((LeanRidgelet.fourierDilationTransform
            m s t)
          ((LeanRidgelet.ridgeletOperator
              m s t h)
            f)) =ᵐ[MeasureTheory.volume]
    fun x ↦ ↑↑f x • h

The concrete form of `T[R_h[f]] = f ⊗ h`, corresponding to equation (34).

theoremdefined in LeanRidgelet/Operator/ClassicalRidgelet.lean

complete

theorem LeanRidgelet.classicalRidgeletIntegral_eq_inverseTensorIntegral {m : ℕ}
  (f : SchwartzMap (LeanRidgelet.InputSpace m) ℂ) (h : SchwartzMap ℝ ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral (⇑f)
      (LeanRidgelet.classicalRidgeletFunction m h) p =
    (2 * ↑Real.pi)⁻¹ *
      ∫ (z : LeanRidgelet.InputSpace m × ℝ),
        f z.1 * h z.2 * LeanRidgelet.inverseFourierDilationKernel p z

theorem LeanRidgelet.classicalRidgeletIntegral_eq_inverseTensorIntegral
  {m : ℕ}
  (f :
    SchwartzMap
      (LeanRidgelet.InputSpace m) ℂ)
  (h : SchwartzMap ℝ ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral
      (⇑f)
      (LeanRidgelet.classicalRidgeletFunction
        m h)
      p =
    (2 * ↑Real.pi)⁻¹ *
      ∫ (z :
        LeanRidgelet.InputSpace m × ℝ),
        f z.1 * h z.2 *
          LeanRidgelet.inverseFourierDilationKernel
            p z

**Agreement with the classical ridgelet integral** (manuscript Definition of `R[f;ρ]` and
Lemma `lem:fourier`, classical part).  For a Schwartz function `f` and a Schwartz coefficient
vector `h`, the classical ridgelet transform with respect to the classical ridgelet function of
spectrum `|ω|^m conj h` equals, at every parameter point, the inverse-coordinate integral
formula (13) applied to the tensor section `(x,ω) ↦ f(x) h(ω)` — the coordinate representative
of `T[R_h[f]]`.

theoremdefined in LeanRidgelet/Operator/ClassicalRidgelet.lean

complete

theorem LeanRidgelet.classicalRidgeletIntegral_eq_inverseFourierDilationTransformCore
  {m : ℕ} (f : SchwartzMap (LeanRidgelet.InputSpace m) ℂ)
  (h : SchwartzMap ℝ ℂ)
  (u : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hu : ∀ (z : LeanRidgelet.InputSpace m × ℝ), u z = f z.1 * h z.2)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral (⇑f)
      (LeanRidgelet.classicalRidgeletFunction m h) p =
    LeanRidgelet.inverseFourierDilationTransformCore u p

theorem LeanRidgelet.classicalRidgeletIntegral_eq_inverseFourierDilationTransformCore
  {m : ℕ}
  (f :
    SchwartzMap
      (LeanRidgelet.InputSpace m) ℂ)
  (h : SchwartzMap ℝ ℂ)
  (u :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hu :
    ∀ (z : LeanRidgelet.InputSpace m × ℝ),
      u z = f z.1 * h z.2)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral
      (⇑f)
      (LeanRidgelet.classicalRidgeletFunction
        m h)
      p =
    LeanRidgelet.inverseFourierDilationTransformCore
      u p

The classical ridgelet integral agrees with the inverse coordinate-transform formula (13)
on any Schwartz representative of the tensor section `(x,ω) ↦ f(x) h(ω)`.

Theorem17

Statement uses 2

Statement dependency previews

Preview

Theorem 2

Loading preview

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

used by 0✓L∃∀N

Let m\ge1, s,t\in\mathbb R, \sigma\in\mathcal A_{s,t}, and h\in\mathcal H_{s,t}. Then S_\sigma\circ R_h=L_\sigma[h]I, that is, S_\sigma[R_h[f]]=L_\sigma[h]f for every f\in L^2(\mathbb R^m). If a classical ridgelet function \rho has h=|\omega|^{-m}\overline{\rho^\sharp}, this becomes S_\sigma[R[f;\rho]]=\langle\!\langle\sigma,\rho\rangle\!\rangle f; bundling the forward map \rho\mapsto h remains outside the current statement.

Lean code for Theorem17●2 theorems

theoremdefined in LeanRidgelet/OverviewL2.lean

complete

theorem LeanRidgelet.l2_theorem_two_reconstruction (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.networkSynthesis m s t σ ∘SL
      LeanRidgelet.ridgeletOperator m s t h =
    (LeanRidgelet.activationFiberFunctional m s t σ) h •
      ContinuousLinearMap.id ℂ ↥(LeanRidgelet.TargetSpace m)

theorem LeanRidgelet.l2_theorem_two_reconstruction
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.networkSynthesis m s t
        σ ∘SL
      LeanRidgelet.ridgeletOperator m s t
        h =
    (LeanRidgelet.activationFiberFunctional
          m s t σ)
        h •
      ContinuousLinearMap.id ℂ
        ↥(LeanRidgelet.TargetSpace m)

Manuscript Theorem 17: synthesis after a prescribed
coefficient is scalar reconstruction.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.networkSynthesis_comp_ridgeletOperator (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.networkSynthesis m s t σ ∘SL
      LeanRidgelet.ridgeletOperator m s t h =
    (LeanRidgelet.activationFiberFunctional m s t σ) h •
      ContinuousLinearMap.id ℂ ↥(LeanRidgelet.TargetSpace m)

theorem LeanRidgelet.networkSynthesis_comp_ridgeletOperator
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.networkSynthesis m s t
        σ ∘SL
      LeanRidgelet.ridgeletOperator m s t
        h =
    (LeanRidgelet.activationFiberFunctional
          m s t σ)
        h •
      ContinuousLinearMap.id ℂ
        ↥(LeanRidgelet.TargetSpace m)

Coordinate reconstruction `\widetilde L_σ J_h = L_σ[h] I`.

Section 5: Neural-Network Specialization: Adjoint, Null Space, and Complete General Solution

Definition18

Statement uses 2

Statement dependency previews

Preview

Definition 8

Loading preview

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

used by 1✓L∃∀N

Let m\ge1, s,t\in\mathbb R, and \sigma\in\mathcal A_{s,t}. Define the Riesz vector h_\sigma\in\mathcal H_{s,t} and normalization c_\sigma by L_\sigma[h]=\langle h,h_\sigma\rangle,\qquad c_\sigma:=\|h_\sigma\|^2=\|L_\sigma\|^2. Define the adjoint ridgelet distribution \sigma_*:=\rho_{h_\sigma}; equivalently, \sigma_*^\sharp=|\omega|^m\overline{h_\sigma}.

Lean code for Definition18●4 declarations

defdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

def LeanRidgelet.activationRieszRepresenter (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.FiberSpace m s t

def LeanRidgelet.activationRieszRepresenter
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.FiberSpace m s t

Implementation after :=

:=
  rieszRepresenter (activationFiberFunctional m s t σ)

The Riesz representer `h_σ` associated with an activation functional.

defdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

def LeanRidgelet.activationNormalization (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) : ℝ

def LeanRidgelet.activationNormalization
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ℝ

Implementation after :=

:=
  fiberNormalization (activationFiberFunctional m s t σ)

The normalization constant `cσ = ‖hσ‖²`.

defdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

def LeanRidgelet.ridgeletFunction (m : ℕ) [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L⋆[ℂ] TemperedDistribution ℝ ℂ

def LeanRidgelet.ridgeletFunction (m : ℕ)
  [NeZero m] (s t : ℝ) :
  LeanRidgelet.FiberSpace m s t →L⋆[ℂ]
    TemperedDistribution ℝ ℂ

Implementation after :=

:= paperFourierInvDistribution (ridgeletSpectrum m s t h)
  map_add' h r := by simp
  map_smul' c h := by simp
  cont := paperFourierInvDistribution.continuous.comp (ridgeletSpectrum m s t).continuous

Reconstruct the ridgelet function `ρ` from a completed coefficient vector `h` by applying the
manuscript inverse Fourier transform to `ρ♯`.

theoremdefined in LeanRidgelet/Space/RidgeletFunction.lean

complete

theorem LeanRidgelet.paperFourierDistribution_ridgeletFunction (m : ℕ)
  [NeZero m] (s t : ℝ) (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.Fourier.paperFourierDistribution
      ((LeanRidgelet.ridgeletFunction m s t) h) =
    (LeanRidgelet.ridgeletSpectrum m s t) h

theorem LeanRidgelet.paperFourierDistribution_ridgeletFunction
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberSpace m s t) :
  LeanRidgelet.Fourier.paperFourierDistribution
      ((LeanRidgelet.ridgeletFunction m s
          t)
        h) =
    (LeanRidgelet.ridgeletSpectrum m s t)
      h

The reconstructed completed ridgelet function has spectrum `ρ♯`.

Lemma19

Statement uses 2

Statement dependency previews

Preview

Theorem 2

Loading preview

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

used by 1✓L∃∀N

Under Definition 18, for every f\in L^2(\mathbb R^m), S_\sigma^*=R_{h_\sigma},\qquad S_\sigma S_\sigma^*=c_\sigma I,\qquad \|S_\sigma^*[f]\|^2=c_\sigma\|f\|^2. With \sigma_* from Definition 18, the first identity is equivalently S_\sigma^*[f]=R[f;\sigma_*].

Lean code for Lemma19●3 theorems

theoremdefined in LeanRidgelet/OverviewL2.lean

complete

theorem LeanRidgelet.l2_lemma_two_adjoint (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ContinuousLinearMap.adjoint (LeanRidgelet.networkSynthesis m s t σ) =
      LeanRidgelet.ridgeletOperator m s t
        (LeanRidgelet.activationRieszRepresenter m s t σ) ∧
    LeanRidgelet.networkSynthesis m s t σ ∘SL
        ContinuousLinearMap.adjoint
          (LeanRidgelet.networkSynthesis m s t σ) =
      ↑(LeanRidgelet.activationNormalization m s t σ) •
        ContinuousLinearMap.id ℂ ↥(LeanRidgelet.TargetSpace m)

theorem LeanRidgelet.l2_lemma_two_adjoint (m : ℕ)
  [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ContinuousLinearMap.adjoint
        (LeanRidgelet.networkSynthesis m s
          t σ) =
      LeanRidgelet.ridgeletOperator m s t
        (LeanRidgelet.activationRieszRepresenter
          m s t σ) ∧
    LeanRidgelet.networkSynthesis m s t
          σ ∘SL
        ContinuousLinearMap.adjoint
          (LeanRidgelet.networkSynthesis m
            s t σ) =
      ↑(LeanRidgelet.activationNormalization
            m s t σ) •
        ContinuousLinearMap.id ℂ
          ↥(LeanRidgelet.TargetSpace m)

Manuscript Lemma 19: the adjoint uses the Riesz representer and
satisfies the scaled coisometry identity.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.adjoint_networkSynthesis (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ContinuousLinearMap.adjoint (LeanRidgelet.networkSynthesis m s t σ) =
    LeanRidgelet.ridgeletOperator m s t
      (LeanRidgelet.activationRieszRepresenter m s t σ)

theorem LeanRidgelet.adjoint_networkSynthesis
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ContinuousLinearMap.adjoint
      (LeanRidgelet.networkSynthesis m s t
        σ) =
    LeanRidgelet.ridgeletOperator m s t
      (LeanRidgelet.activationRieszRepresenter
        m s t σ)

The adjoint synthesis operator is represented in coordinates by `J_{h_σ}`.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.networkSynthesis_comp_adjoint (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.networkSynthesis m s t σ ∘SL
      ContinuousLinearMap.adjoint
        (LeanRidgelet.networkSynthesis m s t σ) =
    ↑(LeanRidgelet.activationNormalization m s t σ) •
      ContinuousLinearMap.id ℂ ↥(LeanRidgelet.TargetSpace m)

theorem LeanRidgelet.networkSynthesis_comp_adjoint
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  LeanRidgelet.networkSynthesis m s t
        σ ∘SL
      ContinuousLinearMap.adjoint
        (LeanRidgelet.networkSynthesis m s
          t σ) =
    ↑(LeanRidgelet.activationNormalization
          m s t σ) •
      ContinuousLinearMap.id ℂ
        ↥(LeanRidgelet.TargetSpace m)

Synthesis composed with its adjoint is multiplication by `cσ`.

Definition20

Statement uses 2

Statement dependency previews

Preview

Theorem 3

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 21

Loading preview

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

✓L∃∀N

Let \sigma\in\mathcal A_{s,t} satisfy \sigma\ne0. Define S_\sigma^\dagger:=c_\sigma^{-1}S_\sigma^*,\qquad P_\sigma:=S_\sigma^\dagger S_\sigma. Then S_\sigma S_\sigma^\dagger=I and P_\sigma^*=P_\sigma.

Lean code for Definition20●4 declarations

defdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

def LeanRidgelet.normalizedNetworkRightInverse (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.TargetSpace m) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

def LeanRidgelet.normalizedNetworkRightInverse
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.TargetSpace m) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

Implementation after :=

:=
  normalizedRightInverse volume (activationFiberFunctional m s t σ)

The normalized Hilbert adjoint `c_σ⁻¹ S*`, giving the Moore--Penrose right inverse.

defdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

def LeanRidgelet.networkVisibleProjection (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.ParameterSpace m s t) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

def LeanRidgelet.networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

Implementation after :=

:=
  visibleProjection volume (activationFiberFunctional m s t σ)

The canonical orthogonal parameter projection `P = S^\dagger S`.

The name `networkVisibleProjection` is retained for API compatibility.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.normalizedNetworkRightInverse_rightInverse (m : ℕ)
  [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  Function.RightInverse
    ⇑(LeanRidgelet.normalizedNetworkRightInverse m s t σ)
    ⇑(LeanRidgelet.networkSynthesis m s t σ)

theorem LeanRidgelet.normalizedNetworkRightInverse_rightInverse
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  Function.RightInverse
    ⇑(LeanRidgelet.normalizedNetworkRightInverse
        m s t σ)
    ⇑(LeanRidgelet.networkSynthesis m s t
        σ)

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.isSelfAdjoint_networkVisibleProjection (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  IsSelfAdjoint (LeanRidgelet.networkVisibleProjection m s t σ)

theorem LeanRidgelet.isSelfAdjoint_networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  IsSelfAdjoint
    (LeanRidgelet.networkVisibleProjection
      m s t σ)

Theorem21

Statement uses 3

Statement dependency previews

Preview

Theorem 4

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Corollary 24

Loading preview

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

✓L∃∀N

Let \sigma\in\mathcal A_{s,t} satisfy \sigma\ne0, let (e_i)_{i\in I} be a Hilbert basis of L^2(\mathbb R^m), and let \gamma\in\mathcal G_{s,t}. Then \gamma\in\ker S_\sigma\iff L_\sigma[T[\gamma](x,\cdot)]=0\ \text{for a.e. }x \iff(\forall i)\;h_i[\gamma]\in\ker L_\sigma, and \gamma=\sum_iR_{h_i[\gamma]}[e_i] with unique coefficient vectors. For f\in L^2(\mathbb R^m), all solutions are exactly \{\gamma:S_\sigma[\gamma]=f\}=S_\sigma^\dagger[f]+\ker S_\sigma, and S_\sigma^\dagger[f] is the unique minimum-norm solution. A Hilbert basis of \ker L_\sigma further gives the double \ell^2 null expansion of Theorem 4.

Lean code for Theorem21●6 theorems

theoremdefined in LeanRidgelet/OverviewL2.lean

complete

theorem LeanRidgelet.l2_theorem_three_null_space_and_general_solution.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m] (s t : ℝ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.TargetSpace m))
  {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker ↔
      ∀ᵐ (x : LeanRidgelet.InputSpace m),
        (LeanRidgelet.activationFiberFunctional m s t σ) (↑↑γ x) = 0) ∧
    HasSum
        (fun i ↦
          (LeanRidgelet.ridgeletOperator m s t
              (LeanRidgelet.fiberCoefficient MeasureTheory.volume (b i)
                γ))
            (b i))
        γ ∧
      (γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker →
          ∀ (i : ι),
            (LeanRidgelet.activationFiberFunctional m s t σ)
                (LeanRidgelet.fiberCoefficient MeasureTheory.volume
                  (b i) γ) =
              0) ∧
        (∀ (h : ι → LeanRidgelet.FiberSpace m s t),
            HasSum
                (fun i ↦
                  (LeanRidgelet.ridgeletOperator m s t (h i)) (b i))
                γ →
              ∀ (i : ι),
                h i =
                  LeanRidgelet.fiberCoefficient MeasureTheory.volume
                    (b i) γ) ∧
          ((LeanRidgelet.networkSynthesis m s t σ) γ = f ↔
              γ -
                  (LeanRidgelet.normalizedNetworkRightInverse m s t σ)
                    f ∈
                (↑(LeanRidgelet.networkSynthesis m s t σ)).ker) ∧
            ∀ (δ : ↥(LeanRidgelet.ParameterSpace m s t)),
              (LeanRidgelet.networkSynthesis m s t σ) δ = f →
                ‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ)
                        f‖ ≤
                    ‖δ‖ ∧
                  (‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ)
                          f‖ =
                      ‖δ‖ →
                    (LeanRidgelet.normalizedNetworkRightInverse m s t σ)
                        f =
                      δ)

theorem LeanRidgelet.l2_theorem_three_null_space_and_general_solution.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m]
  (s t : ℝ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.TargetSpace m))
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (γ ∈
        (↑(LeanRidgelet.networkSynthesis m
              s t σ)).ker ↔
      ∀ᵐ (x : LeanRidgelet.InputSpace m),
        (LeanRidgelet.activationFiberFunctional
              m s t σ)
            (↑↑γ x) =
          0) ∧
    HasSum
        (fun i ↦
          (LeanRidgelet.ridgeletOperator m
              s t
              (LeanRidgelet.fiberCoefficient
                MeasureTheory.volume (b i)
                γ))
            (b i))
        γ ∧
      (γ ∈
            (↑(LeanRidgelet.networkSynthesis
                  m s t σ)).ker →
          ∀ (i : ι),
            (LeanRidgelet.activationFiberFunctional
                  m s t σ)
                (LeanRidgelet.fiberCoefficient
                  MeasureTheory.volume
                  (b i) γ) =
              0) ∧
        (∀
            (h :
              ι →
                LeanRidgelet.FiberSpace m
                  s t),
            HasSum
                (fun i ↦
                  (LeanRidgelet.ridgeletOperator
                      m s t (h i))
                    (b i))
                γ →
              ∀ (i : ι),
                h i =
                  LeanRidgelet.fiberCoefficient
                    MeasureTheory.volume
                    (b i) γ) ∧
          ((LeanRidgelet.networkSynthesis
                    m s t σ)
                  γ =
                f ↔
              γ -
                  (LeanRidgelet.normalizedNetworkRightInverse
                      m s t σ)
                    f ∈
                (↑(LeanRidgelet.networkSynthesis
                      m s t σ)).ker) ∧
            ∀
              (δ :
                ↥(LeanRidgelet.ParameterSpace
                    m s t)),
              (LeanRidgelet.networkSynthesis
                      m s t σ)
                    δ =
                  f →
                ‖(LeanRidgelet.normalizedNetworkRightInverse
                          m s t σ)
                        f‖ ≤
                    ‖δ‖ ∧
                  (‖(LeanRidgelet.normalizedNetworkRightInverse
                            m s t σ)
                          f‖ =
                      ‖δ‖ →
                    (LeanRidgelet.normalizedNetworkRightInverse
                          m s t σ)
                        f =
                      δ)

Manuscript Theorem 21: pointwise nullity, the unique basis expansion,
the complete solution set, and the minimum-norm solution, collected from the coordinate theorems.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation (m : ℕ)
  [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional m s t σ)
          (↑↑((LeanRidgelet.fourierDilationTransform m s t) γ) x) =
        0

theorem LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  γ ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional
            m s t σ)
          (↑↑((LeanRidgelet.fourierDilationTransform
                    m s t)
                  γ)
            x) =
        0

The null-space characterization with the manuscript unitary coordinate transform explicit.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m] (s t : ℝ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  HasSum
    (fun i ↦
      (LeanRidgelet.ridgeletOperator m s t
          (LeanRidgelet.fiberCoefficient MeasureTheory.volume (b i) γ))
        (b i))
    γ

theorem LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m]
  (s t : ℝ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  HasSum
    (fun i ↦
      (LeanRidgelet.ridgeletOperator m s t
          (LeanRidgelet.fiberCoefficient
            MeasureTheory.volume (b i) γ))
        (b i))
    γ

The coefficient-vector series expansion of a parameter distribution.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.networkSolution_iff_kernel_translate (m : ℕ) [NeZero m]
  (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.networkSynthesis m s t σ) γ = f ↔
    γ - (LeanRidgelet.normalizedNetworkRightInverse m s t σ) f ∈
      (↑(LeanRidgelet.networkSynthesis m s t σ)).ker

theorem LeanRidgelet.networkSolution_iff_kernel_translate
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.networkSynthesis m s t σ)
        γ =
      f ↔
    γ -
        (LeanRidgelet.normalizedNetworkRightInverse
            m s t σ)
          f ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker

Every solution is the normalized-adjoint solution plus a null component.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.normalizedNetworkRightInverse_unique_minimal (m : ℕ)
  [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.networkSynthesis m s t σ) γ = f →
    ‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ) f‖ ≤ ‖γ‖ ∧
      (‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ) f‖ = ‖γ‖ →
        (LeanRidgelet.normalizedNetworkRightInverse m s t σ) f = γ)

theorem LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.networkSynthesis m s t σ)
        γ =
      f →
    ‖(LeanRidgelet.normalizedNetworkRightInverse
              m s t σ)
            f‖ ≤
        ‖γ‖ ∧
      (‖(LeanRidgelet.normalizedNetworkRightInverse
                m s t σ)
              f‖ =
          ‖γ‖ →
        (LeanRidgelet.normalizedNetworkRightInverse
              m s t σ)
            f =
          γ)

The normalized-adjoint solution is the unique minimum-norm parameter solution.

theoremdefined in LeanRidgelet/Operator/UnitarySynthesis.lean

complete

theorem LeanRidgelet.hasSum_unitaryRidgelet_kernelBasis.{u_1, u_2, u_3, u_4,
    u_5}
  {α : Type u_1} {H : Type u_2} {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4} {κ : Type u_5}
  (T : G ≃ₗᵢ[ℂ] ↥(LeanRidgelet.BochnerL2 α H μ)) (L : H →L[ℂ] ℂ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.L2 α μ))
  (d : HilbertBasis κ ℂ ↥(↑L).ker) (γ : G)
  (hγ : γ ∈ (↑(LeanRidgelet.unitarySynthesis μ T L)).ker) :
  HasSum
    (fun p ↦
      ↑(LeanRidgelet.unitaryNullDoubleCoefficients μ T L b d γ hγ) p •
        (LeanRidgelet.unitaryRidgelet μ T ↑(d p.2)) (b p.1))
    γ

theorem LeanRidgelet.hasSum_unitaryRidgelet_kernelBasis.{u_1,
    u_2, u_3, u_4, u_5}
  {α : Type u_1} {H : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup G]
  [InnerProductSpace ℂ G] {ι : Type u_4}
  {κ : Type u_5}
  (T :
    G ≃ₗᵢ[ℂ]
      ↥(LeanRidgelet.BochnerL2 α H μ))
  (L : H →L[ℂ] ℂ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.L2 α μ))
  (d : HilbertBasis κ ℂ ↥(↑L).ker) (γ : G)
  (hγ :
    γ ∈
      (↑(LeanRidgelet.unitarySynthesis μ T
            L)).ker) :
  HasSum
    (fun p ↦
      ↑(LeanRidgelet.unitaryNullDoubleCoefficients
              μ T L b d γ hγ)
          p •
        (LeanRidgelet.unitaryRidgelet μ T
            ↑(d p.2))
          (b p.1))
    γ

Every abstract null parameter has the unconditional `I × J` ridgelet expansion associated
with Hilbert bases of `L²(X)` and `ker L`.

Section 6: Examples of Adjoint Ridgelet Functions: ReLU, Sigmoidal, and Gaussian Activations

The manuscript's Example 2 derives one-dimensional weak resolvent formulas for the adjoint ridgelet functions of ReLU, tanh, the Gaussian cumulative distribution function, and the Gaussian density. Lean currently formalizes membership and distributional realizations for several standard activations, but not these explicit Riesz-resolvent formulas.

Section 7: Further Developments: Finite-Width Approximation of Null Elements

Definition22

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 23

Loading preview

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

XL∃∀N

Let \mu be a finite complex Radon measure on parameter space and let \nu be a finite data measure. If the feature map \theta\mapsto\sigma(a\cdot x-b) has finite L^2(\nu) energy with respect to |\mu|, define S_\nu[\mu]:=\int\sigma(a\cdot{\,\cdot\,}-b)\,d\mu(a,b) \in L^2(\nu). This measure-valued domain is distinct from \mathcal G_{s,t}. No Lean declaration is linked because the Radon-measure construction has not yet been formalized.

Theorem23

uses 1used by 1⚠L∃∀N

Let (\Theta,\mu) be a probability space, let H be a complex Hilbert space, and let \Phi:\Theta\to H and u:\Theta\to\mathbb C satisfy |u(\theta)|=1\ \text{a.e.},\qquad \int\|\Phi(\theta)\|^2d\mu(\theta)<\infty,\qquad \int u(\theta)\Phi(\theta)d\mu(\theta)=0. Then for every integer N\ge1 there exist \theta_1,\ldots,\theta_N\in\Theta such that \left\|\frac1N\sum_{j=1}^Nu(\theta_j)\Phi(\theta_j)\right\| \le\sqrt{\frac{\int\|\Phi\|^2d\mu}{N}}. The linked Lean declaration states this Hilbert-valued sampling conclusion. The manuscript's stronger Radon-measure, exact mean-square, and almost-sure convergence assertions are not part of that Lean statement.

Lean code for Theorem23●1 theorem, incomplete

theoremdefined in LeanRidgelet/OverviewL2.lean

contains sorry

theorem LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation.{u_1,
    u_2}
  {Θ : Type u_1} {H : Type u_2} [MeasurableSpace Θ]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (μ : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure μ]
  (Φ : Θ → H) (u : Θ → ℂ) (hu : ∀ᵐ (θ : Θ) ∂μ, ‖u θ‖ = 1)
  (henergy : MeasureTheory.Integrable (fun θ ↦ ‖Φ θ‖ ^ 2) μ)
  (hnull : ∫ (θ : Θ), u θ • Φ θ ∂μ = 0) (N : ℕ) :
  0 < N →
    ∃ θ,
      ‖(↑N)⁻¹ • ∑ j, u (θ j) • Φ (θ j)‖ ≤
        √((∫ (x : Θ), ‖Φ x‖ ^ 2 ∂μ) / ↑N)

theorem LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation.{u_1,
    u_2}
  {Θ : Type u_1} {H : Type u_2}
  [MeasurableSpace Θ]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (μ : MeasureTheory.Measure Θ)
  [MeasureTheory.IsProbabilityMeasure μ]
  (Φ : Θ → H) (u : Θ → ℂ)
  (hu : ∀ᵐ (θ : Θ) ∂μ, ‖u θ‖ = 1)
  (henergy :
    MeasureTheory.Integrable
      (fun θ ↦ ‖Φ θ‖ ^ 2) μ)
  (hnull : ∫ (θ : Θ), u θ • Φ θ ∂μ = 0)
  (N : ℕ) :
  0 < N →
    ∃ θ,
      ‖(↑N)⁻¹ • ∑ j, u (θ j) • Φ (θ j)‖ ≤
        √((∫ (x : Θ), ‖Φ x‖ ^ 2 ∂μ) / ↑N)

Manuscript Theorem 23, in its Hilbert-valued sampling form: a centered
normalized feature distribution has an `N`-term realization with `N⁻¹ᐟ²` output error.

Corollary24

Statement uses 3

Statement dependency previews

Preview

Theorem 21

Loading preview

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

used by 0⚠L∃∀N

Let m\ge1, s,t\in\mathbb R, and let 0\ne\sigma\in\mathcal A_{s,t}. Then there exist 0\ne f\in L^2(\mathbb R^m) and 0\ne h\in\mathcal H_{s,t} such that L_\sigma[h]=0,\qquad R_h[f]\in\ker S_\sigma. This is exactly the coordinate-level conclusion of the linked Lean declaration. The manuscript's additional passage from a Schwartz ridgelet element to a normalized Radon measure, under continuity, polynomial-growth, and compact-support assumptions, remains outside this statement.

Lean code for Corollary24●1 theorem, incomplete

theoremdefined in LeanRidgelet/OverviewL2.lean

contains sorry

theorem LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
  (m : ℕ) [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  ∃ f h,
    f ≠ 0 ∧
      h ≠ 0 ∧
        (LeanRidgelet.activationFiberFunctional m s t σ) h = 0 ∧
          (LeanRidgelet.ridgeletOperator m s t h) f ∈
            (↑(LeanRidgelet.networkSynthesis m s t σ)).ker

theorem LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  ∃ f h,
    f ≠ 0 ∧
      h ≠ 0 ∧
        (LeanRidgelet.activationFiberFunctional
                m s t σ)
              h =
            0 ∧
          (LeanRidgelet.ridgeletOperator m
                s t h)
              f ∈
            (↑(LeanRidgelet.networkSynthesis
                  m s t σ)).ker

Manuscript Corollary 24, at the present coordinate level: a nonzero null ridgelet element exists
and is a candidate for the finite-width discretization theorem.

Proposition25

uses 0used by 0⚠L∃∀N

Let m\ge0, a,x\in\mathbb R^m, and b\in\mathbb R. If \sigma is odd, then \sigma(a\cdot x-b)+\sigma((-a)\cdot x-(-b))=0, and if \sigma is even, the same two terms have difference zero. Moreover, for c_j\in\mathbb R, a_j\in\mathbb R^m, and b_j\in\mathbb R satisfying \sum_jc_ja_j=0,\qquad\sum_jc_jb_j=0, the ReLU features satisfy, for every x, \sum_jc_j\bigl((a_j\cdot x-b_j)_+-((-a_j)\cdot x-(-b_j))_+\bigr)=0. These three algebraic conclusions are the three conjuncts of the linked Lean declaration.

Lean code for Proposition25●1 theorem, incomplete

theoremdefined in LeanRidgelet/OverviewL2.lean

contains sorry

theorem LeanRidgelet.l2_proposition_two_exact_finite_null_relations (m : ℕ) :
  (∀ (σ : ℝ → ℂ),
      (∀ (z : ℝ), σ (-z) = -σ z) →
        ∀ (a x : LeanRidgelet.InputSpace m) (b : ℝ),
          σ (inner ℝ a x - b) + σ (inner ℝ (-a) x - -b) = 0) ∧
    (∀ (σ : ℝ → ℂ),
        (∀ (z : ℝ), σ (-z) = σ z) →
          ∀ (a x : LeanRidgelet.InputSpace m) (b : ℝ),
            σ (inner ℝ a x - b) - σ (inner ℝ (-a) x - -b) = 0) ∧
      ∀ (J : ℕ) (c : Fin J → ℝ) (a : Fin J → LeanRidgelet.InputSpace m)
        (b : Fin J → ℝ),
        ∑ j, c j • a j = 0 →
          ∑ j, c j * b j = 0 →
            ∀ (x : LeanRidgelet.InputSpace m),
              ∑ j,
                  c j *
                    (max (inner ℝ (a j) x - b j) 0 -
                      max (inner ℝ (-a j) x - -b j) 0) =
                0

theorem LeanRidgelet.l2_proposition_two_exact_finite_null_relations
  (m : ℕ) :
  (∀ (σ : ℝ → ℂ),
      (∀ (z : ℝ), σ (-z) = -σ z) →
        ∀
          (a x :
            LeanRidgelet.InputSpace m)
          (b : ℝ),
          σ (inner ℝ a x - b) +
              σ (inner ℝ (-a) x - -b) =
            0) ∧
    (∀ (σ : ℝ → ℂ),
        (∀ (z : ℝ), σ (-z) = σ z) →
          ∀
            (a x :
              LeanRidgelet.InputSpace m)
            (b : ℝ),
            σ (inner ℝ a x - b) -
                σ (inner ℝ (-a) x - -b) =
              0) ∧
      ∀ (J : ℕ) (c : Fin J → ℝ)
        (a :
          Fin J →
            LeanRidgelet.InputSpace m)
        (b : Fin J → ℝ),
        ∑ j, c j • a j = 0 →
          ∑ j, c j * b j = 0 →
            ∀
              (x :
                LeanRidgelet.InputSpace
                  m),
              ∑ j,
                  c j *
                    (max
                        (inner ℝ (a j) x -
                          b j)
                        0 -
                      max
                        (inner ℝ (-a j)
                            x -
                          -b j)
                        0) =
                0

Manuscript Proposition 25: parity and ReLU affine cancellation give
exact finite null relations.

Section 8: Further Developments: Numerical Illustration in Finite Networks

This section is a numerical illustration rather than a formal theorem. It discretizes continuous ridgelet null elements and distinguishes antipodal cancellation from a genuinely nontrivial null relation. No structural result depends on the experiment.

Section 9: Further Developments: Perturbative Readout of Null-Space Information

Theorem26

Statement uses 2

Statement dependency previews

Preview

Definition 20

Loading preview

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

used by 0⚠L∃∀N

Let m\ge1, s,t\in\mathbb R, and let 0\ne\sigma\in\mathcal A_{s,t}. There exist orthonormal (h_i)_{i\in\mathbb N}\subset\ker L_\sigma and activations (\tau_i)_{i\in\mathbb N} satisfying L_{\tau_i}[h_j]=\delta_{ij}. For every f_0\in L^2(\mathbb R^m) and every sequence (f_i) with \sum_i\|f_i\|^2<\infty, there exists \gamma_{\mathrm{enc}}\in\mathcal G_{s,t} such that S_\sigma[\gamma_{\mathrm{enc}}]=f_0,\qquad \gamma_{\mathrm{enc}}-S_\sigma^\dagger[f_0]=\sum_iR_{h_i}[f_i],qquad S_{\tau_i}[\gamma_{\mathrm{enc}}]=f_i. For \delta\gamma_i:=S_\sigma^\dagger[f_i-f_0], one further has S_\sigma[\gamma_{\mathrm{enc}}+\delta\gamma_i]=f_i,qquad (I-P_\sigma)(\gamma_{\mathrm{enc}}+\delta\gamma_i) =(I-P_\sigma)\gamma_{\mathrm{enc}}. These are precisely the existential data and conclusions collected by the linked Lean statement; the manuscript's stronger uniqueness and exact-norm refinements are not asserted there.

Lean code for Theorem26●1 theorem, incomplete

theoremdefined in LeanRidgelet/OverviewL2.lean

contains sorry

theorem LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout (m : ℕ)
  [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  ∃ h τ,
    Orthonormal ℂ h ∧
      (∀ (i : ℕ),
          (LeanRidgelet.activationFiberFunctional m s t σ) (h i) = 0) ∧
        (∀ (i j : ℕ),
            (LeanRidgelet.activationFiberFunctional m s t (τ i)) (h j) =
              if i = j then 1 else 0) ∧
          ∀ (f₀ : ↥(LeanRidgelet.TargetSpace m))
            (f : ℕ → ↥(LeanRidgelet.TargetSpace m)),
            (Summable fun i ↦ ‖f i‖ ^ 2) →
              ∃ γenc,
                HasSum
                    (fun i ↦
                      (LeanRidgelet.ridgeletOperator m s t (h i)) (f i))
                    (γenc -
                      (LeanRidgelet.normalizedNetworkRightInverse m s t
                          σ)
                        f₀) ∧
                  (LeanRidgelet.networkSynthesis m s t σ) γenc = f₀ ∧
                    ∀ (i : ℕ),
                      (LeanRidgelet.networkSynthesis m s t (τ i)) γenc =
                          f i ∧
                        have δγ :=
                          (LeanRidgelet.normalizedNetworkRightInverse m
                              s t σ)
                            (f i - f₀);
                        (LeanRidgelet.networkSynthesis m s t σ)
                              (γenc + δγ) =
                            f i ∧
                          (ContinuousLinearMap.id ℂ
                                  ↥(LeanRidgelet.ParameterSpace m s t) -
                                LeanRidgelet.networkVisibleProjection m
                                  s t σ)
                              (γenc + δγ) =
                            (ContinuousLinearMap.id ℂ
                                  ↥(LeanRidgelet.ParameterSpace m s t) -
                                LeanRidgelet.networkVisibleProjection m
                                  s t σ)
                              γenc

theorem LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  ∃ h τ,
    Orthonormal ℂ h ∧
      (∀ (i : ℕ),
          (LeanRidgelet.activationFiberFunctional
                m s t σ)
              (h i) =
            0) ∧
        (∀ (i j : ℕ),
            (LeanRidgelet.activationFiberFunctional
                  m s t (τ i))
                (h j) =
              if i = j then 1 else 0) ∧
          ∀
            (f₀ :
              ↥(LeanRidgelet.TargetSpace
                  m))
            (f :
              ℕ →
                ↥(LeanRidgelet.TargetSpace
                    m)),
            (Summable fun i ↦ ‖f i‖ ^ 2) →
              ∃ γenc,
                HasSum
                    (fun i ↦
                      (LeanRidgelet.ridgeletOperator
                          m s t (h i))
                        (f i))
                    (γenc -
                      (LeanRidgelet.normalizedNetworkRightInverse
                          m s t σ)
                        f₀) ∧
                  (LeanRidgelet.networkSynthesis
                          m s t σ)
                        γenc =
                      f₀ ∧
                    ∀ (i : ℕ),
                      (LeanRidgelet.networkSynthesis
                              m s t (τ i))
                            γenc =
                          f i ∧
                        have δγ :=
                          (LeanRidgelet.normalizedNetworkRightInverse
                              m s t σ)
                            (f i - f₀);
                        (LeanRidgelet.networkSynthesis
                                m s t σ)
                              (γenc +
                                δγ) =
                            f i ∧
                          (ContinuousLinearMap.id
                                  ℂ
                                  ↥(LeanRidgelet.ParameterSpace
                                      m s
                                      t) -
                                LeanRidgelet.networkVisibleProjection
                                  m s t σ)
                              (γenc +
                                δγ) =
                            (ContinuousLinearMap.id
                                  ℂ
                                  ↥(LeanRidgelet.ParameterSpace
                                      m s
                                      t) -
                                LeanRidgelet.networkVisibleProjection
                                  m s t σ)
                              γenc

Manuscript Theorem 26: countably many null coefficient vectors admit dual
readout activations, giving stable encoding and perturbative readout without changing the null
component.

Section 10: Discussion

This section separates the proved continuous null-space structure, its finite-width traces, and the interpretation of null-space information. It introduces no additional numbered mathematical result.

Section 11: Conclusion

The conclusion summarizes the paper and likewise adds no numbered result.