5.5. Example of filters for the reconstruction formula🔗

Proposition5.12

Statement uses 3

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

Under the input-space and sigma-finite Borel measure hypotheses of Theorem 5.10, let \nu be homogeneous of degree \alpha>0 and finite on the unit ball. Fix s>1/2 and an integer k\ge1 with 2k>\alpha+2s-1/2, and let \rho_k^\sharp(\omega)=\omega^{2k}e^{-\omega^2}, g(\xi)=e^{-\|\xi\|^2}v. Then \rho_k is a real Schwartz filter (i) that is not band pass (ii) but is \alpha-admissible for \alpha<4k+1 (iii). The homogeneous moments \int(1+\|a\|^2)^{-d/2}\mathrm d\nu are finite for d>\alpha (iv); the coefficient \gamma_g is jointly measurable (v), each function h_a(\omega)=\rho_k^\sharp(-\omega)g(\omega a) lies in H^s_\omega (vi), and \mathfrak B_s(\rho_k,g)<\infty (vii). The Sobolev test q_{\alpha,\rho_k} lies in H^s_\omega (viii). Hence Theorem 5.10 applies to this filter for every continuous activation of growth order p<s-1/2 (ix).

Put \delta=2k-\alpha. For \sigma(t)=e^{-t^2/2}, the reconstruction constant is (\!(\sigma,\rho_k)\!)_\alpha=\Gamma((\delta+1)/2)(3/2)^{-(\delta+1)/2}/\sqrt{2\pi}>0. If s>3/2, ReLU also satisfies the hypotheses and (\!(\operatorname{ReLU},\rho_k)\!)_\alpha=-(2\pi)^{-1}\Gamma((\delta-1)/2)\ne0. The unit-ball finiteness hypothesis holds for the homogeneous Gaussian mixtures on the infinite-dimensional Hilbert space used in the main construction.

Lean code for Proposition5.12●13 declarations

defdefined in OperatorRidgelet/Sobolev/GaussianDefs.lean

complete

def OperatorRidgelet.gaussDerivFilter (k : ℕ) : SchwartzMap ℝ ℝ

def OperatorRidgelet.gaussDerivFilter
  (k : ℕ) : SchwartzMap ℝ ℝ

The Gaussian-derivative filter `ρ_k ∈ 𝒮(ℝ;ℝ)` of order `k` of `prop:5.12`.

defdefined in OperatorRidgelet/Sobolev/GaussianDefs.lean

complete

def OperatorRidgelet.gaussTarget.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (v : Y) (ξ : H) : Y

def OperatorRidgelet.gaussTarget.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (v : Y) (ξ : H) : Y

The Gaussian target `g(ξ) = e^{-‖ξ‖²} v` of `prop:5.12`.

defdefined in OperatorRidgelet/Sobolev/GaussianDefs.lean

complete

def OperatorRidgelet.gaussRayCoefficient.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (k : ℕ) (v : Y) (q : H × ℝ) : Y

def OperatorRidgelet.gaussRayCoefficient.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (k : ℕ) (v : Y)
  (q : H × ℝ) : Y

The coefficient of the Gaussian-derivative ray: the dilate `A^{-2k-1} ρ_k(b/A) v` of the
filter.

defdefined in OperatorRidgelet/Sobolev/GaussianDefs.lean

complete

def OperatorRidgelet.gaussSobolevRay (k : ℕ) (α b : ℝ) : ℂ

def OperatorRidgelet.gaussSobolevRay (k : ℕ)
  (α b : ℝ) : ℂ

The coefficient of `q_{α,ρ_k}`: the subordination superposition of the dilated filters.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_i (k : ℕ) (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.gaussDerivFilter k)) ω =
    ↑(ω ^ (2 * k) * Real.exp (-ω ^ 2))

theorem OperatorRidgelet.Paper.prop_5_12_i (k : ℕ)
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.gaussDerivFilter
          k))
      ω =
    ↑(ω ^ (2 * k) * Real.exp (-ω ^ 2))

**Proposition [prop:5.12]**(i) The Gaussian-derivative filter of order `k`
is a real Schwartz function with Fourier transform `ρ♯_k(ω) = ω^{2k} e^{-ω²}`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_ii (k : ℕ) :
  ¬OperatorRidgelet.IsBandPass (OperatorRidgelet.gaussDerivFilter k)

theorem OperatorRidgelet.Paper.prop_5_12_ii
  (k : ℕ) :
  ¬OperatorRidgelet.IsBandPass
      (OperatorRidgelet.gaussDerivFilter
        k)

**Proposition [prop:5.12]**(ii) The filter is not band pass: its Fourier
transform vanishes only at the origin.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_iii {k : ℕ} {α : ℝ} (hα : 0 < α)
  (hk : α < 4 * ↑k + 1) :
  OperatorRidgelet.IsAdmissible α (OperatorRidgelet.gaussDerivFilter k)

theorem OperatorRidgelet.Paper.prop_5_12_iii
  {k : ℕ} {α : ℝ} (hα : 0 < α)
  (hk : α < 4 * ↑k + 1) :
  OperatorRidgelet.IsAdmissible α
    (OperatorRidgelet.gaussDerivFilter k)

**Proposition [prop:5.12]**(iii) The filter is nevertheless `α`-admissible,
`0 < C^{(α)}_{ρ_k} < ∞`, in the range `α < 4k + 1`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_iv.{u_2} {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {α e : ℝ} (hα : 0 < α) {ν : MeasureTheory.Measure H}
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (hB : ν (Metric.closedBall 0 1) ≠ ⊤) (he : 2 * e + α < 0) :
  ∫⁻ (a : H), ENNReal.ofReal ((1 + ‖a‖ ^ 2) ^ e) ∂ν < ⊤

theorem OperatorRidgelet.Paper.prop_5_12_iv.{u_2}
  {H : Type u_2} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {α e : ℝ} (hα : 0 < α)
  {ν : MeasureTheory.Measure H}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (hB : ν (Metric.closedBall 0 1) ≠ ⊤)
  (he : 2 * e + α < 0) :
  ∫⁻ (a : H),
      ENNReal.ofReal
        ((1 + ‖a‖ ^ 2) ^ e) ∂ν <
    ⊤

**Proposition [prop:5.12]**(iv) The polynomial moments
`eq:homogeneous-polynomial-integrability` of a homogeneous measure that is finite on the unit
ball: `∫ (1 + ‖a‖²)^e dν < ∞` whenever `2e + α < 0`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_v.{u_1, u_2} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (k : ℕ) (v : Y) :
  MeasureTheory.StronglyMeasurable
    (OperatorRidgelet.gaussRayCoefficient k v)

theorem OperatorRidgelet.Paper.prop_5_12_v.{u_1,
    u_2}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (k : ℕ) (v : Y) :
  MeasureTheory.StronglyMeasurable
    (OperatorRidgelet.gaussRayCoefficient
      k v)

**Proposition [prop:5.12]**(v) The coefficient associated with the filter for
the Gaussian target `g(ξ) = e^{-‖ξ‖²} v` is jointly strongly measurable.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_vi.{u_1, u_2} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] [CompleteSpace Y] (k : ℕ) (v : Y) {s : ℝ} (hs : 0 ≤ s)
  (a : H) :
  (OperatorRidgelet.MemRaySobolev s fun b =>
      OperatorRidgelet.gaussRayCoefficient k v (a, b)) ∧
    ∀ (ω : ℝ),
      OperatorRidgelet.rayProfile
          (fun b => OperatorRidgelet.gaussRayCoefficient k v (a, b)) ω =
        OperatorRidgelet.filterFourier
            (⇑(OperatorRidgelet.gaussDerivFilter k)) (-ω) •
          OperatorRidgelet.gaussTarget v (ω • a)

theorem OperatorRidgelet.Paper.prop_5_12_vi.{u_1,
    u_2}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  [CompleteSpace Y] (k : ℕ) (v : Y)
  {s : ℝ} (hs : 0 ≤ s) (a : H) :
  (OperatorRidgelet.MemRaySobolev s
      fun b =>
      OperatorRidgelet.gaussRayCoefficient
        k v (a, b)) ∧
    ∀ (ω : ℝ),
      OperatorRidgelet.rayProfile
          (fun b =>
            OperatorRidgelet.gaussRayCoefficient
              k v (a, b))
          ω =
        OperatorRidgelet.filterFourier
            (⇑(OperatorRidgelet.gaussDerivFilter
                k))
            (-ω) •
          OperatorRidgelet.gaussTarget v
            (ω • a)

**Proposition [prop:5.12]**(vi) Every profile belongs to `H^s_ω(ℝ;Y)` and
equals the
profile `h_a(ω) = ρ♯_k(-ω) g(ωa)` required by `thm:5.10`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_vii.{u_1, u_2} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {k : ℕ} {α s : ℝ} (hα : 0 < α) (hs : 0 ≤ s)
  (hk : α + 2 * s - 1 / 2 < 2 * ↑k) {ν : MeasureTheory.Measure H}
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (hB : ν (Metric.closedBall 0 1) ≠ ⊤) (v : Y) :
  ∫⁻ (a : H),
      ENNReal.ofReal
        ((1 + ‖a‖) ^ s *
          OperatorRidgelet.raySobolevNorm s fun b =>
            OperatorRidgelet.gaussRayCoefficient k v (a, b)) ∂ν ≠
    ⊤

theorem OperatorRidgelet.Paper.prop_5_12_vii.{u_1,
    u_2}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {k : ℕ} {α s : ℝ} (hα : 0 < α)
  (hs : 0 ≤ s)
  (hk : α + 2 * s - 1 / 2 < 2 * ↑k)
  {ν : MeasureTheory.Measure H}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (hB : ν (Metric.closedBall 0 1) ≠ ⊤)
  (v : Y) :
  ∫⁻ (a : H),
      ENNReal.ofReal
        ((1 + ‖a‖) ^ s *
          OperatorRidgelet.raySobolevNorm
            s fun b =>
            OperatorRidgelet.gaussRayCoefficient
              k v (a, b)) ∂ν ≠
    ⊤

**Proposition [prop:5.12]**(vii) The Sobolev mass `𝔅_s(ρ_k, g)` is finite in
the range `2k > α + 2s - 1/2` of `eq:nonbandpass-order`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_viii {k : ℕ} {α s : ℝ} (hα : 0 < α)
  (hs : 1 / 2 < s) (hk : α + 2 * s - 1 / 2 < 2 * ↑k) :
  OperatorRidgelet.MemRaySobolev s
      (OperatorRidgelet.gaussSobolevRay k α) ∧
    ∀ (ω : ℝ),
      OperatorRidgelet.rayProfile (OperatorRidgelet.gaussSobolevRay k α)
          ω =
        OperatorRidgelet.filterFourier
            (⇑(OperatorRidgelet.gaussDerivFilter k)) (-ω) *
          ↑(|ω| ^ (-α))

theorem OperatorRidgelet.Paper.prop_5_12_viii
  {k : ℕ} {α s : ℝ} (hα : 0 < α)
  (hs : 1 / 2 < s)
  (hk : α + 2 * s - 1 / 2 < 2 * ↑k) :
  OperatorRidgelet.MemRaySobolev s
      (OperatorRidgelet.gaussSobolevRay k
        α) ∧
    ∀ (ω : ℝ),
      OperatorRidgelet.rayProfile
          (OperatorRidgelet.gaussSobolevRay
            k α)
          ω =
        OperatorRidgelet.filterFourier
            (⇑(OperatorRidgelet.gaussDerivFilter
                k))
            (-ω) *
          ↑(|ω| ^ (-α))

**Proposition [prop:5.12]**(viii) The Sobolev test
`q_{α,ρ_k}(ω) = ρ♯_k(-ω) |ω|^{-α}` lies in `H^s_ω(ℝ)` in the same range.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_5_12_ix.{u_1, u_2} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] [CompleteSpace Y] {k : ℕ} {α s p Cσ : ℝ} (hα : 0 < α)
  (hp : 0 ≤ p) (hps : p + 1 / 2 < s) (hk : α + 2 * s - 1 / 2 < 2 * ↑k)
  {ν : MeasureTheory.Measure H} [MeasureTheory.SFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (hB : ν (Metric.closedBall 0 1) ≠ ⊤) (v : Y) {σ : ℝ → ℂ}
  (hσc : Continuous σ) (hσg : ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p)
  (x : H) :
  ∫ (q : H × ℝ),
      σ (inner ℝ q.1 x - q.2) •
        OperatorRidgelet.gaussRayCoefficient k v
          q ∂ν.prod MeasureTheory.volume =
    OperatorRidgelet.sobolevPairing σ
        (OperatorRidgelet.gaussSobolevRay k α) •
      OperatorRidgelet.spectralTarget ν (OperatorRidgelet.gaussTarget v)
        x

theorem OperatorRidgelet.Paper.prop_5_12_ix.{u_1,
    u_2}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {H : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  [CompleteSpace Y] {k : ℕ} {α s p Cσ : ℝ}
  (hα : 0 < α) (hp : 0 ≤ p)
  (hps : p + 1 / 2 < s)
  (hk : α + 2 * s - 1 / 2 < 2 * ↑k)
  {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (hB : ν (Metric.closedBall 0 1) ≠ ⊤)
  (v : Y) {σ : ℝ → ℂ} (hσc : Continuous σ)
  (hσg :
    ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p)
  (x : H) :
  ∫ (q : H × ℝ),
      σ (inner ℝ q.1 x - q.2) •
        OperatorRidgelet.gaussRayCoefficient
          k v
          q ∂ν.prod MeasureTheory.volume =
    OperatorRidgelet.sobolevPairing σ
        (OperatorRidgelet.gaussSobolevRay
          k α) •
      OperatorRidgelet.spectralTarget ν
        (OperatorRidgelet.gaussTarget v) x

**Proposition [prop:5.12]**(ix) Consequently the filter satisfies every
hypothesis of `thm:5.10`: for each continuous activation of growth order
`p < s - 1/2` the synthesis of the coefficient is absolutely convergent and reproduces the target.

Proof for Proposition 5.12

uses 1

The Fourier transform \rho_k^\sharp is a polynomial times a Gaussian, hence Schwartz, and real and even, so its inverse Fourier transform is a real Schwartz function. It vanishes only at the origin, which is therefore in the closed support, so the filter is not band pass, while |\rho_k^\sharp|^2|\omega|^{-\alpha}=|\omega|^{4k-\alpha}e^{-2\omega^2} is integrable exactly for 4k-\alpha>-1. Homogeneity scales balls, \nu(B_R)=R^\alpha\nu(B_1), and the dyadic annuli give a geometric series, which is the moment bound. Write h_0(\omega)=\omega^{2k}e^{-\omega^2} and A=(1+\|a\|^2)^{1/2}. The function h_a(\omega)=\omega^{2k}e^{-A^2\omega^2}v has inverse transform A^{-2k-1}\rho_k(b/A)v, a dilate of a Schwartz function, so it lies in every H^s_\omega, with \|h_a\|_{H^s_\omega}\le\|v\|\,\|h_0\|_{H^s_\omega}A^{s-2k-1/2}; 1+\|a\|\le\sqrt2A and the moment bound give \mathfrak B_s<\infty exactly in the stated range. For the Sobolev test, the Gamma integral |\omega|^{-\alpha}=\Gamma(\alpha/2)^{-1}\int_0^\infty u^{\alpha/2-1}e^{-u\omega^2}\mathrm du writes q_{\alpha,\rho_k} as a superposition of the rescaled functions A^{-2k}h_0(A\,\cdot) with A=(1+u)^{1/2}; Fubini gives its inverse transform, and Cauchy--Schwarz against the finite weight u^{\alpha/2-1}(1+u)^{(s-2k-1/2)/2} together with Tonelli reduces its Sobolev norm to the norms of the dilated filters.

For the Gaussian activation, substitute \sigma^\sharp(\omega)=\sqrt{2\pi}e^{-\omega^2/2} in the pairing and evaluate \int_{\mathbb R}|\omega|^\delta e^{-3\omega^2/2}\,\mathrm d\omega by the Gamma integral. For ReLU, its Fourier transform away from zero is -\omega^{-2}. When s>3/2, the order condition gives \delta>5/2, so the origin-supported terms vanish against the Sobolev test and the remaining integral is -(2\pi)^{-1}\int_{\mathbb R}|\omega|^{\delta-2}e^{-\omega^2}\,\mathrm d\omega. This is the stated negative, nonzero Gamma constant.

The two displayed closed-form synthesis constants are part of the manuscript statement. The associated Lean statements retain their Sobolev-pairing formulations and do not assert those two closed-form evaluations.