2.5. The finite-dimensional case and the dilation obstruction🔗

Definition2.5.1

uses 1

Used by 2

Reverse dependency previews

Preview

Corollary 2.5.2

Loading preview

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

✓L∃∀N

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 Definition2.5.1●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 G).

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

Corollary2.5.2

Statement uses 4

Statement dependency previews

Preview

Definition 2.3.1

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)\!)_\alphat_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 Corollary2.5.2●6 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.cor_finite_backprojection_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_finite_backprojection_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:finite-backprojection]** 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_finite_backprojection_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_finite_backprojection_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:finite-backprojection]** 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_finite_backprojection_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_finite_backprojection_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:finite-backprojection]** 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_finite_backprojection_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_finite_backprojection_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:finite-backprojection]** 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_finite_backprojection_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_finite_backprojection_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:finite-backprojection]** 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_finite_backprojection_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_finite_backprojection_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:finite-backprojection]** 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 2.5.2

uses 0

Here \mathcal G_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 3.2.7 (iii).

Proposition2.5.3

Statement uses 2

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

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

used by 0✓L∃∀N

Let \dim H=\infty and let W be injective, positive, self-adjoint, and trace class with eigenvectors e_j and eigenvalues w_j>0. The sets E_t, t>0, are Borel (i a) and pairwise disjoint (i b), \mathcal N(0,tW)(E_t)=1 (i c), and consequently a \sigma-finite measure dominates \mathcal N(0,tW) for at most countably many t (i d). Hence, for a bounded Borel r with \{r\ne0\} of positive measure, there is no finite complex Borel measure \Gamma on H\times\mathbb R whose bias slices satisfy \int_{E\times\mathbb R}e^{i\omega c}\,\Gamma(\mathrm da,\mathrm dc)=r(\omega)(D_{1/\omega})_\#\mathcal N(0,W)(E) for almost every \omega\ne0 (ii).

Lean code for Proposition2.5.3●5 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j) (t : ℝ) :
  MeasurableSet (OperatorRidgelet.strongLawSet (⇑e) w t)

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (t : ℝ) :
  MeasurableSet
    (OperatorRidgelet.strongLawSet (⇑e) w
      t)

**Proposition [prop:dilation-obstruction]** Dilation obstruction.  The sets `E_t` are Borel.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j) (t t' : ℝ) :
  t ≠ t' →
    Disjoint (OperatorRidgelet.strongLawSet (⇑e) w t)
      (OperatorRidgelet.strongLawSet (⇑e) w t')

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (t t' : ℝ) :
  t ≠ t' →
    Disjoint
      (OperatorRidgelet.strongLawSet (⇑e)
        w t)
      (OperatorRidgelet.strongLawSet (⇑e)
        w t')

**Proposition [prop:dilation-obstruction]** Dilation obstruction.  The sets `E_t` are pairwise
disjoint.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t → OperatorRidgelet.IsCenteredGaussian (t • W) (γ t))
  (t : ℝ) : 0 < t → (γ t) (OperatorRidgelet.strongLawSet (⇑e) w t) = 1

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t →
        OperatorRidgelet.IsCenteredGaussian
          (t • W) (γ t))
  (t : ℝ) :
  0 < t →
    (γ t)
        (OperatorRidgelet.strongLawSet
          (⇑e) w t) =
      1

**Proposition [prop:dilation-obstruction]** Dilation obstruction.  For `t > 0`,
`𝒩(0,tW)(E_t) = 1`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t → OperatorRidgelet.IsCenteredGaussian (t • W) (γ t))
  (ν : MeasureTheory.Measure H) :
  MeasureTheory.SigmaFinite ν →
    {t | 0 < t ∧ (γ t).AbsolutelyContinuous ν}.Countable

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_i_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t →
        OperatorRidgelet.IsCenteredGaussian
          (t • W) (γ t))
  (ν : MeasureTheory.Measure H) :
  MeasureTheory.SigmaFinite ν →
    {t |
        0 < t ∧
          (γ t).AbsolutelyContinuous
            ν}.Countable

**Proposition [prop:dilation-obstruction]** Dilation obstruction.  Consequently a σ-finite
measure dominates `𝒩(0,tW)` for at most countably many `t > 0`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j) (γW : MeasureTheory.Measure H)
  (hγW : OperatorRidgelet.IsCenteredGaussian W γW) (r : ℝ → ℝ)
  (hr : Measurable r) (hrb : ∃ M, ∀ (ω : ℝ), |r ω| ≤ M)
  (hr0 : 0 < MeasureTheory.volume {ω | r ω ≠ 0}) :
  ¬∃ m,
      MeasureTheory.IsFiniteMeasure m ∧
        ∃ h,
          MeasureTheory.Integrable h m ∧
            ∀ᵐ (ω : ℝ),
              ω ≠ 0 →
                ∀ (E : Set H),
                  MeasurableSet E →
                    ∫ (q : H × ℝ) in E ×ˢ Set.univ,
                        Complex.exp (↑(ω * q.2) * Complex.I) * h q ∂m =
                      ↑(r ω) *
                        ↑((MeasureTheory.Measure.map (fun a => ω⁻¹ • a)
                                γW)
                              E).toReal

theorem OperatorRidgelet.Paper.prop_dilation_obstruction_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γW : MeasureTheory.Measure H)
  (hγW :
    OperatorRidgelet.IsCenteredGaussian W
      γW)
  (r : ℝ → ℝ) (hr : Measurable r)
  (hrb : ∃ M, ∀ (ω : ℝ), |r ω| ≤ M)
  (hr0 :
    0 <
      MeasureTheory.volume
        {ω | r ω ≠ 0}) :
  ¬∃ m,
      MeasureTheory.IsFiniteMeasure m ∧
        ∃ h,
          MeasureTheory.Integrable h m ∧
            ∀ᵐ (ω : ℝ),
              ω ≠ 0 →
                ∀ (E : Set H),
                  MeasurableSet E →
                    ∫ (q : H × ℝ) in
                        E ×ˢ Set.univ,
                        Complex.exp
                            (↑(ω * q.2) *
                              Complex.I) *
                          h q ∂m =
                      ↑(r ω) *
                        ↑((MeasureTheory.Measure.map
                                (fun a =>
                                  ω⁻¹ • a)
                                γW)
                              E).toReal

**Proposition [prop:dilation-obstruction]** Dilation obstruction.  For a bounded Borel `r`
with `{r ≠ 0}` of positive Lebesgue measure, no finite complex Borel measure `Γ = h m` on
`H × ℝ` (a finite measure `m` with an integrable density `h`) has bias slices
`Γ⁺_ω(E) = ∫_{E×ℝ} e^{iωc} Γ(da,dc) = r(ω) (D_{1/ω})_# 𝒩(0,W)(E)` for almost every `ω ≠ 0`.

Proof for Proposition 2.5.3

uses 0

The strong law of large numbers for the independent normalized Gaussian coordinates gives \mathcal N(0,tW)(E_t)=1, a \sigma-finite measure has at most countably many disjoint sets of positive measure, and a measure \Gamma as in (ii) would give a finite measure dominating \mathcal N(0,W/\omega^2) for uncountably many \omega.