Lean Ridgelet Blueprint

2. Fourier conventions and Hilbert spaces🔗

This chapter reorganizes the notation from head.tex and the Hilbert-space framework from the arXiv source src/02theory.tex according to the Lean dependency order. The manuscript inner product is linear in the first argument; Mathlib's is linear in the second, so Lean identities use the reversed argument order. In particular, manuscript L[h]=\langle h,h_L\rangle is represented in Lean by \langle h_L,h\rangle=L[h].

The displayed symbols \mathcal A_{s,t}, \mathcal H_{s,t}, \mathcal G_{s,t}, L_\sigma, T, f^\sharp, \langle x\rangle^r, and \langle\partial\rangle^t correspond to the scoped Lean notations 𝓐 s t, 𝓗 m s t, 𝓖 m s t, L[σ], 𝐓, f♯, ⧼x⧽^r, and ⧼∂⧽^t. The linked declarations remain the canonical API.

Definition2.1
uses 0used by 0✓L∃∀N

Let V be a finite-dimensional real inner-product space. Define the paper-normalized Fourier transform by \widehat f(\xi)=\int_V e^{-i\langle x,\xi\rangle}f(x)\,dx. Mathlib's Fourier character uses the 2\pi convention, so rescaling the frequency by \xi/(2\pi) relates the two conventions. Lean also bundles the one-dimensional forward and inverse transforms on tempered distributions and proves that they are mutual inverses.

Lean code for Definition2.1●3 definitions
  • defdefined in LeanRidgelet/Fourier/Convention.lean
    complete
    def LeanRidgelet.Fourier.paperFourierIntegralInner.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  [BorelSpace V] [FiniteDimensional ℝ V] (f : V → ℂ) (ξ : V) : ℂ
    def LeanRidgelet.Fourier.paperFourierIntegralInner.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V] (f : V → ℂ)
  (ξ : V) : ℂ
    Implementation after :=
    :=
  ∫ x, Complex.exp (-Complex.I * (inner ℝ x ξ : ℂ)) * f x
    The manuscript Fourier integral on an arbitrary finite-dimensional real inner-product space.
  • defdefined in LeanRidgelet/Fourier/PaperDistribution.lean
    complete
    def LeanRidgelet.Fourier.paperFourierDistribution :
  TemperedDistribution ℝ ℂ →L[ℂ] TemperedDistribution ℝ ℂ
    def LeanRidgelet.Fourier.paperFourierDistribution :
  TemperedDistribution ℝ ℂ →L[ℂ]
    TemperedDistribution ℝ ℂ
    Implementation after :=
    :=
  temperedDistributionDilation (2 * Real.pi)⁻¹ (inv_ne_zero two_mul_pi_ne_zero) ∘L
    FourierTransform.fourierCLM ℂ (TemperedDistribution ℝ ℂ)
    Fourier transform of a one-dimensional tempered distribution in the manuscript convention
`exp (-i x ω)`.
  • defdefined in LeanRidgelet/Fourier/PaperDistribution.lean
    complete
    def LeanRidgelet.Fourier.paperFourierInvDistribution :
  TemperedDistribution ℝ ℂ →L[ℂ] TemperedDistribution ℝ ℂ
    def LeanRidgelet.Fourier.paperFourierInvDistribution :
  TemperedDistribution ℝ ℂ →L[ℂ]
    TemperedDistribution ℝ ℂ
    Implementation after :=
    :=
  FourierTransform.fourierInvCLM ℂ (TemperedDistribution ℝ ℂ) ∘L
    temperedDistributionDilation (2 * Real.pi) two_mul_pi_ne_zero
    Inverse Fourier transform of a one-dimensional tempered distribution in the manuscript
convention.
Theorem2.2
uses 0used by 0✓L∃∀N

For every Schwartz function f, the paper-normalized Plancherel identity is \|\widehat f\|_{L^2(V)}^2=(2\pi)^{\dim V}\|f\|_{L^2(V)}^2.

Lean code for Theorem2.2●2 theorems
  • theoremdefined in LeanRidgelet/Fourier/Convention.lean
    complete
    theorem LeanRidgelet.Fourier.paper_plancherel_schwartz_inner.{u_1}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  (f : SchwartzMap V ℂ) :
  ∫ (ξ : V),
      ‖LeanRidgelet.Fourier.paperFourierIntegralInner (⇑f) ξ‖ ^ 2 =
    (2 * Real.pi) ^ Module.finrank ℝ V * ∫ (x : V), ‖f x‖ ^ 2
    theorem LeanRidgelet.Fourier.paper_plancherel_schwartz_inner.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V]
  (f : SchwartzMap V ℂ) :
  ∫ (ξ : V),
      ‖LeanRidgelet.Fourier.paperFourierIntegralInner
            (⇑f) ξ‖ ^
        2 =
    (2 * Real.pi) ^ Module.finrank ℝ V *
      ∫ (x : V), ‖f x‖ ^ 2
    Plancherel normalization for the manuscript Fourier convention on any finite-dimensional
real inner-product space.
  • theoremdefined in LeanRidgelet/Fourier/Convention.lean
    complete
    theorem LeanRidgelet.Fourier.paper_plancherel_schwartz {m : ℕ}
  (f : SchwartzMap (LeanRidgelet.InputSpace m) ℂ) :
  ∫ (ξ : LeanRidgelet.InputSpace m),
      ‖LeanRidgelet.Fourier.paperFourierIntegral (⇑f) ξ‖ ^ 2 =
    (2 * Real.pi) ^ m * ∫ (x : LeanRidgelet.InputSpace m), ‖f x‖ ^ 2
    theorem LeanRidgelet.Fourier.paper_plancherel_schwartz
  {m : ℕ}
  (f :
    SchwartzMap
      (LeanRidgelet.InputSpace m) ℂ) :
  ∫ (ξ : LeanRidgelet.InputSpace m),
      ‖LeanRidgelet.Fourier.paperFourierIntegral
            (⇑f) ξ‖ ^
        2 =
    (2 * Real.pi) ^ m *
      ∫ (x : LeanRidgelet.InputSpace m),
        ‖f x‖ ^ 2
    Plancherel normalization in the manuscript convention, first stated for Schwartz functions.
Definition2.3
uses 0used by 0✓L∃∀N

For a real exponent r, define the Japanese bracket power by \langle x\rangle^r=(1+\|x\|^2)^{r/2}.

Lean code for Definition2.3●1 definition
  • defdefined in LeanRidgelet/Space/Activation.lean
    complete
    def LeanRidgelet.japaneseBracketPow.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (r : ℝ) (x : E) : ℝ
    def LeanRidgelet.japaneseBracketPow.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (r : ℝ) (x : E) : ℝ
    Implementation after :=
    :=
  (1 + ‖x‖ ^ 2) ^ (r / 2)
    The Japanese bracket to the power `r`: `⟨x⟩^r = (1 + ‖x‖²)^(r / 2)`.
Definition1.5
uses 0
Used by 2
Reverse dependency previews
Preview
Proposition 1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For s,t\in\mathbb R, the activation Hilbert space \mathcal A_{s,t} is modeled in L^2(\mathbb R) coordinates. The tempered-distribution realization of a coordinate u is \sigma=\langle\cdot\rangle^t\langle\partial\rangle^{-s}[u]. Thus \mathcal A_{s,t} is a coordinate model of \langle\cdot\rangle^tH^s(\mathbb R).

Lean code for Definition1.5●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(ℝ) ⊆ 𝓢'(ℝ)`.
Proposition1.6
uses 1used by 0✓L∃∀N

\mathcal A_{s,t} is a Hilbert space, and its L^2(\mathbb R) coordinate map is a linear isometric equivalence. Its realization in tempered distributions is injective.

Lean code for Proposition1.6●2 declarations
  • defdefined in LeanRidgelet/Space/Activation.lean
    complete
    def LeanRidgelet.activationCoordinateEquiv (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.L2 ℝ MeasureTheory.volume)
    def LeanRidgelet.activationCoordinateEquiv
  (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s
        t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.L2 ℝ
        MeasureTheory.volume)
    Implementation after :=
    :=
  LinearIsometryEquiv.refl ℂ (L2 ℝ volume)
    The activation-space isometry in the transported `L²` coordinate model.
  • theoremdefined in LeanRidgelet/Space/Activation.lean
    complete
    theorem LeanRidgelet.activationDistribution_injective (s t : ℝ) :
  Function.Injective ⇑(LeanRidgelet.activationDistribution s t)
    theorem LeanRidgelet.activationDistribution_injective
  (s t : ℝ) :
  Function.Injective
    ⇑(LeanRidgelet.activationDistribution
        s t)
    The activation-space isometry gives unique `L²` coordinates for realized activations.
Definition2.4
uses 0used by 0✓L∃∀N

Let m>0. On the Schwartz core, set \|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 first term retains the dilation Jacobian, while the weighted Bessel term controls the activation pairing. The fiber space \mathcal H_{s,t} is the Hilbert completion of this core. Lean also realizes every completed coefficient vector as a tempered distribution by undoing its weighted Bessel coordinate; this realization agrees with the original function on the Schwartz core. The square-root dilation-Jacobian coordinate extends contractively to the completion as an L^2 map and supplies the pairing used by the completed ridgelet spectrum.

Lean code for Definition2.4●6 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.
  • 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.
  • theoremdefined in LeanRidgelet/Space/Duality.lean
    complete
    theorem LeanRidgelet.fiberBaseCoordinate_coe (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.fiberBaseCoordinate m s t) ↑h =
    (LeanRidgelet.fiberBaseCoordinateCore m s t) h
    theorem LeanRidgelet.fiberBaseCoordinate_coe
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t) :
  (LeanRidgelet.fiberBaseCoordinate m s t)
      ↑h =
    (LeanRidgelet.fiberBaseCoordinateCore
        m s t)
      h
Proposition2.5
uses 0used by 0✓L∃∀N

The preceding sesquilinear form is positive definite, and the Schwartz core embeds densely into the completed fiber space.

Lean code for Proposition2.5●2 theorems
  • theoremdefined in LeanRidgelet/Space/Fiber.lean
    complete
    theorem LeanRidgelet.fiberInner_self_eq_zero (m : ℕ) (hm : 0 < m) (s t : ℝ)
  (h : SchwartzMap ℝ ℂ) : LeanRidgelet.fiberInner m s t h h = 0 → h = 0
    theorem LeanRidgelet.fiberInner_self_eq_zero
  (m : ℕ) (hm : 0 < m) (s t : ℝ)
  (h : SchwartzMap ℝ ℂ) :
  LeanRidgelet.fiberInner m s t h h = 0 →
    h = 0
  • theoremdefined in LeanRidgelet/Space/Fiber.lean
    complete
    theorem LeanRidgelet.denseRange_fiberCore_coe (m : ℕ) [NeZero m] (s t : ℝ) :
  DenseRange fun h ↦ ↑h
    theorem LeanRidgelet.denseRange_fiberCore_coe
  (m : ℕ) [NeZero m] (s t : ℝ) :
  DenseRange fun h ↦ ↑h
    The Schwartz core has dense image in the completed fiber Hilbert space.
Definition2.6
uses 0used by 0✓L∃∀N

Each \sigma\in\mathcal A_{s,t} induces a continuous linear functional on the coefficient space: L_\sigma[h]=C_m\int_{\mathbb R}h(\omega)\sigma^\sharp(\omega)\,d\omega. For distributional activations, this formula denotes the dual action mediated by the weighted Bessel coordinates.

Lean code for Definition2.6●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.
Theorem2.7
uses 0used by 0✓L∃∀N

L_\sigma is bounded, and the assignment \sigma\mapsto L_\sigma is a continuous linear map from activations to the fiber dual.

Lean code for Theorem2.7●2 declarations
  • theoremdefined in LeanRidgelet/Space/Duality.lean
    complete
    theorem LeanRidgelet.norm_activationFiberFunctional_le (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ‖LeanRidgelet.activationFiberFunctional m s t σ‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖
    theorem LeanRidgelet.norm_activationFiberFunctional_le
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ‖LeanRidgelet.activationFiberFunctional
        m s t σ‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖
    The operator-norm form of the activation--coefficient dual estimate.
  • defdefined in LeanRidgelet/Space/Duality.lean
    complete
    def LeanRidgelet.activationFiberDualMap (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s t) →L[ℂ]
    LeanRidgelet.FiberSpace m s t →L[ℂ] ℂ
    def LeanRidgelet.activationFiberDualMap
  (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ActivationSpace s
        t) →L[ℂ]
    LeanRidgelet.FiberSpace m s t →L[ℂ] ℂ
    Implementation after :=
    :=
  LinearMap.mkContinuous
    { toFun := activationFiberFunctional m s t
      map_add' := activationFiberFunctional_add m s t
      map_smul' := activationFiberFunctional_smul m s t }
    ((2 * Real.pi) ^ (m - 1))
    (norm_activationFiberFunctional_le m s t)
    The continuous linear map `A_{s,t} → H_{s,t}*` induced by the Fourier pairing.
Definition2.8
uses 0used by 0✓L∃∀N

Define the parameter Hilbert space \mathcal G_{s,t} through the unitary coordinates T so that \mathcal G_{s,t}\simeq L^2(\mathbb R^m;\mathcal H_{s,t}). The concrete construction of T uses the full Fourier transform and a weighted dilation. The Lean development currently takes the resulting Bochner L^2 space as its transported coordinate model.

Lean code for Definition2.8●2 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.