4.3. Weak Sobolev regularity along rays🔗

Lemma4.3.1

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 4.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Write H^s_\omega(\mathbb R;Y) for the profiles 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 Lemma4.3.1●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 `γ` of a ray is square integrable against the Sobolev 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 Sobolev norm `‖h‖_{H^s_ω} = (2π ∫ ⟨t⟩^{2s} ‖γ(t)‖² dt)^{1/2}` of the profile whose
inverse Fourier transform is `γ` (`eq:sobolev-norm`).

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 ray 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:sobolev-tools`, finite exactly when `s - r > 1/2`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.lem_sobolev_tools_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_sobolev_tools_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:sobolev-tools]**(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_sobolev_tools_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_sobolev_tools_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:sobolev-tools]**(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_sobolev_tools_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_sobolev_tools_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:sobolev-tools]**(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_sobolev_tools_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_sobolev_tools_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:sobolev-tools]**(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 4.3.1

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. Only the weighted L^1 bound and the reflection isometry are used for Theorem 4.3.3; the modulation bound and the joint continuity are the mapping properties of the alternative route through an H^s_\omega-valued Bochner integral.

Lemma4.3.2

uses 1used 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\widehat\sigma,\cdot\rangle to H^s_\omega. Moreover \int\sigma(u-b)\gamma(b)\,\mathrm db=L_\sigma^Y(M_uh).

Lean code for Lemma4.3.2●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:sobolev-pairing`.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.lem_sobolev_pairing_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_sobolev_pairing_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:sobolev-pairing]**(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_sobolev_pairing_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_sobolev_pairing_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:sobolev-pairing]**(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_sobolev_pairing_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_sobolev_pairing_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:sobolev-pairing]**(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 4.3.2

uses 0

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 4.3.1 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.

Theorem4.3.3

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

Let \nu be homogeneous of degree \alpha>0, let \rho\in\mathcal S(\mathbb R) be nonzero, let \sigma be continuous with |\sigma(t)|\le C_\sigma(1+|t|)^p and s>p+1/2, and let g:H\to Y be strongly measurable into a complex Banach space Y. Suppose there is a jointly measurable \gamma_g whose bias lines are the coefficients of the rays h_a(\omega)=\widehat\rho(-\omega)g(\omega a)\in H^s_\omega(\mathbb R;Y), 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)=\widehat\rho(-\omega)|\omega|^{-\alpha} lies in H^s_\omega(\mathbb R). 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 ordinary absolutely convergent synthesis satisfies S_\sigma[\Gamma_g](x)=(\!(\sigma,\rho)\!)_\alpha f_g(x) with (\!(\sigma,\rho)\!)_\alpha=(2\pi)^{-1}\langle\widehat\sigma,q_{\alpha,\rho}\rangle, uniformly absolutely on bounded input sets and continuously in x. Admissibility of \rho is not assumed, and neither the inner product nor the separability of Y is used.

Lean code for Theorem4.3.3●5 theorems

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.thm_weak_sobolev_synthesis_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_weak_sobolev_synthesis_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:weak-sobolev-synthesis]**(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_weak_sobolev_synthesis_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_weak_sobolev_synthesis_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:weak-sobolev-synthesis]**(ii) The coefficient measure
`Γ_g = γ_g (ν ⊗ db)` is finite.

theoremdefined in OperatorRidgelet/Paper/Sobolev.lean

complete

theorem OperatorRidgelet.Paper.thm_weak_sobolev_synthesis_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_weak_sobolev_synthesis_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:weak-sobolev-synthesis]**(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_weak_sobolev_synthesis_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_weak_sobolev_synthesis_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:weak-sobolev-synthesis]**(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_weak_sobolev_synthesis_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_weak_sobolev_synthesis_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:weak-sobolev-synthesis]**(v) The synthesis is continuous.

Proof for Theorem 4.3.3

uses 0

The moments are the weighted L^1 estimate of Lemma 4.3.1 on each ray, 1+\|a\|+|b|\le\sqrt2(1+\|a\|)\langle b\rangle, and Tonelli; the case r=0 gives the finite variation, 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 \widehat\rho(\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 4.3.2 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.