Infinite-dimensional operator ridgelet transform

4.2. Weighted Sobolev activation spaces and standard activations🔗

Write \langle u\rangle=(1+u^2)^{1/2} and let B^q be the Bessel operator on the frequency variable. For s\in\mathbb R and t\ge0, the weighted Sobolev activation space is \mathcal A_{s,t}=\langle\cdot\rangle^tH^s(\mathbb R)\subset\mathcal S'(\mathbb R) with \|\beta\|_{\mathcal A_{s,t}}=\|\langle\omega\rangle^sB^{-t}\widehat\beta\|_{L^2}, and the dual test norm is \|r\|_{\mathcal H^\sharp_{s,t}}=\|\langle\omega\rangle^{-s}B^tr\|_{L^2} for r\in\mathcal S(\mathbb R).

Lemma4.2.1
Statement uses 2
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The map \beta\mapsto\langle\omega\rangle^sB^{-t}\widehat\beta is an isometric isomorphism \mathcal A_{s,t}\to L^2(\mathbb R): the coordinate is represented by an L^2 function (i), the map is injective (ii) and onto (iii). Moreover |\frac1{2\pi}\langle\widehat\beta,r\rangle|\le\frac1{2\pi}\|\beta\|_{\mathcal A_{s,t}}\|r\|_{\mathcal H^\sharp_{s,t}} (iv), so the pairing extends to the completion of the test filters in \mathcal H^\sharp_{s,t} (v).

Lean code for Lemma4.2.1●10 declarations
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.activationFourierCoordinate (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ) : TemperedDistribution ℝ ℂ
    def OperatorRidgelet.activationFourierCoordinate
  (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ) :
  TemperedDistribution ℝ ℂ
    The coordinate `⟨ω⟩^s B^{-t} β̂` of `β` under the manuscript's isometry
`𝒜_{s,t} → L²(ℝ)`, as a tempered distribution.
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.activationCoordinate (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ) :
  ↥(LeanRidgelet.L2 ℝ MeasureTheory.volume)
    def OperatorRidgelet.activationCoordinate
  (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ) :
  ↥(LeanRidgelet.L2 ℝ
      MeasureTheory.volume)
    The `L²(ℝ)` element representing `⟨ω⟩^s B^{-t} β̂`, when there is one (i.e. when
`β ∈ 𝒜_{s,t}`), and `0` otherwise.
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.activationNorm (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ) : ℝ
    def OperatorRidgelet.activationNorm (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ) : ℝ
    The norm `‖β‖_{𝒜_{s,t}} = ‖⟨ω⟩^s B^{-t} β̂‖_{L²}`.
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.testFilterCoordinate (s t : ℝ) (r : SchwartzMap ℝ ℂ) :
  SchwartzMap ℝ ℂ
    def OperatorRidgelet.testFilterCoordinate
  (s t : ℝ) (r : SchwartzMap ℝ ℂ) :
  SchwartzMap ℝ ℂ
    The test coordinate `⟨ω⟩^{-s} B^t r` of a Schwartz test filter `r`.
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.testFilterNorm (s t : ℝ) (r : SchwartzMap ℝ ℂ) : ℝ
    def OperatorRidgelet.testFilterNorm (s t : ℝ)
  (r : SchwartzMap ℝ ℂ) : ℝ
    The dual test norm `‖r‖_{ℋ^♯_{s,t}} = ‖⟨ω⟩^{-s} B^t r‖_{L²}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_weighted_duality_i (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : LeanRidgelet.MemActivationSpace s t β) :
  ∃ σ,
    (MeasureTheory.Lp.toTemperedDistributionCLM ℂ MeasureTheory.volume
          2)
        σ =
      OperatorRidgelet.activationFourierCoordinate s t β
    theorem OperatorRidgelet.Paper.lem_weighted_duality_i
  (s t : ℝ) (β : TemperedDistribution ℝ ℂ)
  (hβ :
    LeanRidgelet.MemActivationSpace s t
      β) :
  ∃ σ,
    (MeasureTheory.Lp.toTemperedDistributionCLM
          ℂ MeasureTheory.volume 2)
        σ =
      OperatorRidgelet.activationFourierCoordinate
        s t β
    **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
map `β ↦ ⟨ω⟩^s B^{-t} β̂` is well defined on `𝒜_{s,t}`: its value is represented by an element
of `L²(ℝ)`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_weighted_duality_ii (s t : ℝ)
  (β β' : TemperedDistribution ℝ ℂ)
  (hβ : LeanRidgelet.MemActivationSpace s t β)
  (hβ' : LeanRidgelet.MemActivationSpace s t β')
  (h :
    OperatorRidgelet.activationCoordinate s t β =
      OperatorRidgelet.activationCoordinate s t β') :
  β = β'
    theorem OperatorRidgelet.Paper.lem_weighted_duality_ii
  (s t : ℝ)
  (β β' : TemperedDistribution ℝ ℂ)
  (hβ :
    LeanRidgelet.MemActivationSpace s t β)
  (hβ' :
    LeanRidgelet.MemActivationSpace s t
      β')
  (h :
    OperatorRidgelet.activationCoordinate
        s t β =
      OperatorRidgelet.activationCoordinate
        s t β') :
  β = β'
    **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
map `β ↦ ⟨ω⟩^s B^{-t} β̂` is injective on `𝒜_{s,t}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_weighted_duality_iii (s t : ℝ)
  (σ : ↥(LeanRidgelet.L2 ℝ MeasureTheory.volume)) :
  LeanRidgelet.MemActivationSpace s t
      ((LeanRidgelet.activationRealization s t) σ) ∧
    OperatorRidgelet.activationCoordinate s t
        ((LeanRidgelet.activationRealization s t) σ) =
      σ
    theorem OperatorRidgelet.Paper.lem_weighted_duality_iii
  (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.L2 ℝ
        MeasureTheory.volume)) :
  LeanRidgelet.MemActivationSpace s t
      ((LeanRidgelet.activationRealization
          s t)
        σ) ∧
    OperatorRidgelet.activationCoordinate
        s t
        ((LeanRidgelet.activationRealization
            s t)
          σ) =
      σ
    **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
map `β ↦ ⟨ω⟩^s B^{-t} β̂` is onto `L²(ℝ)`: every `σ ∈ L²(ℝ)` is the coordinate of the activation
`β = 𝓕⁻¹[B^t ⟨ω⟩^{-s} σ] ∈ 𝒜_{s,t}` (the vendored `activationRealization`); the isometry is the
definition of the norm `‖β‖_{𝒜_{s,t}} = ‖σ‖_{L²}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_weighted_duality_iv (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : LeanRidgelet.MemActivationSpace s t β) (r : SchwartzMap ℝ ℂ) :
  ‖↑(2 * Real.pi)⁻¹ *
        (LeanRidgelet.Fourier.angularFourierDistribution β) r‖ ≤
    (2 * Real.pi)⁻¹ * OperatorRidgelet.activationNorm s t β *
      OperatorRidgelet.testFilterNorm s t r
    theorem OperatorRidgelet.Paper.lem_weighted_duality_iv
  (s t : ℝ) (β : TemperedDistribution ℝ ℂ)
  (hβ :
    LeanRidgelet.MemActivationSpace s t β)
  (r : SchwartzMap ℝ ℂ) :
  ‖↑(2 * Real.pi)⁻¹ *
        (LeanRidgelet.Fourier.angularFourierDistribution
            β)
          r‖ ≤
    (2 * Real.pi)⁻¹ *
        OperatorRidgelet.activationNorm s
          t β *
      OperatorRidgelet.testFilterNorm s t
        r
    **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
duality bound `|(2π)⁻¹ ⟨β̂, r⟩| ≤ (2π)⁻¹ ‖β‖_{𝒜_{s,t}} ‖r‖_{ℋ^♯_{s,t}}` for `β ∈ 𝒜_{s,t}` and
Schwartz `r`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_weighted_duality_v (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : LeanRidgelet.MemActivationSpace s t β) :
  ∃ Φ,
    ‖Φ‖ ≤ (2 * Real.pi)⁻¹ * OperatorRidgelet.activationNorm s t β ∧
      ∀ (r : SchwartzMap ℝ ℂ),
        Φ
            ((OperatorRidgelet.testFilterCoordinate s t r).toLp 2
              MeasureTheory.volume) =
          ↑(2 * Real.pi)⁻¹ *
            (LeanRidgelet.Fourier.angularFourierDistribution β) r
    theorem OperatorRidgelet.Paper.lem_weighted_duality_v
  (s t : ℝ) (β : TemperedDistribution ℝ ℂ)
  (hβ :
    LeanRidgelet.MemActivationSpace s t
      β) :
  ∃ Φ,
    ‖Φ‖ ≤
        (2 * Real.pi)⁻¹ *
          OperatorRidgelet.activationNorm
            s t β ∧
      ∀ (r : SchwartzMap ℝ ℂ),
        Φ
            ((OperatorRidgelet.testFilterCoordinate
                  s t r).toLp
              2 MeasureTheory.volume) =
          ↑(2 * Real.pi)⁻¹ *
            (LeanRidgelet.Fourier.angularFourierDistribution
                β)
              r
    **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
pairing extends to the completion of the test filters in `ℋ^♯_{s,t}`, which is `L²(ℝ)` through
the coordinate `r ↦ ⟨ω⟩^{-s} B^t r`: there is a continuous linear functional on `L²(ℝ)` of norm
at most `(2π)⁻¹ ‖β‖_{𝒜_{s,t}}` that agrees with `(2π)⁻¹ ⟨β̂, r⟩` on the test filters.
Proof for Lemma 4.2.1
uses 0

\beta=\langle\cdot\rangle^t\mathcal F^{-1}[\langle\omega\rangle^{-s}g] is a preimage of g\in L^2; the multiplier \langle u\rangle^t is real and even, so B^t is symmetric for the bilinear pairing, the identity \langle\widehat\beta,r\rangle=\int(\langle\omega\rangle^sB^{-t}\widehat\beta)(\langle\omega\rangle^{-s}B^tr)\,\mathrm d\omega extends by density, and Cauchy–Schwarz proves the bound.

Lemma4.2.2
Statement uses 3
Statement dependency previews
Preview
Theorem 3.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

ReLU, \tanh, the Gaussian distribution function \Phi(u)=\int_{-\infty}^u(2\pi)^{-1/2}e^{-v^2/2}\,\mathrm dv, and e^{-u^2/2} belong to \mathcal A_{0,2}=\langle\cdot\rangle^2L^2(\mathbb R), are globally Lipschitz, and are not polynomials (twelve claims). For every non-polynomial real \beta\in\mathcal S' there is a real band-pass \rho with C_{\beta,\rho}^{(\alpha)}=1.

Lean code for Lemma4.2.2●17 declarations
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.MemActivationSpaceFun (s t : ℝ) (β : ℝ → ℝ) : Prop
    def OperatorRidgelet.MemActivationSpaceFun
  (s t : ℝ) (β : ℝ → ℝ) : Prop
    A function `β : ℝ → ℝ` belongs to `𝒜_{s,t}`: some tempered distribution acting by
integration against `β` lies in `𝒜_{s,t}` (vendored `MemActivationSpace`).
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.gaussianCdf (u : ℝ) : ℝ
    def OperatorRidgelet.gaussianCdf (u : ℝ) : ℝ
    The Gaussian distribution function `Φ(u) = ∫_{-∞}^u (2π)^{-1/2} e^{-v²/2} dv`.
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.gaussianFun (u : ℝ) : ℝ
    def OperatorRidgelet.gaussianFun (u : ℝ) : ℝ
    The Gaussian activation `u ↦ e^{-u²/2}`.
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.weightedDistribution (t : ℝ) (β : ℝ → ℝ) :
  TemperedDistribution ℝ ℂ
    def OperatorRidgelet.weightedDistribution
  (t : ℝ) (β : ℝ → ℝ) :
  TemperedDistribution ℝ ℂ
    The tempered distribution `⟨x⟩^t (⟨x⟩^{-t} β)` of a function `β` of polynomial growth with
`⟨x⟩^{-t} β ∈ L²(ℝ)` (and `0` otherwise); it acts by integration against `β`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2 LeanRidgelet.relu
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 LeanRidgelet.relu
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_lipschitz :
  ∃ L, LipschitzWith L LeanRidgelet.relu
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_lipschitz :
  ∃ L, LipschitzWith L LeanRidgelet.relu
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun LeanRidgelet.relu
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      LeanRidgelet.relu
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2 Real.tanh
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 Real.tanh
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_lipschitz :
  ∃ L, LipschitzWith L Real.tanh
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_lipschitz :
  ∃ L, LipschitzWith L Real.tanh
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun Real.tanh
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      Real.tanh
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2
    OperatorRidgelet.gaussianCdf
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 OperatorRidgelet.gaussianCdf
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_lipschitz :
  ∃ L, LipschitzWith L OperatorRidgelet.gaussianCdf
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_lipschitz :
  ∃ L,
    LipschitzWith L
      OperatorRidgelet.gaussianCdf
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun OperatorRidgelet.gaussianCdf
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      OperatorRidgelet.gaussianCdf
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2
    OperatorRidgelet.gaussianFun
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 OperatorRidgelet.gaussianFun
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_lipschitz :
  ∃ L, LipschitzWith L OperatorRidgelet.gaussianFun
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_lipschitz :
  ∃ L,
    LipschitzWith L
      OperatorRidgelet.gaussianFun
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun OperatorRidgelet.gaussianFun
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      OperatorRidgelet.gaussianFun
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_exists_filter
  {α : ℝ} (hα : 0 < α) (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β)
  (hpoly : ¬OperatorRidgelet.IsPolynomialDistribution β) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α β ρ = 1
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_exists_filter
  {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialDistribution
        β) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α β ρ =
        1
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
For every non-polynomial real `β ∈ 𝒮'` there is a real band-pass `ρ` with
`C^{(α)}_{β,ρ} = 1`.
Proof for Lemma 4.2.2
uses 0

Membership in \mathcal A_{0,2} means \langle u\rangle^{-2}\beta\in L^2; three of the functions are bounded and ReLU satisfies \int_0^\infty u^2(1+u^2)^{-2}\mathrm du<\infty. Their derivatives are bounded wherever defined, the bounded functions are nonconstant and ReLU is not smooth at zero, and the last statement is the final part of the proof of Theorem 3.1.5 followed by rescaling \rho.

Proposition4.2.3
Statement uses 4
Statement dependency previews
Preview
Theorem 3.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

ReLU, \tanh, the Gaussian distribution function, and the Gaussian e^{-u^2/2} are globally Lipschitz, are not polynomials, and belong to \mathcal A_{0,2}. Each of them is therefore covered by Theorem 4.1.3, by Theorem 3.1.5 (iii), and by the finite-width bounds of Theorem 5.2.1; the Lean instance of this coverage is that for every \alpha>0 there is a band-pass \rho with C_{\beta,\rho}^{(\alpha)}\ne0 for each of the four activations.

Lean code for Proposition4.2.3●16 theorems
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2 LeanRidgelet.relu
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 LeanRidgelet.relu
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_lipschitz :
  ∃ L, LipschitzWith L LeanRidgelet.relu
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_lipschitz :
  ∃ L, LipschitzWith L LeanRidgelet.relu
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun LeanRidgelet.relu
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_relu_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      LeanRidgelet.relu
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2 Real.tanh
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 Real.tanh
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_lipschitz :
  ∃ L, LipschitzWith L Real.tanh
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_lipschitz :
  ∃ L, LipschitzWith L Real.tanh
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun Real.tanh
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_tanh_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      Real.tanh
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2
    OperatorRidgelet.gaussianCdf
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 OperatorRidgelet.gaussianCdf
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_lipschitz :
  ∃ L, LipschitzWith L OperatorRidgelet.gaussianCdf
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_lipschitz :
  ∃ L,
    LipschitzWith L
      OperatorRidgelet.gaussianCdf
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun OperatorRidgelet.gaussianCdf
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      OperatorRidgelet.gaussianCdf
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2
    OperatorRidgelet.gaussianFun
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 OperatorRidgelet.gaussianFun
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` belongs to `𝒜_{0,2}`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_lipschitz :
  ∃ L, LipschitzWith L OperatorRidgelet.gaussianFun
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_lipschitz :
  ∃ L,
    LipschitzWith L
      OperatorRidgelet.gaussianFun
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` is globally Lipschitz.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun OperatorRidgelet.gaussianFun
    theorem OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      OperatorRidgelet.gaussianFun
    **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` is not a polynomial.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.ex_standard_activations_relu {α : ℝ}
  (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.reluDistribution ρ ≠
        0
    theorem OperatorRidgelet.Paper.ex_standard_activations_relu
  {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.reluDistribution
          ρ ≠
        0
    **Example [ex:standard-activations]** Standard activations.  ReLU is covered by Theorem
`thm:tempered-reconstruction`, Theorem A(iii), and the finite-width bounds: for every `α > 0`
there is a band-pass `ρ` with `C^{(α)}_{ReLU,ρ} ≠ 0`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.ex_standard_activations_tanh {α : ℝ}
  (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.tanhDistribution ρ ≠
        0
    theorem OperatorRidgelet.Paper.ex_standard_activations_tanh
  {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.tanhDistribution
          ρ ≠
        0
    **Example [ex:standard-activations]** Standard activations.  `tanh` is covered by Theorem
`thm:tempered-reconstruction`, Theorem A(iii), and the finite-width bounds: for every `α > 0`
there is a band-pass `ρ` with `C^{(α)}_{tanh,ρ} ≠ 0`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.ex_standard_activations_gaussianCdf {α : ℝ}
  (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.gaussianCdfDistribution ρ ≠
        0
    theorem OperatorRidgelet.Paper.ex_standard_activations_gaussianCdf
  {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.gaussianCdfDistribution
          ρ ≠
        0
    **Example [ex:standard-activations]** Standard activations.  The Gaussian distribution
function `Φ` is covered by Theorem `thm:tempered-reconstruction`, Theorem A(iii), and the
finite-width bounds: for every `α > 0` there is a band-pass `ρ` with `C^{(α)}_{Φ,ρ} ≠ 0`.
  • theoremdefined in OperatorRidgelet/Paper/Tempered.lean
    complete
    theorem OperatorRidgelet.Paper.ex_standard_activations_gaussian {α : ℝ}
  (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.gaussianDistribution ρ ≠
        0
    theorem OperatorRidgelet.Paper.ex_standard_activations_gaussian
  {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.gaussianDistribution
          ρ ≠
        0
    **Example [ex:standard-activations]** Standard activations.  The Gaussian `e^{-u²/2}` is
covered by Theorem `thm:tempered-reconstruction`, Theorem A(iii), and the finite-width bounds:
for every `α > 0` there is a band-pass `ρ` with `C^{(α)}_{e^{-u²/2},ρ} ≠ 0`.
Proof for Proposition 4.2.3
uses 0

The three properties are Lemma 4.2.2; a globally Lipschitz function has polynomial growth, so Theorem 3.1.5 (iii) and Theorem 5.2.1 apply.