Infinite-dimensional operator ridgelet transform

3.6. Examples of analysis filters🔗

A band-pass filter works for every positive homogeneity exponent. The Mexican hat distinguishes admissibility from the extra support assumption in band-pass reconstruction.

Example3.15
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 0✓L∃∀N

Let \eta(u)=\exp(-1/(1-u^2)) for |u|<1 and 0 otherwise, and choose the real Schwartz filter with \rho_{\mathrm{bp}}^\sharp(\omega)=-\eta(2|\omega|-3). The choice-based Lean representative is 0 if the Schwartz condition fails; the statements below verify that condition and the prescribed Fourier transform.

\rho_{\mathrm{bp}}^\sharp 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 5.5.

Lean code for Example3.15●14 declarations
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_i :
  ContDiff ℝ (↑⊤) OperatorRidgelet.Filters.bandPassHat
    theorem OperatorRidgelet.Paper.ex_3_15_i :
  ContDiff ℝ (↑⊤)
    OperatorRidgelet.Filters.bandPassHat
    **Example [ex:3.15]** 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_3_15_ii (ω : ℝ) :
  OperatorRidgelet.Filters.bandPassHat ω ≤ 0
    theorem OperatorRidgelet.Paper.ex_3_15_ii
  (ω : ℝ) :
  OperatorRidgelet.Filters.bandPassHat ω ≤
    0
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  `ρ♯_bp` is
nonpositive.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_iii :
  OperatorRidgelet.Filters.bandPassHat ≠ 0
    theorem OperatorRidgelet.Paper.ex_3_15_iii :
  OperatorRidgelet.Filters.bandPassHat ≠ 0
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  `ρ♯_bp` is
nonzero.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_iv :
  tsupport OperatorRidgelet.Filters.bandPassHat ⊆
    {ω | 1 ≤ |ω| ∧ |ω| ≤ 2}
    theorem OperatorRidgelet.Paper.ex_3_15_iv :
  tsupport
      OperatorRidgelet.Filters.bandPassHat ⊆
    {ω | 1 ≤ |ω| ∧ |ω| ≤ 2}
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  `ρ♯_bp` is
supported in `{1 ≤ |ω| ≤ 2}`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_v :
  ⇑OperatorRidgelet.Filters.bandPass =
    OperatorRidgelet.Filters.bandPassFun
    theorem OperatorRidgelet.Paper.ex_3_15_v :
  ⇑OperatorRidgelet.Filters.bandPass =
    OperatorRidgelet.Filters.bandPassFun
    **Example [ex:3.15]** 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_3_15_vi (t : ℝ) :
  OperatorRidgelet.Filters.bandPass (-t) =
    OperatorRidgelet.Filters.bandPass t
    theorem OperatorRidgelet.Paper.ex_3_15_vi
  (t : ℝ) :
  OperatorRidgelet.Filters.bandPass (-t) =
    OperatorRidgelet.Filters.bandPass t
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  `ρ_bp` is even.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_vii (ω : ℝ) :
  OperatorRidgelet.filterFourier (⇑OperatorRidgelet.Filters.bandPass)
      ω =
    ↑(OperatorRidgelet.Filters.bandPassHat ω)
    theorem OperatorRidgelet.Paper.ex_3_15_vii
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑OperatorRidgelet.Filters.bandPass)
      ω =
    ↑(OperatorRidgelet.Filters.bandPassHat
        ω)
    **Example [ex:3.15]** 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_3_15_viii :
  OperatorRidgelet.IsBandPass OperatorRidgelet.Filters.bandPass
    theorem OperatorRidgelet.Paper.ex_3_15_viii :
  OperatorRidgelet.IsBandPass
    OperatorRidgelet.Filters.bandPass
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  `ρ_bp` satisfies
the band-pass condition.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_ix (α : ℝ) :
  0 < α →
    OperatorRidgelet.IsAdmissible α OperatorRidgelet.Filters.bandPass
    theorem OperatorRidgelet.Paper.ex_3_15_ix
  (α : ℝ) :
  0 < α →
    OperatorRidgelet.IsAdmissible α
      OperatorRidgelet.Filters.bandPass
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  `ρ_bp` is
`α`-admissible for every `α > 0`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_15_x (α : ℝ) :
  0 < α →
    OperatorRidgelet.admissibilityConst α
        ((√(OperatorRidgelet.admissibilityConst α
                ⇑OperatorRidgelet.Filters.bandPass))⁻¹ •
          ⇑OperatorRidgelet.Filters.bandPass) =
      1
    theorem OperatorRidgelet.Paper.ex_3_15_x (α : ℝ) :
  0 < α →
    OperatorRidgelet.admissibilityConst α
        ((√(OperatorRidgelet.admissibilityConst
                α
                ⇑OperatorRidgelet.Filters.bandPass))⁻¹ •
          ⇑OperatorRidgelet.Filters.bandPass) =
      1
    **Example [ex:3.15]** A band-pass filter for every `α > 0`.  Multiplying by
`(C^{(α)}_{ρ_bp})^{-1/2}` normalizes the admissibility constant to one.
  • 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).
Proof for Example 3.15
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.

Example3.16
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 0✓L∃∀N

The Mexican hat is \rho_{\mathrm{MH}}(t)=(1-t^2)e^{-t^2/2}. Its Schwartz representative is obtained by choice, with junk value 0 outside the Schwartz condition verified below.

\rho_{\mathrm{MH}}(t)=(1-t^2)e^{-t^2/2} is a Schwartz function (i) with \rho_{\mathrm{MH}}^\sharp(\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). When 0<\alpha<5, Theorem 3.14, Theorem 4.8 and part (ii) of Theorem 4.5 apply. The band-pass statements in part (iii) of Theorem 4.5 and in Theorem 5.4 do not apply to this filter.

Lean code for Example3.16●8 declarations
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_16_i :
  ⇑OperatorRidgelet.Filters.mexicanHat =
    OperatorRidgelet.Filters.mexicanHatFun
    theorem OperatorRidgelet.Paper.ex_3_16_i :
  ⇑OperatorRidgelet.Filters.mexicanHat =
    OperatorRidgelet.Filters.mexicanHatFun
    **Example [ex:3.16]** Mexican hat.  `ρ_MH(t) = (1 - t²) e^{-t²/2}` is a Schwartz
function.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_16_ii (ω : ℝ) :
  OperatorRidgelet.filterFourier (⇑OperatorRidgelet.Filters.mexicanHat)
      ω =
    ↑(√(2 * Real.pi) * ω ^ 2 * Real.exp (-ω ^ 2 / 2))
    theorem OperatorRidgelet.Paper.ex_3_16_ii
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑OperatorRidgelet.Filters.mexicanHat)
      ω =
    ↑(√(2 * Real.pi) * ω ^ 2 *
        Real.exp (-ω ^ 2 / 2))
    **Example [ex:3.16]** Mexican hat.  `ρ♯_MH(ω) = √(2π) ω² e^{-ω²/2}`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_16_iii (α : ℝ) :
  0 < α →
    (OperatorRidgelet.IsAdmissible α
        OperatorRidgelet.Filters.mexicanHat ↔
      α < 5)
    theorem OperatorRidgelet.Paper.ex_3_16_iii
  (α : ℝ) :
  0 < α →
    (OperatorRidgelet.IsAdmissible α
        OperatorRidgelet.Filters.mexicanHat ↔
      α < 5)
    **Example [ex:3.16]** Mexican hat.  Under the standing assumption `α > 0`, `ρ_MH` is
`α`-admissible exactly for `α < 5`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_16_iv (α : ℝ) :
  0 < α →
    α < 5 →
      OperatorRidgelet.admissibilityConst α
          ⇑OperatorRidgelet.Filters.mexicanHat =
        Real.Gamma ((5 - α) / 2)
    theorem OperatorRidgelet.Paper.ex_3_16_iv
  (α : ℝ) :
  0 < α →
    α < 5 →
      OperatorRidgelet.admissibilityConst
          α
          ⇑OperatorRidgelet.Filters.mexicanHat =
        Real.Gamma ((5 - α) / 2)
    **Example [ex:3.16]** Mexican hat.  For `0 < α < 5`,
`C^{(α)}_{ρ_MH} = Γ((5-α)/2)`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_16_v :
  OperatorRidgelet.admissibilityConst 1
      ⇑OperatorRidgelet.Filters.mexicanHat =
    1
    theorem OperatorRidgelet.Paper.ex_3_16_v :
  OperatorRidgelet.admissibilityConst 1
      ⇑OperatorRidgelet.Filters.mexicanHat =
    1
    **Example [ex:3.16]** Mexican hat.  In particular `C^{(1)}_{ρ_MH} = 1`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_16_vi :
  ¬OperatorRidgelet.IsBandPass OperatorRidgelet.Filters.mexicanHat
    theorem OperatorRidgelet.Paper.ex_3_16_vi :
  ¬OperatorRidgelet.IsBandPass
      OperatorRidgelet.Filters.mexicanHat
    **Example [ex:3.16]** Mexican hat.  `ρ_MH` is not band pass.
  • 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).
Proof for Example 3.16
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.