Lean Ridgelet Blueprint

4. Synthesis, ridgelets, and reconstruction🔗

In Lean statements, the paper expressions S_\sigma[\gamma], R_h[f], R[f;\rho], and L_\sigma[h] can be written S[σ] γ, R[h] f, R[f; ρ] p, and L[σ] h after open scoped LeanRidgelet.Paper. The notation unfolds to the declarations linked below.

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

For an activation \sigma\in\mathcal A_{s,t}, the manuscript factorization is S_\sigma=\widetilde L_\sigma T,\qquad S_\sigma[\gamma](x)=L_\sigma[T[\gamma](x,\cdot)]. The current Lean ParameterSpace is the transported coordinate model, so T=I there and networkSynthesis is definitionally the pointwise lift \widetilde L_\sigma.

Lean code for Definition4.1●4 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_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.
Theorem4.2
uses 0used by 0✓L∃∀N

S_\sigma:\mathcal G_{s,t}\to L^2(\mathbb R^m) is a bounded linear operator, and its operator norm is controlled by the activation--fiber dual bound.

Lean code for Theorem4.2●2 theorems
  • 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.
  • theoremdefined in LeanRidgelet/Operator/Synthesis.lean
    complete
    theorem LeanRidgelet.norm_networkSynthesis_apply_le (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  ‖(LeanRidgelet.networkSynthesis m s t σ) γ‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖ * ‖γ‖
    theorem LeanRidgelet.norm_networkSynthesis_apply_le
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  ‖(LeanRidgelet.networkSynthesis m s t σ)
        γ‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖ * ‖γ‖
    The concrete synthesis estimate evaluated at a parameter distribution.
Theorem4.3
uses 0used by 1✓L∃∀N

The classical integral on the Schwartz compatibility domain, \int\gamma(a,b)\sigma_{\mathrm{cl}}(a\cdot x-b)\,da\,db, agrees almost everywhere with the coordinate synthesis S_\sigma, whenever the classical integral is defined and the realized activation \mathcal F^{-1}[\sigma^\sharp] acts by integration against \sigma_{\mathrm{cl}}. The proof follows the manuscript: 1D Fourier inversion in the preactivation identifies the classical section integral \varphi_x(z)=\int\gamma(a,a\cdot x-z)\,da with (2\pi)^{m-1}(T_{\mathrm{pt}}[\gamma](x,\cdot))^\sharp, and the measure-preserving preactivation shear (a,z)\mapsto(a,a\cdot x-z) performs the final change of variables.

Lean code for Theorem4.3●4 declarations
  • 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`.
  • theoremdefined in LeanRidgelet/Transform/ClassicalSection.lean
    complete
    theorem LeanRidgelet.shearedParameterIntegral_eq_paperFourierSchwartz {m : ℕ}
  [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) (z : ℝ) :
  LeanRidgelet.shearedParameterIntegral γ x z =
    (2 * ↑Real.pi) ^ (m - 1) *
      (LeanRidgelet.Fourier.paperFourierSchwartz
          (LeanRidgelet.fourierDilationTransformFiberCore s t γ
              x).toSchwartz)
        z
    theorem LeanRidgelet.shearedParameterIntegral_eq_paperFourierSchwartz
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m)
  (z : ℝ) :
  LeanRidgelet.shearedParameterIntegral γ
      x z =
    (2 * ↑Real.pi) ^ (m - 1) *
      (LeanRidgelet.Fourier.paperFourierSchwartz
          (LeanRidgelet.fourierDilationTransformFiberCore
              s t γ x).toSchwartz)
        z
    The kernel identity `φ_x(z) = (2π)^{m-1} (T_pt[γ](x,·))♯(z)`: the classical section
integral is the paper Fourier transform of the Fourier--dilation coefficient vector.
  • theoremdefined in LeanRidgelet/Transform/ClassicalSection.lean
    complete
    theorem LeanRidgelet.measurePreserving_preactivationShear {m : ℕ}
  (x : LeanRidgelet.InputSpace m) :
  MeasureTheory.MeasurePreserving (fun p ↦ (p.1, inner ℝ p.1 x - p.2))
    MeasureTheory.volume MeasureTheory.volume
    theorem LeanRidgelet.measurePreserving_preactivationShear
  {m : ℕ}
  (x : LeanRidgelet.InputSpace m) :
  MeasureTheory.MeasurePreserving
    (fun p ↦ (p.1, inner ℝ p.1 x - p.2))
    MeasureTheory.volume
    MeasureTheory.volume
    The preactivation shear preserves Lebesgue measure: it is the identity on the input factor
and a measure-preserving reflection on each bias fiber.
Definition4.4
uses 0used by 0✓L∃∀N

For a fixed h\in\mathcal H_{s,t}, define the coordinate-side tensor embedding by J_h[f](x)=f(x)h. On the original parameter space, the corresponding solution operator is R_h=T^*J_h. The completed vector h has a compatible tempered-distribution realization, agreeing with its Schwartz representative on the dense core. Lean also constructs, continuously and conjugate-linearly for every completed coefficient vector, the ridgelet distribution whose paper-Fourier spectrum is |\omega|^m\overline h; on the Schwartz core this agrees with the pointwise weighted formula.

Lean code for Definition4.4●8 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`.
  • 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.
  • 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 `ρ♯`.
Lemma4.5
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 1.16
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Almost everywhere, the coordinate-side operator is the simple tensor x\mapsto f(x)h.

Lean code for Lemma4.5●2 theorems
  • theoremdefined in LeanRidgelet/Operator/Ridgelet.lean
    complete
    theorem LeanRidgelet.ridgeletOperator_apply_ae (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.ridgeletOperator_apply_ae
  (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
    In unitary coordinates, `J_h[f]` is the simple tensor `x ↦ f(x)h`.
  • 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).
Theorem4.6
uses 1used by 1✓L∃∀N

For Schwartz data, the classical ridgelet transform R[f;\rho](a,b)=\int f(x)\overline{\rho(a\cdot x-b)}\,dx, taken with the classical ridgelet function of spectrum \rho^\sharp=|\omega|^m\overline h, equals at every parameter point the inverse-coordinate integral formula (13) evaluated on the tensor section (x,\omega)\mapsto f(x)h(\omega) that represents T[R_h[f]]. The reconstructed ridgelet distribution acts by integration against the same classical ridgelet function.

Lean code for Theorem4.6●6 declarations
  • 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.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(ω)`.
  • 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`.
  • theoremdefined in LeanRidgelet/Operator/ClassicalRidgelet.lean
    complete
    theorem LeanRidgelet.fourierDilationTransform_ridgeletOperator_toLp_apply_ae
  (m : ℕ) [NeZero m] (s t : ℝ) (h : LeanRidgelet.FiberCore m s t)
  (f : SchwartzMap (LeanRidgelet.InputSpace m) ℂ) :
  ↑↑((LeanRidgelet.fourierDilationTransform m s t)
          ((LeanRidgelet.ridgeletOperator m s t ↑h)
            (f.toLp 2 MeasureTheory.volume))) =ᵐ[MeasureTheory.volume]
    fun x ↦ ↑(f x • h)
    theorem LeanRidgelet.fourierDilationTransform_ridgeletOperator_toLp_apply_ae
  (m : ℕ) [NeZero m] (s t : ℝ)
  (h : LeanRidgelet.FiberCore m s t)
  (f :
    SchwartzMap
      (LeanRidgelet.InputSpace m) ℂ) :
  ↑↑((LeanRidgelet.fourierDilationTransform
            m s t)
          ((LeanRidgelet.ridgeletOperator
              m s t ↑h)
            (f.toLp 2
              MeasureTheory.volume))) =ᵐ[MeasureTheory.volume]
    fun x ↦ ↑(f x • h)
    The tensor section `(x, ω) ↦ f(x) h(ω)` in the inverse-transform integral is the
coordinate representative of the Hilbert-space ridgelet transform: the unitary coordinate of
`ridgeletOperator` at input `x` is the fiber class of the Schwartz function `f x • h`.
Lemma1.16
Statement uses 5
Statement dependency previews
Preview
Theorem 1.14
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 1.17
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N

The bias Fourier transform of the classical ridgelet formula R[f;\rho](a,b)=\int f(x)\overline{\rho(a\cdot x-b)}\,dx and the Fourier representation of synthesis are R[f;\rho]^\sharp(a,\omega)=\widehat f(\omega a)\overline{\rho^\sharp(\omega)} and \widehat{S_\sigma[\gamma]}(\xi)=L_\sigma[T[\gamma](\xi)], respectively. The simple-tensor coordinate representation and the classical-integral agreements are formalized; the two displayed Fourier formulas themselves are still pending.

Theorem4.7
uses 0used by 0✓L∃∀N

For every coefficient vector h, S_\sigma\circ R_h=L_\sigma[h]I. Consequently, if L_\sigma[h]=1 then R_h is a right inverse, while if L_\sigma[h]=0 then its range lies in the null space.

Lean code for Theorem4.7●1 theorem
  • 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`.
Definition4.8
uses 0used by 0✓L∃∀N

By the Riesz representation theorem, the activation has a unique coefficient vector h_\sigma\in\mathcal H_{s,t} satisfying L_\sigma[h]=\langle h,h_\sigma\rangle in the manuscript convention.

Lean code for Definition4.8●1 definition
  • 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.
Definition4.9
uses 0used by 0✓L∃∀N

The manuscript defines the reconstruction constant by c_\sigma=\|h_\sigma\|^2=\|L_\sigma\|^2. Lean identifies the normalization with the squared norm of the Riesz representer; the second equality is the standard isometry of the Riesz representation.

Lean code for Definition4.9●1 definition
  • 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σ‖²`.
Theorem4.10
uses 0used by 0✓L∃∀N

If \sigma\ne0 then L_\sigma\ne0, and hence c_\sigma>0.

Lean code for Theorem4.10●1 theorem
  • theoremdefined in LeanRidgelet/Operator/Ridgelet.lean
    complete
    theorem LeanRidgelet.activationNormalization_pos (m : ℕ) [NeZero m] (s t : ℝ)
  {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0) :
  0 < LeanRidgelet.activationNormalization m s t σ
    theorem LeanRidgelet.activationNormalization_pos
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  0 <
    LeanRidgelet.activationNormalization m
      s t σ
Theorem4.11
uses 0used by 0✓L∃∀N

The Hilbert adjoint of synthesis is the ridgelet operator associated with the Riesz representer, and S_\sigma^*=R_{h_\sigma},\qquad S_\sigma\circ S_\sigma^*=c_\sigma I.

Lean code for Theorem4.11●2 theorems
  • 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σ`.
Definition4.12
uses 0used by 0✓L∃∀N

Define the canonical right inverse to be the normalized adjoint S_\sigma^\dagger=c_\sigma^{-1}S_\sigma^*.

Lean code for Definition4.12●1 definition
  • 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.
Theorem4.13
uses 0used by 0✓L∃∀N

If \sigma\ne0 then S_\sigma\circ S_\sigma^\dagger=I, so synthesis is surjective.

Lean code for Theorem4.13●2 theorems
  • 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.surjective_networkSynthesis (m : ℕ) [NeZero m] (s t : ℝ)
  {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0) :
  Function.Surjective ⇑(LeanRidgelet.networkSynthesis m s t σ)
    theorem LeanRidgelet.surjective_networkSynthesis
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  Function.Surjective
    ⇑(LeanRidgelet.networkSynthesis m s t
        σ)