6. Standard activation functions🔗

Proposition6.1

uses 0used by 0✓L∃∀N

The Gaussian Fourier coordinate e^{-\omega^2/2} belongs to L^2(\mathbb R) and defines a nonzero activation in \mathcal A_{0,0}.

Lean code for Proposition6.1●2 declarations

defdefined in LeanRidgelet/Activation/Gaussian.lean

complete

def LeanRidgelet.gaussianActivation : ↥(LeanRidgelet.ActivationSpace 0 0)

def LeanRidgelet.gaussianActivation :
  ↥(LeanRidgelet.ActivationSpace 0 0)

Implementation after :=

:=
  memLp_gaussianFourierCoordinateFn.toLp gaussianFourierCoordinateFn

The standard Gaussian as an activation coordinate in `A_{0,0}`.

theoremdefined in LeanRidgelet/Activation/Gaussian.lean

complete

theorem LeanRidgelet.gaussianActivation_ne_zero :
  LeanRidgelet.gaussianActivation ≠ 0

theorem LeanRidgelet.gaussianActivation_ne_zero :
  LeanRidgelet.gaussianActivation ≠ 0

The Gaussian activation coordinate is nonzero.

Proposition6.2

uses 0used by 0✓L∃∀N

If t>1/2, then \langle x\rangle^{-t}\tanh x\in L^2(\mathbb R). The nonzero activation coordinate of \tanh in \mathcal A_{0,t} is the paper Fourier transform (\langle\cdot\rangle^{-t}\tanh)^\sharp = \langle\partial_\omega\rangle^{-t}[\tanh^\sharp], and its pairing-consistent classical realization acts by integration against \tanh.

Lean code for Proposition6.2●5 declarations

theoremdefined in LeanRidgelet/Activation/Tanh.lean

complete

theorem LeanRidgelet.memLp_tanhWeightedFn (t : ℝ) (ht : 1 / 2 < t) :
  MeasureTheory.MemLp (LeanRidgelet.tanhWeightedFn t) 2
    MeasureTheory.volume

theorem LeanRidgelet.memLp_tanhWeightedFn (t : ℝ)
  (ht : 1 / 2 < t) :
  MeasureTheory.MemLp
    (LeanRidgelet.tanhWeightedFn t) 2
    MeasureTheory.volume

defdefined in LeanRidgelet/Activation/Tanh.lean

complete

def LeanRidgelet.tanhActivation (t : ℝ) (ht : 1 / 2 < t) :
  ↥(LeanRidgelet.ActivationSpace 0 t)

def LeanRidgelet.tanhActivation (t : ℝ)
  (ht : 1 / 2 < t) :
  ↥(LeanRidgelet.ActivationSpace 0 t)

Implementation after :=

:=
  paperFourierLp (tanhWeightedCoordinate t ht)

The hyperbolic tangent as an activation coordinate in `A_{0,t}`: the manuscript isometry
coordinate `⟨∂ω⟩^{-t}[tanh♯] = (⟨·⟩⁻ᵗ tanh)♯`, i.e. the paper Fourier transform of the
weighted `L²` element.

theoremdefined in LeanRidgelet/Activation/Tanh.lean

complete

theorem LeanRidgelet.tanhActivation_ne_zero (t : ℝ) (ht : 1 / 2 < t) :
  LeanRidgelet.tanhActivation t ht ≠ 0

theorem LeanRidgelet.tanhActivation_ne_zero
  (t : ℝ) (ht : 1 / 2 < t) :
  LeanRidgelet.tanhActivation t ht ≠ 0

theoremdefined in LeanRidgelet/Activation/Tanh.lean

complete

theorem LeanRidgelet.tanhTemperedDistribution_apply (t : ℝ) (ht : 1 / 2 < t)
  (g : SchwartzMap ℝ ℂ) :
  (LeanRidgelet.tanhTemperedDistribution t ht) g =
    ∫ (x : ℝ), g x * ↑(Real.tanh x)

theorem LeanRidgelet.tanhTemperedDistribution_apply
  (t : ℝ) (ht : 1 / 2 < t)
  (g : SchwartzMap ℝ ℂ) :
  (LeanRidgelet.tanhTemperedDistribution t
        ht)
      g =
    ∫ (x : ℝ), g x * ↑(Real.tanh x)

The distribution realization acts by integration against the classical `tanh` function.

theoremdefined in LeanRidgelet/Activation/Tanh.lean

complete

theorem LeanRidgelet.memActivationSpace_tanhTemperedDistribution (t : ℝ)
  (ht : 1 / 2 < t) :
  LeanRidgelet.MemActivationSpace 0 t
    (LeanRidgelet.tanhTemperedDistribution t ht)

theorem LeanRidgelet.memActivationSpace_tanhTemperedDistribution
  (t : ℝ) (ht : 1 / 2 < t) :
  LeanRidgelet.MemActivationSpace 0 t
    (LeanRidgelet.tanhTemperedDistribution
      t ht)

The realized tanh activation lies in `A_{0,t} = ⟨·⟩ᵗ H⁰(ℝ)`.

Proposition6.3

uses 0used by 0✓L∃∀N

If t>3/2, then \langle x\rangle^{-t}x_+\in L^2(\mathbb R). The nonzero activation coordinate of ReLU in \mathcal A_{0,t} is the paper Fourier transform (\langle\cdot\rangle^{-t}x_+)^\sharp = \langle\partial_\omega\rangle^{-t}[(x_+)^\sharp], and its pairing-consistent classical realization acts by integration against ReLU.

Lean code for Proposition6.3●5 declarations

theoremdefined in LeanRidgelet/Activation/ReLU.lean

complete

theorem LeanRidgelet.memLp_reluWeightedFn (t : ℝ) (ht : 3 / 2 < t) :
  MeasureTheory.MemLp (LeanRidgelet.reluWeightedFn t) 2
    MeasureTheory.volume

theorem LeanRidgelet.memLp_reluWeightedFn (t : ℝ)
  (ht : 3 / 2 < t) :
  MeasureTheory.MemLp
    (LeanRidgelet.reluWeightedFn t) 2
    MeasureTheory.volume

defdefined in LeanRidgelet/Activation/ReLU.lean

complete

def LeanRidgelet.reluActivation (t : ℝ) (ht : 3 / 2 < t) :
  ↥(LeanRidgelet.ActivationSpace 0 t)

def LeanRidgelet.reluActivation (t : ℝ)
  (ht : 3 / 2 < t) :
  ↥(LeanRidgelet.ActivationSpace 0 t)

Implementation after :=

:=
  paperFourierLp (reluWeightedCoordinate t ht)

The rectified linear unit as an activation coordinate in `A_{0,t}`: the manuscript isometry
coordinate `⟨∂ω⟩^{-t}[relu♯] = (⟨·⟩⁻ᵗ relu)♯`, i.e. the paper Fourier transform of the
weighted `L²` element.

theoremdefined in LeanRidgelet/Activation/ReLU.lean

complete

theorem LeanRidgelet.reluActivation_ne_zero (t : ℝ) (ht : 3 / 2 < t) :
  LeanRidgelet.reluActivation t ht ≠ 0

theorem LeanRidgelet.reluActivation_ne_zero
  (t : ℝ) (ht : 3 / 2 < t) :
  LeanRidgelet.reluActivation t ht ≠ 0

theoremdefined in LeanRidgelet/Activation/ReLU.lean

complete

theorem LeanRidgelet.reluTemperedDistribution_apply (t : ℝ) (ht : 3 / 2 < t)
  (g : SchwartzMap ℝ ℂ) :
  (LeanRidgelet.reluTemperedDistribution t ht) g =
    ∫ (x : ℝ), g x * ↑(LeanRidgelet.relu x)

theorem LeanRidgelet.reluTemperedDistribution_apply
  (t : ℝ) (ht : 3 / 2 < t)
  (g : SchwartzMap ℝ ℂ) :
  (LeanRidgelet.reluTemperedDistribution t
        ht)
      g =
    ∫ (x : ℝ),
      g x * ↑(LeanRidgelet.relu x)

The distribution realization acts by integration against the classical ReLU function.

theoremdefined in LeanRidgelet/Activation/ReLU.lean

complete

theorem LeanRidgelet.memActivationSpace_reluTemperedDistribution (t : ℝ)
  (ht : 3 / 2 < t) :
  LeanRidgelet.MemActivationSpace 0 t
    (LeanRidgelet.reluTemperedDistribution t ht)

theorem LeanRidgelet.memActivationSpace_reluTemperedDistribution
  (t : ℝ) (ht : 3 / 2 < t) :
  LeanRidgelet.MemActivationSpace 0 t
    (LeanRidgelet.reluTemperedDistribution
      t ht)

The realized ReLU activation lies in `A_{0,t} = ⟨·⟩ᵗ H⁰(ℝ)`.

Proposition6.4

uses 0used by 0✓L∃∀N

For t>1/2, tanh synthesis is surjective and admits an adjoint ridgelet operator, a complete description of its solutions, and a unique minimum-norm solution.

Lean code for Proposition6.4●3 theorems

theoremdefined in LeanRidgelet/Operator/Tanh.lean

complete

theorem LeanRidgelet.surjective_tanhSynthesis (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 1 / 2 < t) :
  Function.Surjective ⇑(LeanRidgelet.tanhSynthesis m t ht)

theorem LeanRidgelet.surjective_tanhSynthesis
  (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 1 / 2 < t) :
  Function.Surjective
    ⇑(LeanRidgelet.tanhSynthesis m t ht)

theoremdefined in LeanRidgelet/Operator/Tanh.lean

complete

theorem LeanRidgelet.adjoint_tanhSynthesis (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 1 / 2 < t) :
  ContinuousLinearMap.adjoint (LeanRidgelet.tanhSynthesis m t ht) =
    LeanRidgelet.ridgeletOperator m 0 t
      (LeanRidgelet.tanhRieszRepresenter m t ht)

theorem LeanRidgelet.adjoint_tanhSynthesis (m : ℕ)
  [NeZero m] (t : ℝ) (ht : 1 / 2 < t) :
  ContinuousLinearMap.adjoint
      (LeanRidgelet.tanhSynthesis m t
        ht) =
    LeanRidgelet.ridgeletOperator m 0 t
      (LeanRidgelet.tanhRieszRepresenter m
        t ht)

theoremdefined in LeanRidgelet/Operator/Tanh.lean

complete

theorem LeanRidgelet.tanhSolution_iff_kernel_translate (m : ℕ) [NeZero m]
  (t : ℝ) (ht : 1 / 2 < t) (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m 0 t)) :
  (LeanRidgelet.tanhSynthesis m t ht) γ = f ↔
    γ - (LeanRidgelet.normalizedTanhRightInverse m t ht) f ∈
      (↑(LeanRidgelet.tanhSynthesis m t ht)).ker

theorem LeanRidgelet.tanhSolution_iff_kernel_translate
  (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 1 / 2 < t)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m 0
        t)) :
  (LeanRidgelet.tanhSynthesis m t ht) γ =
      f ↔
    γ -
        (LeanRidgelet.normalizedTanhRightInverse
            m t ht)
          f ∈
      (↑(LeanRidgelet.tanhSynthesis m t
            ht)).ker

Proposition6.5

uses 0used by 0✓L∃∀N

For t>3/2, ReLU synthesis is surjective and admits an adjoint ridgelet operator, a complete description of its solutions, and a unique minimum-norm solution.

Lean code for Proposition6.5●3 theorems

theoremdefined in LeanRidgelet/Operator/ReLU.lean

complete

theorem LeanRidgelet.surjective_reluSynthesis (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 3 / 2 < t) :
  Function.Surjective ⇑(LeanRidgelet.reluSynthesis m t ht)

theorem LeanRidgelet.surjective_reluSynthesis
  (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 3 / 2 < t) :
  Function.Surjective
    ⇑(LeanRidgelet.reluSynthesis m t ht)

theoremdefined in LeanRidgelet/Operator/ReLU.lean

complete

theorem LeanRidgelet.adjoint_reluSynthesis (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 3 / 2 < t) :
  ContinuousLinearMap.adjoint (LeanRidgelet.reluSynthesis m t ht) =
    LeanRidgelet.ridgeletOperator m 0 t
      (LeanRidgelet.reluRieszRepresenter m t ht)

theorem LeanRidgelet.adjoint_reluSynthesis (m : ℕ)
  [NeZero m] (t : ℝ) (ht : 3 / 2 < t) :
  ContinuousLinearMap.adjoint
      (LeanRidgelet.reluSynthesis m t
        ht) =
    LeanRidgelet.ridgeletOperator m 0 t
      (LeanRidgelet.reluRieszRepresenter m
        t ht)

theoremdefined in LeanRidgelet/Operator/ReLU.lean

complete

theorem LeanRidgelet.reluSolution_iff_kernel_translate (m : ℕ) [NeZero m]
  (t : ℝ) (ht : 3 / 2 < t) (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m 0 t)) :
  (LeanRidgelet.reluSynthesis m t ht) γ = f ↔
    γ - (LeanRidgelet.normalizedReLURightInverse m t ht) f ∈
      (↑(LeanRidgelet.reluSynthesis m t ht)).ker

theorem LeanRidgelet.reluSolution_iff_kernel_translate
  (m : ℕ) [NeZero m] (t : ℝ)
  (ht : 3 / 2 < t)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m 0
        t)) :
  (LeanRidgelet.reluSynthesis m t ht) γ =
      f ↔
    γ -
        (LeanRidgelet.normalizedReLURightInverse
            m t ht)
          f ∈
      (↑(LeanRidgelet.reluSynthesis m t
            ht)).ker

Theorem6.6

uses 0used by 0XL∃∀N

If s\le0, there is a continuous inclusion from \mathcal A_{0,t} into \mathcal A_{s,t}. This extends the present s=0 theory of tanh and ReLU toward the range treated in the source manuscript.

Theorem6.7

uses 0used by 0XL∃∀N

Identify the distributional Fourier formulas for ReLU, tanh, the Gaussian CDF, and the Gaussian, including finite-part, principal-value, and Dirac distributions.

Theorem6.8

uses 0used by 0XL∃∀N

For each standard activation, the Riesz representer satisfies the one-dimensional weak resolvent equation from the manuscript, from which an explicit adjoint ridgelet function can be derived.