4.4. Non-band-pass filters for Sobolev synthesis🔗

Proposition4.4.1

Statement uses 4

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

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 \widehat\rho_k(\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 of the rays is jointly measurable (v), each ray lies in H^s_\omega with profile \widehat\rho_k(-\omega)g(\omega a) (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 4.3.3 applies to this filter for every continuous activation of growth order p<s-1/2 (ix).

Lean code for Proposition4.4.1●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:nonbandpass-sobolev`.

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:nonbandpass-sobolev`.

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_nonbandpass_sobolev_i (k : ℕ) (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.gaussDerivFilter k)) ω =
    ↑(ω ^ (2 * k) * Real.exp (-ω ^ 2))

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

**Proposition [prop:nonbandpass-sobolev]**(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_nonbandpass_sobolev_ii (k : ℕ) :
  ¬OperatorRidgelet.IsBandPass (OperatorRidgelet.gaussDerivFilter k)

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

**Proposition [prop:nonbandpass-sobolev]**(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_nonbandpass_sobolev_iii {k : ℕ} {α : ℝ}
  (hα : 0 < α) (hk : α < 4 * ↑k + 1) :
  OperatorRidgelet.IsAdmissible α (OperatorRidgelet.gaussDerivFilter k)

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

**Proposition [prop:nonbandpass-sobolev]**(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_nonbandpass_sobolev_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_nonbandpass_sobolev_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:nonbandpass-sobolev]**(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_nonbandpass_sobolev_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_nonbandpass_sobolev_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:nonbandpass-sobolev]**(v) The coefficient of the rays of the filter for
the Gaussian target `g(ξ) = e^{-‖ξ‖²} v` is jointly strongly measurable.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_nonbandpass_sobolev_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_nonbandpass_sobolev_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:nonbandpass-sobolev]**(vi) Every ray lies in `H^s_ω(ℝ;Y)` and has the
profile `h_a(ω) = ρ̂_k(-ω) g(ωa)` required by `thm:weak-sobolev-synthesis`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.prop_nonbandpass_sobolev_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_nonbandpass_sobolev_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:nonbandpass-sobolev]**(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_nonbandpass_sobolev_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_nonbandpass_sobolev_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:nonbandpass-sobolev]**(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_nonbandpass_sobolev_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_nonbandpass_sobolev_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:nonbandpass-sobolev]**(ix) Consequently the filter satisfies every
hypothesis of `thm:weak-sobolev-synthesis`: for each continuous activation of growth order
`p < s - 1/2` the synthesis of the rays is absolutely convergent and reproduces the target.

Proof for Proposition 4.4.1

uses 0

The symbol is a polynomial times a Gaussian, hence Schwartz, and real and even, so its inverse angular 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 |\widehat\rho_k|^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. Writing A=(1+\|a\|^2)^{1/2}, the ray with profile \omega^{2k}e^{-A^2\omega^2}v has coefficient 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 same symbols at the scales (1+u)^{1/2}; Fubini gives its profile, 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.