2.6. Explicit admissible filters🔗

Definition2.6.1

uses 1

Used by 2

Reverse dependency previews

Preview

Proposition 2.6.2

Loading preview

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

✓L∃∀N

With the bump \eta(u)=\exp(-1/(1-u^2)) for |u|<1 and 0 otherwise, the band-pass filter \rho_{\mathrm{bp}} is the real even Schwartz function with \widehat\rho_{\mathrm{bp}}(\omega)=-\eta(2|\omega|-3), obtained by Fourier inversion; the Mexican hat is \rho_{\mathrm{MH}}(t)=(1-t^2)e^{-t^2/2}. Both are taken as Schwartz maps by choice, with junk value 0 should the explicit function fail to be Schwartz.

Lean code for Definition2.6.1●6 definitions

defdefined in OperatorRidgelet/Filters/Defs.lean

complete

def OperatorRidgelet.Filters.bump (u : ℝ) : ℝ

def OperatorRidgelet.Filters.bump (u : ℝ) : ℝ

The bump `η(u) = exp(-1/(1-u²))` for `|u| < 1` and `η(u) = 0` otherwise.

defdefined in OperatorRidgelet/Filters/Defs.lean

complete

def OperatorRidgelet.Filters.bandPassHat (ω : ℝ) : ℝ

def OperatorRidgelet.Filters.bandPassHat
  (ω : ℝ) : ℝ

The Fourier transform `ρ̂_bp(ω) = -η(2|ω| - 3)` of the band-pass filter, supported in
`{1 ≤ |ω| ≤ 2}`.

defdefined in OperatorRidgelet/Filters/Defs.lean

complete

def OperatorRidgelet.Filters.bandPassFun (t : ℝ) : ℝ

def OperatorRidgelet.Filters.bandPassFun
  (t : ℝ) : ℝ

The band-pass filter as a function: the Fourier inversion
`ρ_bp(t) = (2π)⁻¹ ∫ ρ̂_bp(ω) exp(itω) dω`, which is real because `ρ̂_bp` is real and even.

defdefined in OperatorRidgelet/Filters/Defs.lean

complete

def OperatorRidgelet.Filters.bandPass : SchwartzMap ℝ ℝ

def OperatorRidgelet.Filters.bandPass :
  SchwartzMap ℝ ℝ

The band-pass filter `ρ_bp ∈ 𝒮(ℝ)` (junk value `0` if `bandPassFun` were not Schwartz).

defdefined in OperatorRidgelet/Filters/Defs.lean

complete

def OperatorRidgelet.Filters.mexicanHatFun (t : ℝ) : ℝ

def OperatorRidgelet.Filters.mexicanHatFun
  (t : ℝ) : ℝ

The Mexican hat `ρ_MH(t) = (1 - t²) exp(-t²/2)` as a function.

defdefined in OperatorRidgelet/Filters/Defs.lean

complete

def OperatorRidgelet.Filters.mexicanHat : SchwartzMap ℝ ℝ

def OperatorRidgelet.Filters.mexicanHat :
  SchwartzMap ℝ ℝ

The Mexican hat `ρ_MH ∈ 𝒮(ℝ)` (junk value `0` if `mexicanHatFun` were not Schwartz).

Proposition2.6.2

Statement uses 3

Statement dependency previews

Preview

Definition 2.2.1

Loading preview

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

used by 0✓L∃∀N

\widehat\rho_{\mathrm{bp}} is smooth (i), nonpositive (ii), nonzero (iii), and supported in \{1\le|\omega|\le2\} (iv), so \rho_{\mathrm{bp}}\in\mathcal S(\mathbb R) is real (v) and even (vi) with the prescribed Fourier transform (vii), satisfies the band-pass condition (viii), and is \alpha-admissible for every \alpha>0 (ix); multiplying by ((\!(\rho_{\mathrm{bp}},\rho_{\mathrm{bp}})\!)_\alpha)^{-1/2} normalizes the admissibility constant to one (x). The sign makes it admissible for ReLU synthesis in the sense of Corollary 4.1.4.

Lean code for Proposition2.6.2●10 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_i :
  ContDiff ℝ (↑⊤) OperatorRidgelet.Filters.bandPassHat

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_i :
  ContDiff ℝ (↑⊤)
    OperatorRidgelet.Filters.bandPassHat

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  The prescribed
Fourier transform `ρ̂_bp` is smooth.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_ii (ω : ℝ) :
  OperatorRidgelet.Filters.bandPassHat ω ≤ 0

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_ii
  (ω : ℝ) :
  OperatorRidgelet.Filters.bandPassHat ω ≤
    0

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ̂_bp` is
nonpositive.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_iii :
  OperatorRidgelet.Filters.bandPassHat ≠ 0

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_iii :
  OperatorRidgelet.Filters.bandPassHat ≠ 0

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ̂_bp` is
nonzero.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_iv :
  tsupport OperatorRidgelet.Filters.bandPassHat ⊆
    {ω | 1 ≤ |ω| ∧ |ω| ≤ 2}

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_iv :
  tsupport
      OperatorRidgelet.Filters.bandPassHat ⊆
    {ω | 1 ≤ |ω| ∧ |ω| ≤ 2}

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ̂_bp` is
supported in `{1 ≤ |ω| ≤ 2}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_v :
  ⇑OperatorRidgelet.Filters.bandPass =
    OperatorRidgelet.Filters.bandPassFun

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_v :
  ⇑OperatorRidgelet.Filters.bandPass =
    OperatorRidgelet.Filters.bandPassFun

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  The inverse
Fourier transform `ρ_bp` of `ρ̂_bp` is a real Schwartz function.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_vi (t : ℝ) :
  OperatorRidgelet.Filters.bandPass (-t) =
    OperatorRidgelet.Filters.bandPass t

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_vi
  (t : ℝ) :
  OperatorRidgelet.Filters.bandPass (-t) =
    OperatorRidgelet.Filters.bandPass t

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ_bp` is even.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_vii (ω : ℝ) :
  OperatorRidgelet.filterFourier (⇑OperatorRidgelet.Filters.bandPass)
      ω =
    ↑(OperatorRidgelet.Filters.bandPassHat ω)

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_vii
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑OperatorRidgelet.Filters.bandPass)
      ω =
    ↑(OperatorRidgelet.Filters.bandPassHat
        ω)

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  The Fourier
transform of `ρ_bp` is the prescribed `ρ̂_bp`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_viii :
  OperatorRidgelet.IsBandPass OperatorRidgelet.Filters.bandPass

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_viii :
  OperatorRidgelet.IsBandPass
    OperatorRidgelet.Filters.bandPass

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ_bp` satisfies
the band-pass condition.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_ix (α : ℝ) :
  0 < α →
    OperatorRidgelet.IsAdmissible α OperatorRidgelet.Filters.bandPass

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_ix
  (α : ℝ) :
  0 < α →
    OperatorRidgelet.IsAdmissible α
      OperatorRidgelet.Filters.bandPass

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ_bp` is
`α`-admissible for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_x (α : ℝ) :
  0 < α →
    OperatorRidgelet.admissibilityConst α
        ((√(OperatorRidgelet.admissibilityConst α
                ⇑OperatorRidgelet.Filters.bandPass))⁻¹ •
          ⇑OperatorRidgelet.Filters.bandPass) =
      1

theorem OperatorRidgelet.Paper.ex_bandlimited_filter_x
  (α : ℝ) :
  0 < α →
    OperatorRidgelet.admissibilityConst α
        ((√(OperatorRidgelet.admissibilityConst
                α
                ⇑OperatorRidgelet.Filters.bandPass))⁻¹ •
          ⇑OperatorRidgelet.Filters.bandPass) =
      1

**Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  Multiplying by
`(C^{(α)}_{ρ_bp})^{-1/2}` normalizes the admissibility constant to one.

Proof for Proposition 2.6.2

uses 0

The bump and all its derivatives vanish at |u|=1, the support stays away from \omega=0, Fourier inversion maps C_c^\infty into \mathcal S, even real Fourier data give an even real inverse, and on the compact support |\omega|^{-\alpha} is bounded above and below.

Proposition2.6.3

Statement uses 3

Statement dependency previews

Preview

Definition 2.2.1

Loading preview

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

used by 0✓L∃∀N

\rho_{\mathrm{MH}}(t)=(1-t^2)e^{-t^2/2} is a Schwartz function (i) with \widehat\rho_{\mathrm{MH}}(\omega)=\sqrt{2\pi}\,\omega^2e^{-\omega^2/2} (ii). It is \alpha-admissible exactly for 0<\alpha<5 (iii), with (\!(\rho_{\mathrm{MH}},\rho_{\mathrm{MH}})\!)_\alpha=\Gamma((5-\alpha)/2) (iv) and (\!(\rho_{\mathrm{MH}},\rho_{\mathrm{MH}})\!)_1=1 (v). It is not band pass (vi), so Theorem 2.4.2 applies to it but Theorem 3.1.5 and Theorem 4.1.3 do not.

Lean code for Proposition2.6.3●6 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_mexican_hat_i :
  ⇑OperatorRidgelet.Filters.mexicanHat =
    OperatorRidgelet.Filters.mexicanHatFun

theorem OperatorRidgelet.Paper.ex_mexican_hat_i :
  ⇑OperatorRidgelet.Filters.mexicanHat =
    OperatorRidgelet.Filters.mexicanHatFun

**Example [ex:mexican-hat]** Mexican hat.  `ρ_MH(t) = (1 - t²) e^{-t²/2}` is a Schwartz
function.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_mexican_hat_ii (ω : ℝ) :
  OperatorRidgelet.filterFourier (⇑OperatorRidgelet.Filters.mexicanHat)
      ω =
    ↑(√(2 * Real.pi) * ω ^ 2 * Real.exp (-ω ^ 2 / 2))

theorem OperatorRidgelet.Paper.ex_mexican_hat_ii
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑OperatorRidgelet.Filters.mexicanHat)
      ω =
    ↑(√(2 * Real.pi) * ω ^ 2 *
        Real.exp (-ω ^ 2 / 2))

**Example [ex:mexican-hat]** Mexican hat.  `ρ̂_MH(ω) = √(2π) ω² e^{-ω²/2}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_mexican_hat_iii (α : ℝ) :
  0 < α →
    (OperatorRidgelet.IsAdmissible α
        OperatorRidgelet.Filters.mexicanHat ↔
      α < 5)

theorem OperatorRidgelet.Paper.ex_mexican_hat_iii
  (α : ℝ) :
  0 < α →
    (OperatorRidgelet.IsAdmissible α
        OperatorRidgelet.Filters.mexicanHat ↔
      α < 5)

**Example [ex:mexican-hat]** Mexican hat.  Under the standing assumption `α > 0`, `ρ_MH` is
`α`-admissible exactly for `α < 5`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_mexican_hat_iv (α : ℝ) :
  0 < α →
    α < 5 →
      OperatorRidgelet.admissibilityConst α
          ⇑OperatorRidgelet.Filters.mexicanHat =
        Real.Gamma ((5 - α) / 2)

theorem OperatorRidgelet.Paper.ex_mexican_hat_iv
  (α : ℝ) :
  0 < α →
    α < 5 →
      OperatorRidgelet.admissibilityConst
          α
          ⇑OperatorRidgelet.Filters.mexicanHat =
        Real.Gamma ((5 - α) / 2)

**Example [ex:mexican-hat]** Mexican hat.  For `0 < α < 5`,
`C^{(α)}_{ρ_MH} = Γ((5-α)/2)`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_mexican_hat_v :
  OperatorRidgelet.admissibilityConst 1
      ⇑OperatorRidgelet.Filters.mexicanHat =
    1

theorem OperatorRidgelet.Paper.ex_mexican_hat_v :
  OperatorRidgelet.admissibilityConst 1
      ⇑OperatorRidgelet.Filters.mexicanHat =
    1

**Example [ex:mexican-hat]** Mexican hat.  In particular `C^{(1)}_{ρ_MH} = 1`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_mexican_hat_vi :
  ¬OperatorRidgelet.IsBandPass OperatorRidgelet.Filters.mexicanHat

theorem OperatorRidgelet.Paper.ex_mexican_hat_vi :
  ¬OperatorRidgelet.IsBandPass
      OperatorRidgelet.Filters.mexicanHat

**Example [ex:mexican-hat]** Mexican hat.  `ρ_MH` is not band pass.

Proof for Proposition 2.6.3

uses 0

With g(t)=e^{-t^2/2}, \rho_{\mathrm{MH}}=-g'' and the differentiation rule gives the Fourier transform; then (\!(\rho_{\mathrm{MH}},\rho_{\mathrm{MH}})\!)_\alpha=\int_{\mathbb R}|\omega|^{4-\alpha}e^{-\omega^2}\mathrm d\omega=\Gamma((5-\alpha)/2), convergent at zero exactly when \alpha<5.