Infinite-dimensional operator ridgelet transform

5.3. Inverse Fourier estimates and dual pairing🔗

For Hilbert-valued profiles, H^s_\omega is the Bessel-potential space in the frequency variable. In the Banach-valued hypotheses below, the same norm notation means the displayed weighted L^2 norm of the specified inverse transform. These hypotheses are stated directly; a Fourier isometry is used only for Hilbert-valued functions.

Lemma5.8
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 5.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Use \|h\|_{H^s_\omega} for the norm of a profile h whose inverse Fourier transform \gamma=\check h satisfies \|h\|_{H^s_\omega}^2=2\pi\int\langle t\rangle^{2s}\|\gamma(t)\|^2\,\mathrm dt<\infty. For s>1/2 and 0\le r<s-1/2, \int\langle t\rangle^r\|\gamma(t)\|\,\mathrm dt\le A_{s,r}\|h\|_{H^s_\omega} with A_{s,r}=(2\pi)^{-1/2}(\int(1+t^2)^{-(s-r)}\mathrm dt)^{1/2}. Reflection Rh(\omega)=h(-\omega) is an isometry, \|M_uh\|_{H^s_\omega}\le(1+|u|)^s\|h\|_{H^s_\omega} for the modulation M_uh(\omega)=e^{iu\omega}h(\omega), and (u,h)\mapsto M_uh is jointly continuous.

Lean code for Lemma5.8●9 declarations
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.bracket (t : ℝ) : ℝ
    def OperatorRidgelet.bracket (t : ℝ) : ℝ
    The Japanese bracket `⟨t⟩ = (1 + t²)^{1/2}` on the line.
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.MemRaySobolev.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (s : ℝ) (γ : ℝ → Y) : Prop
    def OperatorRidgelet.MemRaySobolev.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (s : ℝ) (γ : ℝ → Y) :
  Prop
    The coefficient `γ : ℝ → Y` is square integrable against the weight `⟨t⟩^{2s}`.
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.raySobolevNorm.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] (s : ℝ) (γ : ℝ → Y) : ℝ
    def OperatorRidgelet.raySobolevNorm.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  (s : ℝ) (γ : ℝ → Y) : ℝ
    The weighted norm `(2π ∫ ⟨t⟩^{2s} ‖γ(t)‖² dt)^{1/2}` (`eq:sobolev-norm`). For Hilbert
`Y` and a profile `h` with inverse Fourier transform `γ`, it equals the Bessel potential norm
`‖h‖_{H^s_ω}`. For general Banach `Y`, it means the displayed quantity directly.
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.rayProfile.{u_1} {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (γ : ℝ → Y) (ω : ℝ) : Y
    def OperatorRidgelet.rayProfile.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (γ : ℝ → Y) (ω : ℝ) :
  Y
    The frequency profile `γ♯(ω) = ∫ γ(b) e^{-iωb} db` of a bias coefficient, in the angular
convention of the manuscript.
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.sobolevMomentConst (s r : ℝ) : ℝ
    def OperatorRidgelet.sobolevMomentConst
  (s r : ℝ) : ℝ
    The constant `A_{s,r} = (2π)^{-1/2}(∫_ℝ (1+t²)^{-(s-r)} dt)^{1/2}` of Lemma
`lem:5.8`, finite exactly when `s - r > 1/2`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_8_i.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {s r : ℝ} (hr0 : 0 ≤ r)
  (hrs : r + 1 / 2 < s) {γ : ℝ → Y}
  (hγ : OperatorRidgelet.MemRaySobolev s γ) :
  ∫ (t : ℝ), OperatorRidgelet.bracket t ^ r * ‖γ t‖ ≤
    OperatorRidgelet.sobolevMomentConst s r *
      OperatorRidgelet.raySobolevNorm s γ
    theorem OperatorRidgelet.Paper.lem_5_8_i.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {s r : ℝ}
  (hr0 : 0 ≤ r) (hrs : r + 1 / 2 < s)
  {γ : ℝ → Y}
  (hγ :
    OperatorRidgelet.MemRaySobolev s γ) :
  ∫ (t : ℝ),
      OperatorRidgelet.bracket t ^ r *
        ‖γ t‖ ≤
    OperatorRidgelet.sobolevMomentConst s
        r *
      OperatorRidgelet.raySobolevNorm s γ
    **Lemma [lem:5.8]**(i) The weighted inverse Fourier estimate
`∫ ⟨t⟩^r ‖γ(t)‖ dt ≤ A_{s,r} ‖h‖_{H^s_ω}` (`eq:sobolev-weighted-l1`) for `0 ≤ r < s - 1/2`,
where `γ = ȟ` and `A_{s,r} = (2π)^{-1/2}(∫ (1+t²)^{-(s-r)} dt)^{1/2}`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_8_ii.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {s : ℝ} {γ : ℝ → Y}
  (hγ : OperatorRidgelet.MemRaySobolev s γ) :
  (OperatorRidgelet.MemRaySobolev s fun t => γ (-t)) ∧
    (OperatorRidgelet.raySobolevNorm s fun t => γ (-t)) =
        OperatorRidgelet.raySobolevNorm s γ ∧
      ∀ (ω : ℝ),
        OperatorRidgelet.rayProfile (fun t => γ (-t)) ω =
          OperatorRidgelet.rayProfile γ (-ω)
    theorem OperatorRidgelet.Paper.lem_5_8_ii.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {s : ℝ} {γ : ℝ → Y}
  (hγ :
    OperatorRidgelet.MemRaySobolev s γ) :
  (OperatorRidgelet.MemRaySobolev s
      fun t => γ (-t)) ∧
    (OperatorRidgelet.raySobolevNorm s
          fun t => γ (-t)) =
        OperatorRidgelet.raySobolevNorm s
          γ ∧
      ∀ (ω : ℝ),
        OperatorRidgelet.rayProfile
            (fun t => γ (-t)) ω =
          OperatorRidgelet.rayProfile γ
            (-ω)
    **Lemma [lem:5.8]**(ii) Reflection `R h(ω) = h(-ω)` is an isometry of
`H^s_ω(ℝ;Y)`: the reflected coefficient is again in the class with the same norm, and its
profile is the reflected profile.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_8_iii.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {s : ℝ} (hs : 0 ≤ s)
  {γ : ℝ → Y} (hγ : OperatorRidgelet.MemRaySobolev s γ) (u : ℝ) :
  (OperatorRidgelet.MemRaySobolev s fun t => γ (t + u)) ∧
    (OperatorRidgelet.raySobolevNorm s fun t => γ (t + u)) ≤
        (1 + |u|) ^ s * OperatorRidgelet.raySobolevNorm s γ ∧
      ∀ (ω : ℝ),
        OperatorRidgelet.rayProfile (fun t => γ (t + u)) ω =
          Complex.exp (↑(u * ω) * Complex.I) •
            OperatorRidgelet.rayProfile γ ω
    theorem OperatorRidgelet.Paper.lem_5_8_iii.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {s : ℝ} (hs : 0 ≤ s)
  {γ : ℝ → Y}
  (hγ :
    OperatorRidgelet.MemRaySobolev s γ)
  (u : ℝ) :
  (OperatorRidgelet.MemRaySobolev s
      fun t => γ (t + u)) ∧
    (OperatorRidgelet.raySobolevNorm s
          fun t => γ (t + u)) ≤
        (1 + |u|) ^ s *
          OperatorRidgelet.raySobolevNorm
            s γ ∧
      ∀ (ω : ℝ),
        OperatorRidgelet.rayProfile
            (fun t => γ (t + u)) ω =
          Complex.exp
              (↑(u * ω) * Complex.I) •
            OperatorRidgelet.rayProfile γ
              ω
    **Lemma [lem:5.8]**(iii) Modulation `M_u h(ω) = e^{iuω} h(ω)` maps `H^s_ω(ℝ;Y)`
to itself with `‖M_u h‖_{H^s_ω} ≤ (1 + |u|)^s ‖h‖_{H^s_ω}` (`eq:sobolev-modulation`); its
coefficient is the translate `γ(· + u)`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_8_iv.{u_1, u_2} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {S : Type u_2} {l : Filter S}
  {s : ℝ} (hs : 0 ≤ s) {γ : ℝ → Y} {γ' : S → ℝ → Y} {u : S → ℝ} {u₀ : ℝ}
  (hγ : OperatorRidgelet.MemRaySobolev s γ)
  (hγ' : ∀ (i : S), OperatorRidgelet.MemRaySobolev s (γ' i))
  (hu : Filter.Tendsto u l (nhds u₀))
  (hconv :
    Filter.Tendsto
      (fun i => OperatorRidgelet.raySobolevNorm s fun t => γ' i t - γ t)
      l (nhds 0)) :
  Filter.Tendsto
    (fun i =>
      OperatorRidgelet.raySobolevNorm s fun t =>
        γ' i (t + u i) - γ (t + u₀))
    l (nhds 0)
    theorem OperatorRidgelet.Paper.lem_5_8_iv.{u_1,
    u_2}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {S : Type u_2}
  {l : Filter S} {s : ℝ} (hs : 0 ≤ s)
  {γ : ℝ → Y} {γ' : S → ℝ → Y} {u : S → ℝ}
  {u₀ : ℝ}
  (hγ :
    OperatorRidgelet.MemRaySobolev s γ)
  (hγ' :
    ∀ (i : S),
      OperatorRidgelet.MemRaySobolev s
        (γ' i))
  (hu : Filter.Tendsto u l (nhds u₀))
  (hconv :
    Filter.Tendsto
      (fun i =>
        OperatorRidgelet.raySobolevNorm s
          fun t => γ' i t - γ t)
      l (nhds 0)) :
  Filter.Tendsto
    (fun i =>
      OperatorRidgelet.raySobolevNorm s
        fun t =>
        γ' i (t + u i) - γ (t + u₀))
    l (nhds 0)
    **Lemma [lem:5.8]**(iv) The map `(u, h) ↦ M_u h` is jointly continuous: if the
biases converge and the profiles converge in `H^s_ω(ℝ;Y)`, then so do the modulated profiles.
Proof for Lemma 5.8
uses 0

The weighted L^1 bound is Cauchy--Schwarz applied to \langle t\rangle^{-(s-r)} and \langle t\rangle^{s}\|\gamma(t)\|, the scalar factor being integrable exactly when s-r>1/2. Reflection and modulation correspond to \gamma(-\cdot) and \gamma(\cdot+u) on the coefficient side, and \langle t-u\rangle\le(1+|u|)\langle t\rangle gives the modulation bound. Joint continuity reduces, by that bound and the triangle inequality, to the strong continuity of translation, which follows from the strong continuity of translation in L^2 and dominated convergence for the multiplier (\langle t\rangle/\langle t+u\rangle)^s.

The weighted L^1 estimate and reflection identity are used in the representation proof below. The modulation bound and joint continuity describe the alternative route through an H^s_\omega-valued Bochner integral.

Lemma5.9
uses 0used by 1✓L∃∀N

Let \sigma be continuous with |\sigma(t)|\le C_\sigma(1+|t|)^p, p\ge0, and s>p+1/2, and put b_{\sigma,s}=\|\langle\cdot\rangle^{-s}\sigma\|_2, which is finite. The pairing L_\sigma^Y(h)=\int\sigma(t)\check h(-t)\,\mathrm dt converges absolutely and satisfies \|L_\sigma^Y(h)\|\le(2\pi)^{-1/2}b_{\sigma,s}\|h\|_{H^s_\omega}, so it is the bounded extension of (2\pi)^{-1}\langle\sigma^\sharp,\cdot\rangle to H^s_\omega. Moreover \int\sigma(u-b)\gamma(b)\,\mathrm db=L_\sigma^Y(M_uh).

Lean code for Lemma5.9●5 declarations
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.sobolevPairing.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (σ : ℝ → ℂ) (γ : ℝ → Y) : Y
    def OperatorRidgelet.sobolevPairing.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (σ : ℝ → ℂ)
  (γ : ℝ → Y) : Y
    The Sobolev pairing `L_σ^Y(h) = ∫ σ(t) • γ(-t) dt` of an activation `σ` of polynomial
growth with the profile `h` whose inverse Fourier transform is `γ` (`eq:sobolev-pairing`).
  • defdefined in OperatorRidgelet/Sobolev/Defs.lean
    complete
    def OperatorRidgelet.sobolevPairingConst (σ : ℝ → ℂ) (s : ℝ) : ℝ
    def OperatorRidgelet.sobolevPairingConst
  (σ : ℝ → ℂ) (s : ℝ) : ℝ
    The constant `b_{σ,s} = ‖⟨·⟩^{-s} σ‖_2` of Lemma `lem:5.9`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_9_i {σ : ℝ → ℂ} {p s C : ℝ} (hp : 0 ≤ p)
  (hps : p + 1 / 2 < s) (hσ : Continuous σ)
  (hbound : ∀ (t : ℝ), ‖σ t‖ ≤ C * (1 + |t|) ^ p) :
  MeasureTheory.MemLp (fun t => OperatorRidgelet.bracket t ^ (-s) • σ t)
    2 MeasureTheory.volume
    theorem OperatorRidgelet.Paper.lem_5_9_i
  {σ : ℝ → ℂ} {p s C : ℝ} (hp : 0 ≤ p)
  (hps : p + 1 / 2 < s)
  (hσ : Continuous σ)
  (hbound :
    ∀ (t : ℝ),
      ‖σ t‖ ≤ C * (1 + |t|) ^ p) :
  MeasureTheory.MemLp
    (fun t =>
      OperatorRidgelet.bracket t ^ (-s) •
        σ t)
    2 MeasureTheory.volume
    **Lemma [lem:5.9]**(i) For a continuous activation of polynomial growth `p` and
`s > p + 1/2`, the weighted activation `⟨·⟩^{-s} σ` is square integrable, that is
`b_{σ,s} = ‖⟨·⟩^{-s}σ‖_2 < ∞`.
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_9_ii.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {σ : ℝ → ℂ} {s : ℝ}
  {γ : ℝ → Y}
  (hσ :
    MeasureTheory.MemLp
      (fun t => OperatorRidgelet.bracket t ^ (-s) • σ t) 2
      MeasureTheory.volume)
  (hγ : OperatorRidgelet.MemRaySobolev s γ) :
  MeasureTheory.Integrable (fun t => σ t • γ (-t))
      MeasureTheory.volume ∧
    ‖OperatorRidgelet.sobolevPairing σ γ‖ ≤
      OperatorRidgelet.sobolevPairingConst σ s / √(2 * Real.pi) *
        OperatorRidgelet.raySobolevNorm s γ
    theorem OperatorRidgelet.Paper.lem_5_9_ii.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] {σ : ℝ → ℂ} {s : ℝ}
  {γ : ℝ → Y}
  (hσ :
    MeasureTheory.MemLp
      (fun t =>
        OperatorRidgelet.bracket t ^
            (-s) •
          σ t)
      2 MeasureTheory.volume)
  (hγ :
    OperatorRidgelet.MemRaySobolev s γ) :
  MeasureTheory.Integrable
      (fun t => σ t • γ (-t))
      MeasureTheory.volume ∧
    ‖OperatorRidgelet.sobolevPairing σ
          γ‖ ≤
      OperatorRidgelet.sobolevPairingConst
            σ s /
          √(2 * Real.pi) *
        OperatorRidgelet.raySobolevNorm s
          γ
    **Lemma [lem:5.9]**(ii) The pairing `L_σ^Y(h) = ∫ σ(t) γ(-t) dt` converges
absolutely and is bounded: `‖L_σ^Y(h)‖ ≤ (2π)^{-1/2} b_{σ,s} ‖h‖_{H^s_ω}`, so it is an element
of the bilinear dual of `H^s_ω(ℝ;Y)` with that norm (`eq:sobolev-pairing`).
  • theoremdefined in OperatorRidgelet/Paper/Sobolev.lean
    complete
    theorem OperatorRidgelet.Paper.lem_5_9_iii.{u_1} {Y : Type u_1}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (σ : ℝ → ℂ) (γ : ℝ → Y)
  (u : ℝ) :
  ∫ (b : ℝ), σ (u - b) • γ b =
    OperatorRidgelet.sobolevPairing σ fun t => γ (t + u)
    theorem OperatorRidgelet.Paper.lem_5_9_iii.{u_1}
  {Y : Type u_1} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (σ : ℝ → ℂ)
  (γ : ℝ → Y) (u : ℝ) :
  ∫ (b : ℝ), σ (u - b) • γ b =
    OperatorRidgelet.sobolevPairing σ
      fun t => γ (t + u)
    **Lemma [lem:5.9]**(iii) The bias translation of the activation is the
modulation of the profile: `∫ σ(u - b) γ(b) db = L_σ^Y(M_u h)` (`eq:sobolev-bias-pairing`).
Proof for Lemma 5.9
uses 1

1+|t|\le\sqrt2\langle t\rangle turns the growth bound into \langle t\rangle^{-s}|\sigma(t)|\le C_\sigma2^{p/2}\langle t\rangle^{p-s}, whose square is integrable for s-p>1/2. Weighted Cauchy--Schwarz against Lemma 5.8 gives absolute convergence and the bound, the reflection isometry turning \|\gamma(-\cdot)\| into \|h\|_{H^s_\omega}. The translation formula is the change of variables b=u-t.