Infinite-dimensional operator ridgelet transform

5.4. Integral representation under Sobolev conditions🔗

For the density g, write f_g(x)=\int_H e^{i\langle x,\xi\rangle}g(\xi)\,\nu(\mathrm d\xi) whenever g\in L^1(\nu;Y), and \Gamma_g=\gamma_g(\nu\otimes\mathrm db). This is the same spectral synthesis denoted g_G above when the density is written G.

Theorem5.10
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 1✓L∃∀N

Let H be a real inner-product space with its Borel structure, and let \nu be a sigma-finite Borel measure with (D_t)_\#\nu=|t|^{-\alpha}\nu for every t\ne0, where D_ta=ta and \alpha>0. Let \rho\in\mathcal S(\mathbb R;\mathbb R) be nonzero, let \sigma:\mathbb R\to\mathbb C be continuous with |\sigma(t)|\le C_\sigma(1+|t|)^p, p\ge0 and s>p+1/2, and let g:H\to Y be strongly measurable into a complex Banach space Y. Write g_a(\omega):=g(\omega a) and h_a(\omega):=\rho^\sharp(-\omega)g_a(\omega). Suppose there is a jointly measurable \gamma_g such that for almost every a, \int\langle b\rangle^{2s}\|\gamma_g(a,b)\|^2\,\mathrm db<\infty and \int\gamma_g(a,b)e^{-i\omega b}\,\mathrm db=h_a(\omega) for every \omega. For Hilbert Y this means h_a\in H^s_\omega(\mathbb R;Y) with \check h_a=\gamma_g(a,\cdot). Assume also that \mathfrak B_s(\rho,g)=\int(1+\|a\|)^s\|h_a\|_{H^s_\omega}\,\mathrm d\nu<\infty, and that q_{\alpha,\rho}(\omega)=\rho^\sharp(-\omega)|\omega|^{-\alpha} lies in H^s_\omega(\mathbb R) as a Lebesgue class, without prescribing its value at zero. Then g\in L^1(\nu;Y); for 0\le r<s-1/2 \int(1+\|a\|+|b|)^r\|\gamma_g\|\le2^{r/2}A_{s,r}\mathfrak B_s(\rho,g), so the coefficient measure is finite; the direction average \Psi_x(t)=\int\gamma_g(a,\langle a,x\rangle-t)\,\mathrm d\nu is integrable and equals \check q_{\alpha,\rho}(-t)f_g(x) almost everywhere; and the absolutely convergent network integral satisfies S_\sigma[\Gamma_g](x)=(\!(\sigma,\rho)\!)_\alpha f_g(x) with (\!(\sigma,\rho)\!)_\alpha=(2\pi)^{-1}\langle\sigma^\sharp,q_{\alpha,\rho}\rangle, uniformly absolutely on bounded input sets and continuously in x. Here A_{s,r}=(2\pi)^{-1/2}(\int_{\mathbb R}(1+t^2)^{-(s-r)}\,\mathrm dt)^{1/2}. Admissibility of \rho and non-polynomiality of \sigma are not assumed for this identity. Normalization to reproduce f_g separately requires a nonzero pairing.

If in addition Y is a separable complex Hilbert space, (\!(\rho,\rho)\!)_\alpha<\infty and g\in L^2(\nu;Y), then \gamma_g\in L^2(\nu\otimes\mathrm db;Y) and \int_{H\times\mathbb R}\|\gamma_g(a,b)\|_Y^2\,\nu(\mathrm da)\,\mathrm db=(\!(\rho,\rho)\!)_\alpha\|g\|_{L^2(\nu;Y)}^2. The Hilbert structure and separability of Y enter only in this last conclusion.

Lean code for Theorem5.10●5 theorems
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.thm_5_10_i.{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] {s r : ℝ} (hr0 : 0 ≤ r)
  (hrs : r + 1 / 2 < s) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SFinite ν] {γ : H × ℝ → Y}
  (hγm : MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν, OperatorRidgelet.MemRaySobolev s fun b => γ (a, b)) :
  ∫⁻ (q : H × ℝ),
      ENNReal.ofReal
        ((1 + ‖q.1‖ + |q.2|) ^ r * ‖γ q‖) ∂ν.prod MeasureTheory.volume ≤
    ENNReal.ofReal
        (2 ^ (r / 2) * OperatorRidgelet.sobolevMomentConst s r) *
      ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm s fun b => γ (a, b)) ∂ν
    theorem OperatorRidgelet.Paper.thm_5_10_i.{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] {s r : ℝ}
  (hr0 : 0 ≤ r) (hrs : r + 1 / 2 < s)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SFinite ν]
  {γ : H × ℝ → Y}
  (hγm :
    MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν,
      OperatorRidgelet.MemRaySobolev s
        fun b => γ (a, b)) :
  ∫⁻ (q : H × ℝ),
      ENNReal.ofReal
        ((1 + ‖q.1‖ + |q.2|) ^ r *
          ‖γ
              q‖) ∂ν.prod
        MeasureTheory.volume ≤
    ENNReal.ofReal
        (2 ^ (r / 2) *
          OperatorRidgelet.sobolevMomentConst
            s r) *
      ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm
              s fun b => γ (a, b)) ∂ν
    **Theorem [thm:5.10]**(i) The coefficient moments `eq:sobolev-moments`:
for `0 ≤ r < s - 1/2`,
`∫ (1 + ‖a‖ + |b|)^r ‖γ_g(a,b)‖ dν db ≤ 2^{r/2} A_{s,r} 𝔅_s(ρ,g)`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.thm_5_10_ii.{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] {s : ℝ} (hs : 1 / 2 < s)
  (ν : MeasureTheory.Measure H) [MeasureTheory.SFinite ν]
  {γ : H × ℝ → Y} (hγm : MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν, OperatorRidgelet.MemRaySobolev s fun b => γ (a, b))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm s fun b => γ (a, b)) ∂ν ≠
      ⊤) :
  MeasureTheory.Integrable γ (ν.prod MeasureTheory.volume)
    theorem OperatorRidgelet.Paper.thm_5_10_ii.{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] {s : ℝ}
  (hs : 1 / 2 < s)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SFinite ν]
  {γ : H × ℝ → Y}
  (hγm :
    MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν,
      OperatorRidgelet.MemRaySobolev s
        fun b => γ (a, b))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm
              s fun b => γ (a, b)) ∂ν ≠
      ⊤) :
  MeasureTheory.Integrable γ
    (ν.prod MeasureTheory.volume)
    **Theorem [thm:5.10]**(ii) The coefficient measure
`Γ_g = γ_g (ν ⊗ db)` is finite.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.thm_5_10_iii.{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] {s p α Cσ : ℝ} (hp : 0 ≤ p)
  (hps : p + 1 / 2 < s) {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν] (hν : OperatorRidgelet.IsHomogeneous α ν)
  {ρ : SchwartzMap ℝ ℝ} {g : H → Y}
  (hgm : MeasureTheory.StronglyMeasurable g) {σ : ℝ → ℂ}
  (hσc : Continuous σ) (hσg : ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p)
  {γ : H × ℝ → Y} (hγm : MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν, OperatorRidgelet.MemRaySobolev s fun b => γ (a, b))
  (hprofile :
    ∀ᵐ (a : H) ∂ν,
      ∀ (ω : ℝ),
        OperatorRidgelet.rayProfile (fun b => γ (a, b)) ω =
          OperatorRidgelet.filterFourier (⇑ρ) (-ω) • g (ω • a))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm s fun b => γ (a, b)) ∂ν ≠
      ⊤)
  {γq : ℝ → ℂ} (hγq : OperatorRidgelet.MemRaySobolev s γq)
  (hqprofile :
    ∀ (ω : ℝ),
      OperatorRidgelet.rayProfile γq ω =
        OperatorRidgelet.filterFourier (⇑ρ) (-ω) * ↑(|ω| ^ (-α)))
  (x : H) :
  ∫ (q : H × ℝ),
      σ (inner ℝ q.1 x - q.2) • γ q ∂ν.prod MeasureTheory.volume =
    OperatorRidgelet.sobolevPairing σ γq •
      OperatorRidgelet.spectralTarget ν g x
    theorem OperatorRidgelet.Paper.thm_5_10_iii.{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] {s p α Cσ : ℝ}
  (hp : 0 ≤ p) (hps : p + 1 / 2 < s)
  {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  {ρ : SchwartzMap ℝ ℝ} {g : H → Y}
  (hgm :
    MeasureTheory.StronglyMeasurable g)
  {σ : ℝ → ℂ} (hσc : Continuous σ)
  (hσg :
    ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p)
  {γ : H × ℝ → Y}
  (hγm :
    MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν,
      OperatorRidgelet.MemRaySobolev s
        fun b => γ (a, b))
  (hprofile :
    ∀ᵐ (a : H) ∂ν,
      ∀ (ω : ℝ),
        OperatorRidgelet.rayProfile
            (fun b => γ (a, b)) ω =
          OperatorRidgelet.filterFourier
              (⇑ρ) (-ω) •
            g (ω • a))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm
              s fun b => γ (a, b)) ∂ν ≠
      ⊤)
  {γq : ℝ → ℂ}
  (hγq :
    OperatorRidgelet.MemRaySobolev s γq)
  (hqprofile :
    ∀ (ω : ℝ),
      OperatorRidgelet.rayProfile γq ω =
        OperatorRidgelet.filterFourier
            (⇑ρ) (-ω) *
          ↑(|ω| ^ (-α)))
  (x : H) :
  ∫ (q : H × ℝ),
      σ (inner ℝ q.1 x - q.2) •
        γ q ∂ν.prod MeasureTheory.volume =
    OperatorRidgelet.sobolevPairing σ γq •
      OperatorRidgelet.spectralTarget ν g
        x
    **Theorem [thm:5.10]**(iii) The synthesis identity
`eq:weak-sobolev-synthesis`: the ordinary, absolutely convergent synthesis of the coefficient
is `C^{(α)}_{σ,ρ} f_g`, the cross constant being the Sobolev pairing of `σ` with the coefficient
of `q_{α,ρ}`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.thm_5_10_iv.{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] {s p Cσ R : ℝ} (hp : 0 ≤ p)
  (hps : p + 1 / 2 < s) {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν] {σ : ℝ → ℂ}
  (hσg : ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p) {γ : H × ℝ → Y}
  (hγm : MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν, OperatorRidgelet.MemRaySobolev s fun b => γ (a, b))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm s fun b => γ (a, b)) ∂ν ≠
      ⊤) :
  ∃ M,
    MeasureTheory.Integrable M (ν.prod MeasureTheory.volume) ∧
      ∀ (x : H),
        ‖x‖ ≤ R → ∀ (q : H × ℝ), ‖σ (inner ℝ q.1 x - q.2) • γ q‖ ≤ M q
    theorem OperatorRidgelet.Paper.thm_5_10_iv.{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] {s p Cσ R : ℝ}
  (hp : 0 ≤ p) (hps : p + 1 / 2 < s)
  {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν] {σ : ℝ → ℂ}
  (hσg :
    ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p)
  {γ : H × ℝ → Y}
  (hγm :
    MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν,
      OperatorRidgelet.MemRaySobolev s
        fun b => γ (a, b))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm
              s fun b => γ (a, b)) ∂ν ≠
      ⊤) :
  ∃ M,
    MeasureTheory.Integrable M
        (ν.prod MeasureTheory.volume) ∧
      ∀ (x : H),
        ‖x‖ ≤ R →
          ∀ (q : H × ℝ),
            ‖σ (inner ℝ q.1 x - q.2) •
                  γ q‖ ≤
              M q
    **Theorem [thm:5.10]**(iv) The absolute convergence is uniform on bounded
input sets: on `‖x‖ ≤ R` the synthesis integrand has one integrable majorant.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.thm_5_10_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] [CompleteSpace Y] {s p Cσ : ℝ} (hp : 0 ≤ p)
  (hps : p + 1 / 2 < s) {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν] {σ : ℝ → ℂ} (hσc : Continuous σ)
  (hσg : ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p) {γ : H × ℝ → Y}
  (hγm : MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν, OperatorRidgelet.MemRaySobolev s fun b => γ (a, b))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm s fun b => γ (a, b)) ∂ν ≠
      ⊤) :
  Continuous fun x =>
    ∫ (q : H × ℝ),
      σ (inner ℝ q.1 x - q.2) • γ q ∂ν.prod MeasureTheory.volume
    theorem OperatorRidgelet.Paper.thm_5_10_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]
  [CompleteSpace Y] {s p Cσ : ℝ}
  (hp : 0 ≤ p) (hps : p + 1 / 2 < s)
  {ν : MeasureTheory.Measure H}
  [MeasureTheory.SFinite ν] {σ : ℝ → ℂ}
  (hσc : Continuous σ)
  (hσg :
    ∀ (t : ℝ), ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p)
  {γ : H × ℝ → Y}
  (hγm :
    MeasureTheory.StronglyMeasurable γ)
  (hray :
    ∀ᵐ (a : H) ∂ν,
      OperatorRidgelet.MemRaySobolev s
        fun b => γ (a, b))
  (hB :
    ∫⁻ (a : H),
        ENNReal.ofReal
          ((1 + ‖a‖) ^ s *
            OperatorRidgelet.raySobolevNorm
              s fun b => γ (a, b)) ∂ν ≠
      ⊤) :
  Continuous fun x =>
    ∫ (q : H × ℝ),
      σ (inner ℝ q.1 x - q.2) •
        γ q ∂ν.prod MeasureTheory.volume
    **Theorem [thm:5.10]**(v) The synthesis is continuous.
Proof for Theorem 5.10
Proof uses 2
Proof dependency previews
Preview
Lemma 5.8
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

First choose \omega_0\ne0 with \rho^\sharp(-\omega_0)\ne0. The weighted inverse Fourier estimate with r=0 gives \|h_a(\omega_0)\|\le A_{s,0}\|h_a\|_{H^s_\omega}. Integrating this inequality and using homogeneity yields \|g\|_{L^1(\nu;Y)}\le |\omega_0|^\alpha |\rho^\sharp(-\omega_0)|^{-1} A_{s,0}\mathfrak B_s(\rho,g)<\infty. Thus f_g is defined, bounded, and continuous by the earlier spectral-target lemma.

The moments are the weighted L^1 estimate of Lemma 5.8 applied to b\mapsto\gamma_g(a,b), 1+\|a\|+|b|\le\sqrt2(1+\|a\|)\langle b\rangle, and Tonelli; the case r=0 gives the finite total variation of the coefficient measure, and the growth bound of \sigma with r=p gives the absolute convergence and the majorant. For the identity, Fubini in the two parameters turns the synthesis into \int\sigma(t)\Psi(t)\,\mathrm dt with \Psi(t)=\int\gamma_g(a,\langle a,x\rangle-t)\,\mathrm d\nu. Fubini again computes the profile of the integrable \Psi, which homogeneity identifies with \rho^\sharp(\omega)|\omega|^{-\alpha}f_g(x) off the origin, hence everywhere by continuity; the L^1 uniqueness of the profile then identifies \Psi with \check q_{\alpha,\rho}(-\cdot)f_g(x), and the pairing of Lemma 5.9 gives the constant. Continuity is dominated convergence with the majorant. The final clause of the manuscript statement, that \gamma_g lies in L^2(\nu\otimes\mathrm db;Y) with \|\gamma_g\|^2=(\!(\rho,\rho)\!)_\alpha\|g\|^2_{L^2(\nu;Y)} when Y is a separable complex Hilbert space, (\!(\rho,\rho)\!)_\alpha<\infty and g\in L^2(\nu;Y), is not part of the Lean statement.

The displayed statement includes the manuscript product-space L^2 conclusion. The associated Lean statements carry that clause in a weaker form; their verification does not assert the full clause as written here.

Remark 5.11 (What the synthesis identity uses).

The absolutely convergent integral representation uses the inner product and Borel structure of the input space, homogeneity of the direction measure, and completeness of the output norm. The output Hilbert structure is needed only for the L^2 coefficient conclusion. Positivity of the admissibility constant is not required. The ray hypotheses already imply G\in L^1(\nu;Y) by evaluating the weighted inverse-transform estimate at a nonzero frequency where \rho^\sharp does not vanish and then using homogeneity.

A second parameter moment needs s>5/2. With a globally Lipschitz activation, Theorem 6.5 then applies; reconstruction of f_G also requires division by a nonzero synthesis pairing. The example below verifies concrete filters without band-pass support.

Examples of filters for the reconstruction formula.

The following explicit filters meet the Sobolev criterion without band-pass support. Their coefficient estimates and constants are proved immediately below.