5.2. Reconstruction with tempered activations🔗

Definition5.3

Statement uses 5

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

Let \beta\in\mathcal S'(\mathbb R) be real, that is, fixed by distributional conjugation, and let \rho be a band-pass filter. Choose an even \chi\in C_c^\infty(\mathbb R\setminus\{0\}) equal to one on a neighbourhood of \operatorname{supp}\rho^\sharp (i) and an even, compactly supported, smooth approximate identity (\eta_\varepsilon)_{\varepsilon>0} (ii), and define the real Schwartz functions \beta_\varepsilon by \beta_\varepsilon^\sharp=\chi\,(\beta^\sharp*\eta_\varepsilon)\in C_c^\infty(\mathbb R\setminus\{0\}) (iii–v: membership, existence, and uniqueness of \beta_\varepsilon). For \gamma\in\operatorname{Ran}R_\rho, the regularized synthesis is S_{\beta_\varepsilon}\gamma=R_{\beta_\varepsilon}'\gamma\in\mathcal E_\alpha' (vi), and the synthesis with \beta is S_\beta\gamma=\lim_{\varepsilon\downarrow0}S_{\beta_\varepsilon}\gamma in the norm of \mathcal E_\alpha', whenever the limit exists.

Lean code for Definition5.3●14 declarations

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

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

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

`β ∈ 𝒮'(ℝ)` is real: it is fixed by the distributional conjugation
`conj u [φ] = conj (u [conj φ])`; equivalently, `β` pairs real test functions to real numbers.

structure(5 fields)defined in OperatorRidgelet/Tempered/Defs.lean

complete

structure OperatorRidgelet.IsCutoff (ρ : SchwartzMap ℝ ℝ) (χ : ℝ → ℝ) : Prop

structure OperatorRidgelet.IsCutoff
  (ρ : SchwartzMap ℝ ℝ) (χ : ℝ → ℝ) : Prop

An even `χ ∈ C_c^∞(ℝ ∖ {0})` equal to one on a neighbourhood of `supp ρ♯`.

Fields

contDiff : ContDiff ℝ (↑⊤) χ

`χ` is smooth.

hasCompactSupport : HasCompactSupport χ

`χ` has compact support.

zero_notMem_tsupport : 0 ∉ tsupport χ

The support of `χ` stays away from the origin.

even : ∀ (ω : ℝ), χ (-ω) = χ ω

`χ` is even.

eventuallyEq_one : ∀ᶠ (ω : ℝ) in nhdsSet (tsupport (OperatorRidgelet.filterFourier ⇑ρ)), χ ω = 1

`χ = 1` on a neighbourhood of `supp ρ♯`.

structure(6 fields)defined in OperatorRidgelet/Tempered/Defs.lean

complete

structure OperatorRidgelet.IsApproximateIdentity (η : ℝ → ℝ → ℝ) : Prop

structure OperatorRidgelet.IsApproximateIdentity
  (η : ℝ → ℝ → ℝ) : Prop

An even, compactly supported, smooth approximate identity `(η_ε)_{ε>0}`: for every `ε > 0`
the function `η_ε` is smooth, compactly supported, even, nonnegative, with integral one, and the
supports shrink to `{0}` as `ε ↓ 0`.  (The values of `η` at `ε ≤ 0` are irrelevant.)

Fields

contDiff : ∀ (ε : ℝ), 0 < ε → ContDiff ℝ (↑⊤) (η ε)

Each `η_ε` is smooth.

hasCompactSupport : ∀ (ε : ℝ), 0 < ε → HasCompactSupport (η ε)

Each `η_ε` has compact support.

even : ∀ (ε : ℝ), 0 < ε → ∀ (x : ℝ), η ε (-x) = η ε x

Each `η_ε` is even.

nonneg : ∀ (ε : ℝ), 0 < ε → ∀ (x : ℝ), 0 ≤ η ε x

Each `η_ε` is nonnegative.

integral_eq_one : ∀ (ε : ℝ), 0 < ε → ∫ (x : ℝ), η ε x = 1

Each `η_ε` has integral one.

tendsto_tsupport : Filter.Tendsto (fun ε => tsupport (η ε)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0).smallSets

The supports of `η_ε` shrink to `{0}` as `ε ↓ 0`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.distributionConvolution (u : TemperedDistribution ℝ ℂ)
  (η : ℝ → ℝ) (ω : ℝ) : ℂ

def OperatorRidgelet.distributionConvolution
  (u : TemperedDistribution ℝ ℂ)
  (η : ℝ → ℝ) (ω : ℝ) : ℂ

The convolution `(u * η)(ω) = ⟨u, η(ω - ·)⟩` of a tempered distribution `u` with a test
function `η` (smooth and compactly supported in the applications).

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.regularizedSpectrum (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε ω : ℝ) : ℂ

def OperatorRidgelet.regularizedSpectrum
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε ω : ℝ) :
  ℂ

The regularized spectrum `β♯_ε = χ (β♯ * η_ε)` of a tempered activation `β`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.regularizedActivation (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ) : SchwartzMap ℝ ℝ

def OperatorRidgelet.regularizedActivation
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ) :
  SchwartzMap ℝ ℝ

The regularized activation `β_ε`: the real Schwartz function with `β♯_ε = χ (β♯ * η_ε)`
(unique by Fourier injectivity), and `0` if there is none.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.regularizedSynthesis.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.regularizedSynthesis.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

The regularized synthesis `S_{β_ε} γ := R'_{β_ε} γ ∈ 𝓔_α'`, the synthesis operator
`synthesis` of Section 4 with the regularized activation `β_ε` as filter.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.temperedSynthesis.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.temperedSynthesis.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

The synthesis with the tempered activation `β`, `S_β γ := lim_{ε ↓ 0} S_{β_ε} γ` in
`𝓔_α'`, whenever the limit exists (and `0` otherwise).

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_5_3_i (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) :
  ∃ χ, OperatorRidgelet.IsCutoff ρ χ

theorem OperatorRidgelet.Paper.def_5_3_i
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) :
  ∃ χ, OperatorRidgelet.IsCutoff ρ χ

**Definition [def:5.3]** Regularized synthesis.  For a band-pass `ρ` there
is an even `χ ∈ C_c^∞(ℝ ∖ {0})` equal to one on a neighbourhood of `supp ρ♯`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_5_3_ii :
  ∃ η, OperatorRidgelet.IsApproximateIdentity η

theorem OperatorRidgelet.Paper.def_5_3_ii :
  ∃ η,
    OperatorRidgelet.IsApproximateIdentity
      η

**Definition [def:5.3]** Regularized synthesis.  There is an even,
compactly supported, smooth approximate identity `(η_ε)_{ε>0}`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_5_3_iii (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε) :
  ContDiff ℝ (↑⊤) (OperatorRidgelet.regularizedSpectrum β χ η ε) ∧
    HasCompactSupport (OperatorRidgelet.regularizedSpectrum β χ η ε) ∧
      0 ∉ tsupport (OperatorRidgelet.regularizedSpectrum β χ η ε)

theorem OperatorRidgelet.Paper.def_5_3_iii
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε) :
  ContDiff ℝ (↑⊤)
      (OperatorRidgelet.regularizedSpectrum
        β χ η ε) ∧
    HasCompactSupport
        (OperatorRidgelet.regularizedSpectrum
          β χ η ε) ∧
      0 ∉
        tsupport
          (OperatorRidgelet.regularizedSpectrum
            β χ η ε)

**Definition [def:5.3]** Regularized synthesis.  For real `β`, band-pass
`ρ`, a cutoff `χ`, and an approximate identity `(η_ε)`, the regularized spectrum
`β♯_ε = χ (β♯ * η_ε)` belongs to `C_c^∞(ℝ ∖ {0})` for every `ε > 0`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_5_3_iv (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε)
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.regularizedActivation β χ η ε)) ω =
    OperatorRidgelet.regularizedSpectrum β χ η ε ω

theorem OperatorRidgelet.Paper.def_5_3_iv
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε) (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.regularizedActivation
          β χ η ε))
      ω =
    OperatorRidgelet.regularizedSpectrum β
      χ η ε ω

**Definition [def:5.3]** Regularized synthesis.  There is a real Schwartz
function `β_ε` with `β♯_ε = χ (β♯ * η_ε)`: the chosen `regularizedActivation` has this Fourier
transform.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_5_3_v (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε)
  (b : SchwartzMap ℝ ℝ) :
  (∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑b) ω =
        OperatorRidgelet.regularizedSpectrum β χ η ε ω) →
    b = OperatorRidgelet.regularizedActivation β χ η ε

theorem OperatorRidgelet.Paper.def_5_3_v
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε)
  (b : SchwartzMap ℝ ℝ) :
  (∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑b)
          ω =
        OperatorRidgelet.regularizedSpectrum
          β χ η ε ω) →
    b =
      OperatorRidgelet.regularizedActivation
        β χ η ε

**Definition [def:5.3]** Regularized synthesis.  The real Schwartz function
`β_ε` with `β♯_ε = χ (β♯ * η_ε)` is unique.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_5_3_vi.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hγ : γ ∈ OperatorRidgelet.ridgeletRange μ ν ⇑ρ)
  (g : ↥(OperatorRidgelet.spectralRange μ ν)) :
  (OperatorRidgelet.regularizedSynthesis μ ν β χ η ε γ) g =
    inner ℂ
      ((OperatorRidgelet.ridgeletExtension μ ν
          ⇑(OperatorRidgelet.regularizedActivation β χ η ε))
        g)
      γ

theorem OperatorRidgelet.Paper.def_5_3_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (hγ :
    γ ∈
      OperatorRidgelet.ridgeletRange μ ν
        ⇑ρ)
  (g :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  (OperatorRidgelet.regularizedSynthesis μ
        ν β χ η ε γ)
      g =
    inner ℂ
      ((OperatorRidgelet.ridgeletExtension
          μ ν
          ⇑(OperatorRidgelet.regularizedActivation
              β χ η ε))
        g)
      γ

**Definition [def:5.3]** Regularized synthesis.  For `γ ∈ Ran R_ρ` the
regularized synthesis `S_{β_ε} γ = R'_{β_ε} γ` is a well-defined element of `𝓔_α'`: it is the
continuous anti-linear functional `g ↦ ⟨γ, R_{β_ε} g⟩_{L²(λ)}` (in the representation of
`OperatorRidgelet.Reconstruction.Defs`, where `S_ρ` is the transpose of the bounded extension
`R_ρ`, this holds by definition).

Theorem5.4

Statement uses 2

Statement dependency previews

Preview

Definition Aux.5

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Corollary 5.5

Loading preview

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

✓L∃∀N

Let \beta\in\mathcal S'(\mathbb R) be real and let \rho be a band-pass filter. For every f\in\mathcal E_\alpha the limit defining S_\beta R_\rho f exists (i), does not depend on \chi or (\eta_\varepsilon) (ii), and S_\beta R_\rho f=C_{\beta,\rho}^{(\alpha)}T_\alpha f (iii). If C_{\beta,\rho}^{(\alpha)}\ne0, then f=(C_{\beta,\rho}^{(\alpha)})^{-1}T_\alpha^{-1}S_\beta R_\rho f for f\in\mathcal E_\alpha (iv) and g=(C_{\beta,\rho}^{(\alpha)})^{-1}S_\beta(R_\rho T_\alpha^{-1}g) for g\in\mathcal E_\alpha' (v). If \beta is not a polynomial, then a band-pass \rho with C_{\beta,\rho}^{(\alpha)}\ne0 exists (vi).

Lean code for Theorem5.4●6 theorems

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_5_4_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  ∃ F,
    Filter.Tendsto
      (fun ε =>
        OperatorRidgelet.regularizedSynthesis μ ν β χ η ε
          ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f))
      (nhdsWithin 0 (Set.Ioi 0)) (nhds F)

theorem OperatorRidgelet.Paper.thm_5_4_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  ∃ F,
    Filter.Tendsto
      (fun ε =>
        OperatorRidgelet.regularizedSynthesis
          μ ν β χ η ε
          ((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f))
      (nhdsWithin 0 (Set.Ioi 0)) (nhds F)

**Theorem [thm:5.4]** Reconstruction with a tempered activation.  For
every `f ∈ 𝓔_α` the limit `S_β R_ρ f = lim_{ε ↓ 0} S_{β_ε} R_ρ f` exists in `𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_5_4_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ χ' : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (hχ' : OperatorRidgelet.IsCutoff ρ χ') (η η' : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (hη' : OperatorRidgelet.IsApproximateIdentity η')
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β χ η
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =
    OperatorRidgelet.temperedSynthesis μ ν β χ' η'
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f)

theorem OperatorRidgelet.Paper.thm_5_4_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ χ' : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (hχ' : OperatorRidgelet.IsCutoff ρ χ')
  (η η' : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (hη' :
    OperatorRidgelet.IsApproximateIdentity
      η')
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β
      χ η
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f) =
    OperatorRidgelet.temperedSynthesis μ ν
      β χ' η'
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f)

**Theorem [thm:5.4]** Reconstruction with a tempered activation.  The
limit `S_β R_ρ f` does not depend on the cutoff `χ` or on the approximate identity `(η_ε)`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_5_4_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β χ η
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =
    OperatorRidgelet.temperedAdmissibilityConst α β ρ •
      (OperatorRidgelet.rieszMap μ ν) f

theorem OperatorRidgelet.Paper.thm_5_4_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β
      χ η
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f) =
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ •
      (OperatorRidgelet.rieszMap μ ν) f

**Theorem [thm:5.4]** Reconstruction with a tempered activation.  The
frame identity `S_β R_ρ f = C^{(α)}_{β,ρ} T_α f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_5_4_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  f =
    (OperatorRidgelet.temperedAdmissibilityConst α β ρ)⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.temperedSynthesis μ ν β χ η
          ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f))

theorem OperatorRidgelet.Paper.thm_5_4_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ ≠
      0)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  f =
    (OperatorRidgelet.temperedAdmissibilityConst
          α β ρ)⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.temperedSynthesis
          μ ν β χ η
          ((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f))

**Theorem [thm:5.4]** Reconstruction with a tempered activation.  If
`C^{(α)}_{β,ρ} ≠ 0`, then `f = (C^{(α)}_{β,ρ})⁻¹ T_α⁻¹ S_β R_ρ f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_5_4_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0)
  (g : OperatorRidgelet.SpectralAntiDual μ ν) :
  g =
    (OperatorRidgelet.temperedAdmissibilityConst α β ρ)⁻¹ •
      OperatorRidgelet.temperedSynthesis μ ν β χ η
        ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
          (OperatorRidgelet.rieszInv μ ν g))

theorem OperatorRidgelet.Paper.thm_5_4_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ ≠
      0)
  (g :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  g =
    (OperatorRidgelet.temperedAdmissibilityConst
          α β ρ)⁻¹ •
      OperatorRidgelet.temperedSynthesis μ
        ν β χ η
        ((OperatorRidgelet.ridgeletExtension
            μ ν ⇑ρ)
          (OperatorRidgelet.rieszInv μ ν
            g))

**Theorem [thm:5.4]** Reconstruction with a tempered activation.  If
`C^{(α)}_{β,ρ} ≠ 0`, then `g = (C^{(α)}_{β,ρ})⁻¹ S_β (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

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

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

**Theorem [thm:5.4]** Reconstruction with a tempered activation.  If
`β` is not a polynomial (equivalently `β ≠ 0` in `𝒮'/𝒫`), then a band-pass `ρ` with
`C^{(α)}_{β,ρ} ≠ 0` exists.

Proof for Theorem 5.4

Proof uses 3

Proof dependency previews

Preview

Theorem 3.14

Loading preview

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

Each \beta_\varepsilon is a real Schwartz function whose Fourier transform has compact support away from zero. It is admissible whenever it is nonzero. Plancherel gives the following identity in that case; the zero case is immediate: S_{\beta_\varepsilon}R_\rho f=C_{\beta_\varepsilon,\rho}^{(\alpha)}T_\alpha f; distributional convergence of \beta^\sharp*\eta_\varepsilon against the fixed test function \rho^\sharp(-\omega)|\omega|^{-\alpha} gives convergence of the constants, and T_\alpha is an isometry, so the functionals converge in \mathcal E_\alpha'. The existence of \rho with nonzero constant is the last step of the proof of Theorem 4.5.

Corollary5.5

Statement uses 5

Statement dependency previews

Preview

Definition 3.3

Loading preview

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

used by 0✓L∃∀N

Let \beta=\operatorname{ReLU}, \operatorname{ReLU}(t)=\max(t,0). Then \operatorname{ReLU}^\sharp=-\operatorname{fp}(\omega^{-2})+i\pi\delta_0' (i), which equals -\omega^{-2} away from the origin (ii). If \rho^\sharp\in C_c^\infty(\mathbb R\setminus\{0\}) is nonzero, even, and nonpositive, then C_{\operatorname{ReLU},\rho}^{(\alpha)}=-\frac1{2\pi}\int_{\mathbb R}\rho^\sharp(\omega)|\omega|^{-\alpha-2}\,\mathrm d\omega (iii), which is positive (iv). After rescaling \rho the constant is one (v), and the two reconstruction formulas of Theorem 5.4 (vi, vii) and Theorem 4.5 (iii) (viii) hold with ReLU synthesis for every \alpha>0.

Lean code for Corollary5.5●11 declarations

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.reluDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.reluDistribution :
  TemperedDistribution ℝ ℂ

`ReLU ∈ 𝒮'(ℝ)`, the vendored realization `reluTemperedDistribution` (weight exponent
`t = 2`), which acts by integration against `ReLU(t) = max(t, 0)`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.reluAdmissibilityScale (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  ℝ

def OperatorRidgelet.reluAdmissibilityScale
  (α : ℝ) (ρ : SchwartzMap ℝ ℝ) : ℝ

The ReLU admissibility constant `-(2π)⁻¹ ∫ ρ♯(ω) |ω|^{-α-2} dω` of a filter with real `ρ♯`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.reluNormalizedFilter (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  SchwartzMap ℝ ℝ

def OperatorRidgelet.reluNormalizedFilter
  (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  SchwartzMap ℝ ℝ

The filter `ρ` rescaled so that `C^{(α)}_{ReLU,ρ} = 1`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_i (φ : SchwartzMap ℝ ℂ) :
  Filter.Tendsto
    (fun ε => (∫ (ω : ℝ) in {ω | ε < |ω|}, φ ω / ↑ω ^ 2) - 2 * φ 0 / ↑ε)
    (nhdsWithin 0 (Set.Ioi 0))
    (nhds
      (-(LeanRidgelet.Fourier.angularFourierDistribution
              OperatorRidgelet.reluDistribution)
            φ -
        ↑Real.pi * Complex.I * deriv (⇑φ) 0))

theorem OperatorRidgelet.Paper.cor_5_5_i
  (φ : SchwartzMap ℝ ℂ) :
  Filter.Tendsto
    (fun ε =>
      (∫ (ω : ℝ) in {ω | ε < |ω|},
          φ ω / ↑ω ^ 2) -
        2 * φ 0 / ↑ε)
    (nhdsWithin 0 (Set.Ioi 0))
    (nhds
      (-(LeanRidgelet.Fourier.angularFourierDistribution
              OperatorRidgelet.reluDistribution)
            φ -
        ↑Real.pi * Complex.I *
          deriv (⇑φ) 0))

**Corollary [cor:5.5]** ReLU is admissible.  Under the manuscript's convention
`ReLU^ = -fp(ω^{-2}) + iπ δ₀'`: tested against a Schwartz function `φ`, the Hadamard finite part
`⟨fp(ω^{-2}), φ⟩ = lim_{ε ↓ 0} (∫_{|ω|>ε} φ(ω) ω^{-2} dω - 2 φ(0)/ε)` equals
`-⟨ReLU^, φ⟩ - iπ φ'(0)`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_ii (φ : SchwartzMap ℝ ℂ) :
  0 ∉ tsupport ⇑φ →
    (LeanRidgelet.Fourier.angularFourierDistribution
          OperatorRidgelet.reluDistribution)
        φ =
      ∫ (ω : ℝ), -(↑ω ^ 2)⁻¹ * φ ω

theorem OperatorRidgelet.Paper.cor_5_5_ii
  (φ : SchwartzMap ℝ ℂ) :
  0 ∉ tsupport ⇑φ →
    (LeanRidgelet.Fourier.angularFourierDistribution
          OperatorRidgelet.reluDistribution)
        φ =
      ∫ (ω : ℝ), -(↑ω ^ 2)⁻¹ * φ ω

**Corollary [cor:5.5]** ReLU is admissible.  Away from the origin `ReLU^` equals
`-ω^{-2}`: `⟨ReLU^, φ⟩ = ∫ (-ω^{-2}) φ(ω) dω` for every Schwartz `φ` supported away from `0`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_iii {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0) :
  OperatorRidgelet.temperedAdmissibilityConst α
      OperatorRidgelet.reluDistribution ρ =
    ↑(OperatorRidgelet.reluAdmissibilityScale α ρ)

theorem OperatorRidgelet.Paper.cor_5_5_iii {α : ℝ}
  (hα : 0 < α) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0) :
  OperatorRidgelet.temperedAdmissibilityConst
      α OperatorRidgelet.reluDistribution
      ρ =
    ↑(OperatorRidgelet.reluAdmissibilityScale
        α ρ)

**Corollary [cor:5.5]** ReLU is admissible.  If `ρ♯ ∈ C_c^∞(ℝ ∖ {0})` is
nonzero, even, and nonpositive, then `C^{(α)}_{ReLU,ρ} = -(2π)⁻¹ ∫ ρ♯(ω) |ω|^{-α-2} dω`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_iv {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0) :
  0 < OperatorRidgelet.reluAdmissibilityScale α ρ

theorem OperatorRidgelet.Paper.cor_5_5_iv {α : ℝ}
  (hα : 0 < α) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0) :
  0 <
    OperatorRidgelet.reluAdmissibilityScale
      α ρ

**Corollary [cor:5.5]** ReLU is admissible.  Under the same hypotheses the
constant `-(2π)⁻¹ ∫ ρ♯(ω) |ω|^{-α-2} dω` is positive.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_v {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0) :
  OperatorRidgelet.IsBandPass
      (OperatorRidgelet.reluNormalizedFilter α ρ) ∧
    OperatorRidgelet.temperedAdmissibilityConst α
        OperatorRidgelet.reluDistribution
        (OperatorRidgelet.reluNormalizedFilter α ρ) =
      1

theorem OperatorRidgelet.Paper.cor_5_5_v {α : ℝ}
  (hα : 0 < α) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0) :
  OperatorRidgelet.IsBandPass
      (OperatorRidgelet.reluNormalizedFilter
        α ρ) ∧
    OperatorRidgelet.temperedAdmissibilityConst
        α
        OperatorRidgelet.reluDistribution
        (OperatorRidgelet.reluNormalizedFilter
          α ρ) =
      1

**Corollary [cor:5.5]** ReLU is admissible.  After rescaling, `ρ` is still
band-pass and `C^{(α)}_{ReLU,ρ} = 1`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_vi.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter α ρ) χ)
  (η : ℝ → ℝ → ℝ) (hη : OperatorRidgelet.IsApproximateIdentity η)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  f =
    OperatorRidgelet.rieszInv μ ν
      (OperatorRidgelet.temperedSynthesis μ ν
        OperatorRidgelet.reluDistribution χ η
        ((OperatorRidgelet.ridgeletExtension μ ν
            ⇑(OperatorRidgelet.reluNormalizedFilter α ρ))
          f))

theorem OperatorRidgelet.Paper.cor_5_5_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter
        α ρ)
      χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  f =
    OperatorRidgelet.rieszInv μ ν
      (OperatorRidgelet.temperedSynthesis
        μ ν
        OperatorRidgelet.reluDistribution
        χ η
        ((OperatorRidgelet.ridgeletExtension
            μ ν
            ⇑(OperatorRidgelet.reluNormalizedFilter
                α ρ))
          f))

**Corollary [cor:5.5]** ReLU is admissible.  With the rescaled filter the first
reconstruction formula holds with ReLU synthesis for every `α > 0`:
`f = T_α⁻¹ S_{ReLU} R_ρ f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_vii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter α ρ) χ)
  (η : ℝ → ℝ → ℝ) (hη : OperatorRidgelet.IsApproximateIdentity η)
  (g : OperatorRidgelet.SpectralAntiDual μ ν) :
  g =
    OperatorRidgelet.temperedSynthesis μ ν
      OperatorRidgelet.reluDistribution χ η
      ((OperatorRidgelet.ridgeletExtension μ ν
          ⇑(OperatorRidgelet.reluNormalizedFilter α ρ))
        (OperatorRidgelet.rieszInv μ ν g))

theorem OperatorRidgelet.Paper.cor_5_5_vii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter
        α ρ)
      χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (g :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  g =
    OperatorRidgelet.temperedSynthesis μ ν
      OperatorRidgelet.reluDistribution χ
      η
      ((OperatorRidgelet.ridgeletExtension
          μ ν
          ⇑(OperatorRidgelet.reluNormalizedFilter
              α ρ))
        (OperatorRidgelet.rieszInv μ ν g))

**Corollary [cor:5.5]** ReLU is admissible.  With the rescaled filter the second
reconstruction formula holds with ReLU synthesis for every `α > 0`:
`g = S_{ReLU} (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_5_5_viii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0)
  (I : Set ℝ) (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (G : H → ℂ) (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          OperatorRidgelet.coefficientFormula
              (⇑(OperatorRidgelet.reluNormalizedFilter α ρ)) G (a, c) *
            ↑(LeanRidgelet.relu (inner ℝ a x + c)))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
        (fun a =>
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter α ρ)) G
                (a, c) *
              ↑(LeanRidgelet.relu (inner ℝ a x + c)))
        ν ∧
      ∫ (a : H),
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter α ρ)) G
                (a, c) *
              ↑(LeanRidgelet.relu (inner ℝ a x + c)) ∂ν =
        OperatorRidgelet.spectralTarget ν G x

theorem OperatorRidgelet.Paper.cor_5_5_viii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          OperatorRidgelet.coefficientFormula
              (⇑(OperatorRidgelet.reluNormalizedFilter
                  α ρ))
              G (a, c) *
            ↑(LeanRidgelet.relu
                (inner ℝ a x + c)))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
        (fun a =>
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter
                    α ρ))
                G (a, c) *
              ↑(LeanRidgelet.relu
                  (inner ℝ a x + c)))
        ν ∧
      ∫ (a : H),
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter
                    α ρ))
                G (a, c) *
              ↑(LeanRidgelet.relu
                  (inner ℝ a x + c)) ∂ν =
        OperatorRidgelet.spectralTarget ν
          G x

**Corollary [cor:5.5]** ReLU is admissible.  With the rescaled filter Theorem
A(iii) holds with ReLU synthesis for every `α > 0`: for `G` regular along rays and every `x`,
the inner integral `∫ γ_G(a,c) ReLU(⟪a,x⟫ + c) dc` converges absolutely for `ν`-almost every
`a`, its `ν`-integral converges absolutely, and it equals `g_G(x)`.

Proof for Corollary 5.5

uses 0

From \operatorname{ReLU}(t)=(|t|+t)/2, the identities (|t|)^\sharp=-2\operatorname{fp}(\omega^{-2}) and t^\sharp=2\pi i\delta_0' give the Fourier transform; the test function is supported away from zero, so the \delta_0' term vanishes and the finite part is ordinary multiplication by \omega^{-2}, and evenness and the sign of \rho^\sharp give the constant.

Example5.6

Statement uses 3

Statement dependency previews

Preview

Theorem 4.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 5.4, by Theorem 4.5 (iii), and by the finite-width bounds of Theorem 6.6; 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 Example5.6●16 theorems

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.ex_5_6_relu {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.reluDistribution ρ ≠
        0

theorem OperatorRidgelet.Paper.ex_5_6_relu {α : ℝ}
  (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.reluDistribution
          ρ ≠
        0

**Example [ex:5.6]** Standard activations.  ReLU is covered by Theorem
`thm:5.4`, Theorem 4.5(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_5_6_tanh {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.tanhDistribution ρ ≠
        0

theorem OperatorRidgelet.Paper.ex_5_6_tanh {α : ℝ}
  (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.tanhDistribution
          ρ ≠
        0

**Example [ex:5.6]** Standard activations.  `tanh` is covered by Theorem
`thm:5.4`, Theorem 4.5(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_5_6_gaussianCdf {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.gaussianCdfDistribution ρ ≠
        0

theorem OperatorRidgelet.Paper.ex_5_6_gaussianCdf
  {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.gaussianCdfDistribution
          ρ ≠
        0

**Example [ex:5.6]** Standard activations.  The Gaussian distribution
function `Φ` is covered by Theorem `thm:5.4`, Theorem 4.5(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_5_6_gaussian {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α
          OperatorRidgelet.gaussianDistribution ρ ≠
        0

theorem OperatorRidgelet.Paper.ex_5_6_gaussian
  {α : ℝ} (hα : 0 < α) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α
          OperatorRidgelet.gaussianDistribution
          ρ ≠
        0

**Example [ex:5.6]** Standard activations.  The Gaussian `e^{-u²/2}` is
covered by Theorem `thm:5.4`, Theorem 4.5(iii), and the finite-width bounds:
for every `α > 0` there is a band-pass `ρ` with `C^{(α)}_{e^{-u²/2},ρ} ≠ 0`.

Proof for Example 5.6

uses 1

The three properties are Lemma 5.2; a globally Lipschitz function has polynomial growth, so Theorem 4.5 (iii) applies. The activation assumptions of the finite-width results below are therefore satisfied.

Remark 5.7 (Identity in the dual space versus integral network).

The frame identity for a tempered activation holds in \mathcal E_\alpha'. By itself it does not produce a finite coefficient measure on H\times\mathbb R. For a spectral density regular along rays, Theorem 4.5 gives an absolutely convergent integral network; Theorem 6.6 supplies finite total variation and moments. The ReLU examples use this stronger conclusion.