5.1. Weighted Sobolev activation spaces🔗

DefinitionAux.8

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 5.1

Loading preview

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

✓L∃∀N

This is the common distributional setup of Section 5. Polynomiality enters Lemma 5.2 and Theorem 5.4, the realizations of standard activations enter Lemma 5.2, and the choice of a Schwartz representative enters Definition 5.3.

A tempered distribution \beta\in\mathcal S'(\mathbb R) is a polynomial, equivalently \beta=0 in \mathcal S'/\mathcal P, when it acts by integration against some polynomial. The Schwartz function with prescribed values is obtained by choice when one exists. The standard activations \tanh, the Gaussian distribution function \Phi, and the Gaussian e^{-u^2/2} are realized as tempered distributions acting by integration against the function; ReLU is treated in Corollary 5.5.

Lean code for DefinitionAux.8●5 definitions

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.IsPolynomialDistribution
  (β : TemperedDistribution ℝ ℂ) : Prop

def OperatorRidgelet.IsPolynomialDistribution
  (β : TemperedDistribution ℝ ℂ) : Prop

`β ∈ 𝒮'(ℝ)` is a polynomial (`β = 0` in `𝒮'/𝒫`): it acts by integration against the
evaluation of some `p : ℂ[X]`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.schwartzOfFun (f : ℝ → ℂ) : SchwartzMap ℝ ℂ

def OperatorRidgelet.schwartzOfFun
  (f : ℝ → ℂ) : SchwartzMap ℝ ℂ

The Schwartz function with the values `f`, when one exists; `0` otherwise.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.tanhDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.tanhDistribution :
  TemperedDistribution ℝ ℂ

`tanh ∈ 𝒮'(ℝ)`, the vendored realization `tanhTemperedDistribution` (weight exponent
`t = 2`), which acts by integration against `tanh`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.gaussianCdfDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.gaussianCdfDistribution :
  TemperedDistribution ℝ ℂ

`Φ ∈ 𝒮'(ℝ)`, the weighted realization of the Gaussian distribution function.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.gaussianDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.gaussianDistribution :
  TemperedDistribution ℝ ℂ

`e^{-u²/2} ∈ 𝒮'(ℝ)`, the weighted realization of the Gaussian activation.

Write \langle u\rangle=(1+u^2)^{1/2} and B^qv=F_{\mathbb R}[\langle\cdot\rangle^qF_{\mathbb R}^{-1}v]. For s\in\mathbb R, t\ge0, define \mathcal A_{s,t}=\langle\cdot\rangle^tH^s(\mathbb R) with norm \|\beta\|_{\mathcal A_{s,t}}=\|\langle\omega\rangle^sB^{-t}\beta^\sharp\|_2, and the test norm \|r\|_{\mathcal T^\sharp_{s,t}}=\|\langle\omega\rangle^{-s}B^tr\|_2. Membership controls distributional pairings; a continuous pointwise representative remains a separate assumption.

Lemma5.1

Statement uses 2

Statement dependency previews

Preview

Definition Aux.4

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}\beta^\sharp 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\beta^\sharp,r\rangle|\le\frac1{2\pi}\|\beta\|_{\mathcal A_{s,t}}\|r\|_{\mathcal T^\sharp_{s,t}} (iv), so the pairing extends to the completion of the test filters in \mathcal T^\sharp_{s,t} (v).

Lean code for Lemma5.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_5_1_i (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : LeanRidgelet.MemActivationSpace s t β) :
  ∃ σ,
    (MeasureTheory.Lp.toTemperedDistributionCLM ℂ MeasureTheory.volume
          2)
        σ =
      OperatorRidgelet.activationFourierCoordinate s t β

theorem OperatorRidgelet.Paper.lem_5_1_i (s t : ℝ)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    LeanRidgelet.MemActivationSpace s t
      β) :
  ∃ σ,
    (MeasureTheory.Lp.toTemperedDistributionCLM
          ℂ MeasureTheory.volume 2)
        σ =
      OperatorRidgelet.activationFourierCoordinate
        s t β

**Lemma [lem:5.1]** 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_5_1_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_5_1_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:5.1]** 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_5_1_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_5_1_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:5.1]** 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_5_1_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_5_1_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:5.1]** 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_5_1_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_5_1_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:5.1]** 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 5.1

uses 0

\beta=\langle\cdot\rangle^tF_{\mathbb R}^{-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\beta^\sharp,r\rangle=\int(\langle\omega\rangle^sB^{-t}\beta^\sharp)(\langle\omega\rangle^{-s}B^tr)\,\mathrm d\omega extends by density, and Cauchy–Schwarz proves the bound.

Lemma5.2

uses 1used 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 Lemma5.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_5_2_relu_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2 LeanRidgelet.relu

theorem OperatorRidgelet.Paper.lem_5_2_relu_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 LeanRidgelet.relu

**Lemma [lem:5.2]** Standard activations and admissible test filters.
ReLU belongs to `𝒜_{0,2}`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_relu_lipschitz :
  ∃ L, LipschitzWith L LeanRidgelet.relu

theorem OperatorRidgelet.Paper.lem_5_2_relu_lipschitz :
  ∃ L, LipschitzWith L LeanRidgelet.relu

**Lemma [lem:5.2]** Standard activations and admissible test filters.
ReLU is globally Lipschitz.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_relu_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun LeanRidgelet.relu

theorem OperatorRidgelet.Paper.lem_5_2_relu_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      LeanRidgelet.relu

**Lemma [lem:5.2]** Standard activations and admissible test filters.
ReLU is not a polynomial.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_tanh_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2 Real.tanh

theorem OperatorRidgelet.Paper.lem_5_2_tanh_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 Real.tanh

**Lemma [lem:5.2]** Standard activations and admissible test filters.
`tanh` belongs to `𝒜_{0,2}`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_tanh_lipschitz :
  ∃ L, LipschitzWith L Real.tanh

theorem OperatorRidgelet.Paper.lem_5_2_tanh_lipschitz :
  ∃ L, LipschitzWith L Real.tanh

**Lemma [lem:5.2]** Standard activations and admissible test filters.
`tanh` is globally Lipschitz.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_tanh_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun Real.tanh

theorem OperatorRidgelet.Paper.lem_5_2_tanh_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      Real.tanh

**Lemma [lem:5.2]** Standard activations and admissible test filters.
`tanh` is not a polynomial.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_gaussianCdf_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2
    OperatorRidgelet.gaussianCdf

theorem OperatorRidgelet.Paper.lem_5_2_gaussianCdf_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 OperatorRidgelet.gaussianCdf

**Lemma [lem:5.2]** 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_5_2_gaussianCdf_lipschitz :
  ∃ L, LipschitzWith L OperatorRidgelet.gaussianCdf

theorem OperatorRidgelet.Paper.lem_5_2_gaussianCdf_lipschitz :
  ∃ L,
    LipschitzWith L
      OperatorRidgelet.gaussianCdf

**Lemma [lem:5.2]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is globally Lipschitz.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.lem_5_2_gaussianCdf_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun OperatorRidgelet.gaussianCdf

theorem OperatorRidgelet.Paper.lem_5_2_gaussianCdf_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      OperatorRidgelet.gaussianCdf

**Lemma [lem:5.2]** 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_5_2_gaussian_mem :
  OperatorRidgelet.MemActivationSpaceFun 0 2
    OperatorRidgelet.gaussianFun

theorem OperatorRidgelet.Paper.lem_5_2_gaussian_mem :
  OperatorRidgelet.MemActivationSpaceFun 0
    2 OperatorRidgelet.gaussianFun

**Lemma [lem:5.2]** 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_5_2_gaussian_lipschitz :
  ∃ L, LipschitzWith L OperatorRidgelet.gaussianFun

theorem OperatorRidgelet.Paper.lem_5_2_gaussian_lipschitz :
  ∃ L,
    LipschitzWith L
      OperatorRidgelet.gaussianFun

**Lemma [lem:5.2]** 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_5_2_gaussian_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun OperatorRidgelet.gaussianFun

theorem OperatorRidgelet.Paper.lem_5_2_gaussian_not_polynomial :
  ¬OperatorRidgelet.IsPolynomialFun
      OperatorRidgelet.gaussianFun

**Lemma [lem:5.2]** 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_5_2_exists_filter {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β)
  (hpoly : ¬OperatorRidgelet.IsPolynomialDistribution β) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α β ρ = 1

theorem OperatorRidgelet.Paper.lem_5_2_exists_filter
  {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialDistribution
        β) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α β ρ =
        1

**Lemma [lem:5.2]** Standard activations and admissible test filters.
For every non-polynomial real `β ∈ 𝒮'` there is a real band-pass `ρ` with
`C^{(α)}_{β,ρ} = 1`.

Proof for Lemma 5.2

Proof uses 2

Proof dependency previews

Preview

Theorem 4.5

Loading preview

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

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 4.5 followed by rescaling \rho.