D.3 Filtered backprojection🔗

DefinitionAux.14

uses 1

Used by 2

Reverse dependency previews

Preview

Corollary D.2

Loading preview

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

✓L∃∀N

This is the finite-dimensional reference measure introduced in Section D.2 and used in Corollary D.2.

On H=\mathbb R^m with P=I and 0<\alpha<m, the mixture is \nu_\alpha(\mathrm da)=c_{m,\alpha}\|a\|^{\alpha-m}\,\mathrm da with c_{m,\alpha}=2^{-\alpha}\pi^{-m/2}\Gamma((m-\alpha)/2) and k_{m,\alpha}=(2\pi)^mc_{m,\alpha}; for a Gaussian density p and g=fp, the frame representative is t_f(x)=\int e^{i\langle x,\xi\rangle}\widehat g(\xi)\,\nu_\alpha(\mathrm d\xi), and (-\Delta)^s is the Fourier multiplier \|\xi\|^{2s}. For the dilation obstruction, with eigenvectors e_j and eigenvalues w_j>0 of W, the strong-law sets are E_t=\{x:\lim_n\frac1n\sum_{j\le n}\langle x,e_j\rangle^2/w_j=t\}.

Lean code for DefinitionAux.14●8 definitions

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.mixtureConst (m : ℕ) (α : ℝ) : ℝ

def OperatorRidgelet.FiniteDim.mixtureConst
  (m : ℕ) (α : ℝ) : ℝ

The constant `c_{m,α} = 2^{-α} π^{-m/2} Γ((m-α)/2)` of the finite-dimensional density.

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.directionMeasure (m : ℕ) (α : ℝ) :
  MeasureTheory.Measure (OperatorRidgelet.FiniteDim.Euclid m)

def OperatorRidgelet.FiniteDim.directionMeasure
  (m : ℕ) (α : ℝ) :
  MeasureTheory.Measure
    (OperatorRidgelet.FiniteDim.Euclid m)

The finite-dimensional reference measure `ν_α(da) = c_{m,α} ‖a‖^{α-m} da` on `ℝ^m`.

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.frameConst (m : ℕ) (α : ℝ) : ℝ

def OperatorRidgelet.FiniteDim.frameConst
  (m : ℕ) (α : ℝ) : ℝ

The constant `k_{m,α} = (2π)^m c_{m,α}` of the filtered backprojection.

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.fourier {m : ℕ}
  (g : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (ξ : OperatorRidgelet.FiniteDim.Euclid m) : ℂ

def OperatorRidgelet.FiniteDim.fourier {m : ℕ}
  (g :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (ξ :
    OperatorRidgelet.FiniteDim.Euclid m) :
  ℂ

The Fourier transform `ĝ(ξ) = ∫ g(x) exp(-i⟪x,ξ⟫) dx` on `ℝ^m`.

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.densityMeasure {m : ℕ}
  (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ) :
  MeasureTheory.Measure (OperatorRidgelet.FiniteDim.Euclid m)

def OperatorRidgelet.FiniteDim.densityMeasure
  {m : ℕ}
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ) :
  MeasureTheory.Measure
    (OperatorRidgelet.FiniteDim.Euclid m)

The measure `p dx` with a nonnegative density `p` (the pivot measure of Appendix D).

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.frameRepresentative {m : ℕ}
  (ν : MeasureTheory.Measure (OperatorRidgelet.FiniteDim.Euclid m))
  (g : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (x : OperatorRidgelet.FiniteDim.Euclid m) : ℂ

def OperatorRidgelet.FiniteDim.frameRepresentative
  {m : ℕ}
  (ν :
    MeasureTheory.Measure
      (OperatorRidgelet.FiniteDim.Euclid
        m))
  (g :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (x :
    OperatorRidgelet.FiniteDim.Euclid m) :
  ℂ

The representative `t_f(x) = ∫ exp(i⟪x,ξ⟫) ĝ(ξ) ν(dξ)` of the frame operator against the
pivot measure, for `g = f p`.

defdefined in OperatorRidgelet/FiniteDim/Defs.lean

complete

def OperatorRidgelet.FiniteDim.fracLaplacian {m : ℕ} (s : ℝ)
  (g : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (x : OperatorRidgelet.FiniteDim.Euclid m) : ℂ

def OperatorRidgelet.FiniteDim.fracLaplacian
  {m : ℕ} (s : ℝ)
  (g :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (x :
    OperatorRidgelet.FiniteDim.Euclid m) :
  ℂ

The fractional Laplacian `(-Δ)^s g` as the Fourier multiplier `‖ξ‖^{2s}` in the
manuscript's convention:
`(-Δ)^s g (x) = (2π)^{-m} ∫ exp(i⟪x,ξ⟫) ‖ξ‖^{2s} ĝ(ξ) dξ`.  For `s = -(m-α)/2` it is the
Riesz potential `(-Δ)^{-(m-α)/2}`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.strongLawSet.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (e : ℕ → H) (w : ℕ → ℝ)
  (t : ℝ) : Set H

def OperatorRidgelet.strongLawSet.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (e : ℕ → H)
  (w : ℕ → ℝ) (t : ℝ) : Set H

The set `E_t` of the dilation obstruction: inputs whose normalized coordinate sums along the
eigenvectors `e_j` with eigenvalues `w_j` satisfy the strong law with limit `t`.

CorollaryD.2

Statement uses 2

Statement dependency previews

Preview

Definition 3.10

Loading preview

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

used by 0✓L∃∀N

Let H=\mathbb R^m, 0<\alpha<m, and let p be a nondegenerate Gaussian density. If f\in L^2(p\,\mathrm dx) with g=fp\in\mathcal S(\mathbb R^m), then f\in\mathcal D_\alpha (i) and t_f=k_{m,\alpha}(-\Delta)^{-(m-\alpha)/2}g (ii). For a band-pass \rho, the synthesis S_\rho R_\rho f is represented against p\,\mathrm dx by (\!(\rho,\rho)\!)_\alpha t_f (iii), so that, distributionally, f=\frac{p^{-1}}{k_{m,\alpha}(\!(\rho,\rho)\!)_\alpha}(-\Delta)^{(m-\alpha)/2}S_\rho R_\rho f (iv). With Lebesgue direction measure and \alpha=m, t_f=(2\pi)^mg (v) and f=(2\pi)^{-m}((\!(\rho,\rho)\!)_m)^{-1}p^{-1}S_\rho R_\rho f (vi).

Lean code for CorollaryD.2●6 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_D_2_i {m : ℕ} {α : ℝ} (hα : 0 < α)
  (hαm : α < ↑m) (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ)
  (hp : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), 0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (f : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (g : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ)
  (hg :
    ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), g x = f x * ↑(p x)) :
  MeasureTheory.MemLp.toLp f hf ∈
    OperatorRidgelet.spectralCore
      (OperatorRidgelet.FiniteDim.densityMeasure p)
      (OperatorRidgelet.FiniteDim.directionMeasure m α)

theorem OperatorRidgelet.Paper.cor_D_2_i {m : ℕ}
  {α : ℝ} (hα : 0 < α) (hαm : α < ↑m)
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ)
  (hp :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid
        m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (f :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (g :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ)
  (hg :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      g x = f x * ↑(p x)) :
  MeasureTheory.MemLp.toLp f hf ∈
    OperatorRidgelet.spectralCore
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)
      (OperatorRidgelet.FiniteDim.directionMeasure
        m α)

**Corollary [cor:D.2]** The frame operator in finite dimension.  If
`f ∈ L²(p dx)` with `g = f p ∈ 𝒮(ℝ^m)`, then `f ∈ 𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_D_2_ii {m : ℕ} {α : ℝ} (hα : 0 < α)
  (hαm : α < ↑m) (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ)
  (hp : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), 0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (f : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (g : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ)
  (hg : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), g x = f x * ↑(p x))
  (x : OperatorRidgelet.FiniteDim.Euclid m) :
  OperatorRidgelet.FiniteDim.frameRepresentative
      (OperatorRidgelet.FiniteDim.directionMeasure m α) (⇑g) x =
    ↑(OperatorRidgelet.FiniteDim.frameConst m α) *
      OperatorRidgelet.FiniteDim.fracLaplacian (-((↑m - α) / 2)) (⇑g) x

theorem OperatorRidgelet.Paper.cor_D_2_ii {m : ℕ}
  {α : ℝ} (hα : 0 < α) (hαm : α < ↑m)
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ)
  (hp :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid
        m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (f :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (g :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ)
  (hg :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      g x = f x * ↑(p x))
  (x :
    OperatorRidgelet.FiniteDim.Euclid m) :
  OperatorRidgelet.FiniteDim.frameRepresentative
      (OperatorRidgelet.FiniteDim.directionMeasure
        m α)
      (⇑g) x =
    ↑(OperatorRidgelet.FiniteDim.frameConst
          m α) *
      OperatorRidgelet.FiniteDim.fracLaplacian
        (-((↑m - α) / 2)) (⇑g) x

**Corollary [cor:D.2]** The frame operator in finite dimension.  The
representative of the frame operator against the pivot measure is the Riesz potential
`t_f = ∫ e^{i⟨x,ξ⟩} ĝ(ξ) ν_α(dξ) = k_{m,α} (-Δ)^{-(m-α)/2} g`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_D_2_iii {m : ℕ} {α : ℝ} (hα : 0 < α)
  (hαm : α < ↑m) (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ)
  (hp : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), 0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (f : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (g : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ)
  (hg : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), g x = f x * ↑(p x))
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (h :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.FiniteDim.densityMeasure p))) :
  h ∈
      OperatorRidgelet.spectralCore
        (OperatorRidgelet.FiniteDim.densityMeasure p)
        (OperatorRidgelet.FiniteDim.directionMeasure m α) →
    ∫ (q : OperatorRidgelet.FiniteDim.Euclid m × ℝ),
        OperatorRidgelet.ridgelet
            (OperatorRidgelet.FiniteDim.densityMeasure p) (⇑ρ) f q *
          (starRingEnd ℂ)
            (OperatorRidgelet.ridgelet
              (OperatorRidgelet.FiniteDim.densityMeasure p) (⇑ρ) (↑↑h)
              q) ∂OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.FiniteDim.directionMeasure m α) =
      ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) *
        ∫ (x : OperatorRidgelet.FiniteDim.Euclid m),
          OperatorRidgelet.FiniteDim.frameRepresentative
              (OperatorRidgelet.FiniteDim.directionMeasure m α) (⇑g) x *
            (starRingEnd ℂ)
              (↑↑h x) ∂OperatorRidgelet.FiniteDim.densityMeasure p

theorem OperatorRidgelet.Paper.cor_D_2_iii {m : ℕ}
  {α : ℝ} (hα : 0 < α) (hαm : α < ↑m)
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ)
  (hp :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid
        m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (f :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (g :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ)
  (hg :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      g x = f x * ↑(p x))
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (h :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.FiniteDim.densityMeasure
          p))) :
  h ∈
      OperatorRidgelet.spectralCore
        (OperatorRidgelet.FiniteDim.densityMeasure
          p)
        (OperatorRidgelet.FiniteDim.directionMeasure
          m α) →
    ∫ (q :
        OperatorRidgelet.FiniteDim.Euclid
            m ×
          ℝ),
        OperatorRidgelet.ridgelet
            (OperatorRidgelet.FiniteDim.densityMeasure
              p)
            (⇑ρ) f q *
          (starRingEnd ℂ)
            (OperatorRidgelet.ridgelet
              (OperatorRidgelet.FiniteDim.densityMeasure
                p)
              (⇑ρ) (↑↑h)
              q) ∂OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.FiniteDim.directionMeasure
            m α) =
      ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ) *
        ∫ (x :
          OperatorRidgelet.FiniteDim.Euclid
            m),
          OperatorRidgelet.FiniteDim.frameRepresentative
              (OperatorRidgelet.FiniteDim.directionMeasure
                m α)
              (⇑g) x *
            (starRingEnd ℂ)
              (↑↑h
                x) ∂OperatorRidgelet.FiniteDim.densityMeasure
            p

**Corollary [cor:D.2]** The frame operator in finite dimension.  For a
band-pass `ρ`, the synthesis `S_ρ R_ρ f`, i.e. the functional `h ↦ ⟨R_ρ f, R_ρ h⟩_{L²(λ_α)}` on
`𝒟_α`, is represented against the pivot measure by `C^{(α)}_ρ t_f`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_D_2_iv {m : ℕ} {α : ℝ} (hα : 0 < α)
  (hαm : α < ↑m) (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ)
  (hp : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), 0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (f : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (g : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ)
  (hg : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), g x = f x * ↑(p x))
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (φ : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ) :
  ∫ (x : OperatorRidgelet.FiniteDim.Euclid m),
      f x * φ x ∂OperatorRidgelet.FiniteDim.densityMeasure p =
    ↑(OperatorRidgelet.FiniteDim.frameConst m α *
            OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ *
      ∫ (x : OperatorRidgelet.FiniteDim.Euclid m),
        ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) *
            OperatorRidgelet.FiniteDim.frameRepresentative
              (OperatorRidgelet.FiniteDim.directionMeasure m α) (⇑g) x *
          OperatorRidgelet.FiniteDim.fracLaplacian ((↑m - α) / 2) (⇑φ) x

theorem OperatorRidgelet.Paper.cor_D_2_iv {m : ℕ}
  {α : ℝ} (hα : 0 < α) (hαm : α < ↑m)
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ)
  (hp :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid
        m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (f :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (g :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ)
  (hg :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      g x = f x * ↑(p x))
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (φ :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ) :
  ∫ (x :
      OperatorRidgelet.FiniteDim.Euclid
        m),
      f x *
        φ
          x ∂OperatorRidgelet.FiniteDim.densityMeasure
        p =
    ↑(OperatorRidgelet.FiniteDim.frameConst
              m α *
            OperatorRidgelet.admissibilityConst
              α ⇑ρ)⁻¹ *
      ∫ (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
        ↑(OperatorRidgelet.admissibilityConst
                α ⇑ρ) *
            OperatorRidgelet.FiniteDim.frameRepresentative
              (OperatorRidgelet.FiniteDim.directionMeasure
                m α)
              (⇑g) x *
          OperatorRidgelet.FiniteDim.fracLaplacian
            ((↑m - α) / 2) (⇑φ) x

**Corollary [cor:D.2]** The frame operator in finite dimension.  The
distributional reconstruction `f = p^{-1} (k_{m,α} C^{(α)}_ρ)^{-1} (-Δ)^{(m-α)/2} S_ρ R_ρ f`,
with `S_ρ R_ρ f` represented by `C^{(α)}_ρ t_f`: tested against Schwartz functions `φ`,
`∫ f φ p dx = (k C)^{-1} ∫ (C t_f) (-Δ)^{(m-α)/2} φ dx`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_D_2_v {m : ℕ}
  (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ)
  (hp : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), 0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (f : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (g : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ)
  (hg : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), g x = f x * ↑(p x))
  (x : OperatorRidgelet.FiniteDim.Euclid m) :
  OperatorRidgelet.FiniteDim.frameRepresentative MeasureTheory.volume
      (⇑g) x =
    ↑((2 * Real.pi) ^ m) * (f x * ↑(p x))

theorem OperatorRidgelet.Paper.cor_D_2_v {m : ℕ}
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ)
  (hp :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid
        m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (f :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (g :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ)
  (hg :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      g x = f x * ↑(p x))
  (x :
    OperatorRidgelet.FiniteDim.Euclid m) :
  OperatorRidgelet.FiniteDim.frameRepresentative
      MeasureTheory.volume (⇑g) x =
    ↑((2 * Real.pi) ^ m) * (f x * ↑(p x))

**Corollary [cor:D.2]** The frame operator in finite dimension.  With
Lebesgue direction measure and `α = m`, the multiplier is one and `k = (2π)^m`:
`t_f = (2π)^m g`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_D_2_vi {m : ℕ}
  (p : OperatorRidgelet.FiniteDim.Euclid m → ℝ)
  (hp : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), 0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (f : OperatorRidgelet.FiniteDim.Euclid m → ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure p))
  (g : SchwartzMap (OperatorRidgelet.FiniteDim.Euclid m) ℂ)
  (hg : ∀ (x : OperatorRidgelet.FiniteDim.Euclid m), g x = f x * ↑(p x))
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (h :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.FiniteDim.densityMeasure p))) :
  h ∈
      OperatorRidgelet.spectralCore
        (OperatorRidgelet.FiniteDim.densityMeasure p)
        MeasureTheory.volume →
    ∫ (q : OperatorRidgelet.FiniteDim.Euclid m × ℝ),
        OperatorRidgelet.ridgelet
            (OperatorRidgelet.FiniteDim.densityMeasure p) (⇑ρ) f q *
          (starRingEnd ℂ)
            (OperatorRidgelet.ridgelet
              (OperatorRidgelet.FiniteDim.densityMeasure p) (⇑ρ) (↑↑h)
              q) ∂OperatorRidgelet.parameterMeasure
          MeasureTheory.volume =
      ∫ (x : OperatorRidgelet.FiniteDim.Euclid m),
        ↑((2 * Real.pi) ^ m *
                OperatorRidgelet.admissibilityConst ↑m ⇑ρ) *
            (f x * ↑(p x)) *
          (starRingEnd ℂ)
            (↑↑h x) ∂OperatorRidgelet.FiniteDim.densityMeasure p

theorem OperatorRidgelet.Paper.cor_D_2_vi {m : ℕ}
  (p :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℝ)
  (hp :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      0 < p x)
  (hpc : Continuous p)
  {Q :
    OperatorRidgelet.FiniteDim.Euclid
        m →L[ℝ]
      OperatorRidgelet.FiniteDim.Euclid m}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  [MeasureTheory.IsProbabilityMeasure
      (OperatorRidgelet.FiniteDim.densityMeasure
        p)]
  (hpQ :
    OperatorRidgelet.IsCenteredGaussian Q
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (f :
    OperatorRidgelet.FiniteDim.Euclid m →
      ℂ)
  (hf :
    MeasureTheory.MemLp f 2
      (OperatorRidgelet.FiniteDim.densityMeasure
        p))
  (g :
    SchwartzMap
      (OperatorRidgelet.FiniteDim.Euclid
        m)
      ℂ)
  (hg :
    ∀
      (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
      g x = f x * ↑(p x))
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (h :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.FiniteDim.densityMeasure
          p))) :
  h ∈
      OperatorRidgelet.spectralCore
        (OperatorRidgelet.FiniteDim.densityMeasure
          p)
        MeasureTheory.volume →
    ∫ (q :
        OperatorRidgelet.FiniteDim.Euclid
            m ×
          ℝ),
        OperatorRidgelet.ridgelet
            (OperatorRidgelet.FiniteDim.densityMeasure
              p)
            (⇑ρ) f q *
          (starRingEnd ℂ)
            (OperatorRidgelet.ridgelet
              (OperatorRidgelet.FiniteDim.densityMeasure
                p)
              (⇑ρ) (↑↑h)
              q) ∂OperatorRidgelet.parameterMeasure
          MeasureTheory.volume =
      ∫ (x :
        OperatorRidgelet.FiniteDim.Euclid
          m),
        ↑((2 * Real.pi) ^ m *
                OperatorRidgelet.admissibilityConst
                  ↑m ⇑ρ) *
            (f x * ↑(p x)) *
          (starRingEnd ℂ)
            (↑↑h
              x) ∂OperatorRidgelet.FiniteDim.densityMeasure
          p

**Corollary [cor:D.2]** The frame operator in finite dimension.  With
Lebesgue direction measure and `α = m`, `S_ρ R_ρ f` is represented against the pivot measure by
`(2π)^m C^{(m)}_ρ f p`, that is `f = (2π)^{-m} (C^{(m)}_ρ)^{-1} p^{-1} S_ρ R_ρ f`.

Proof for Corollary D.2

Proof uses 2

Proof dependency previews

Preview

Theorem 3.14

Loading preview

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

Here F_Qf=\widehat g, the weight \|\xi\|^{\alpha-m} is locally integrable, and Fourier inversion gives \widehat{t_f}=k_{m,\alpha}\|\xi\|^{\alpha-m}\widehat g; Fubini identifies \int t_f\overline h\,p\,\mathrm dx with \langle f,h\rangle_{\mathcal E_\alpha}, which is the frame-operator representation of Theorem 4.8 (iii).