3.2. The frame operator and the reconstruction formula🔗

Definition3.2.1

Statement uses 2

Statement dependency previews

Preview

Definition 2.3.1

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Lemma 3.2.4

Loading preview

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

✓L∃∀N

Let \mathcal E_\alpha' be the continuous anti-dual of \mathcal E_\alpha, represented as the continuous conjugate-linear functionals on \mathcal K_\alpha. The Riesz map is J_\alpha f[g]=\langle f,g\rangle_{\mathcal E_\alpha}, with inverse J_\alpha^{-1} from the Riesz representation theorem; the transpose of U_\alpha is U_\alpha'F[g]=\langle F,U_\alpha g\rangle_{L^2(\nu_\alpha)} for F\in L^2(\nu_\alpha), and the frame operator is T_\alpha=U_\alpha'U_\alpha. With R_\rho:\mathcal E_\alpha\to L^2(\lambda_\alpha) the bounded extension of Theorem 2.4.2 (ii) and \operatorname{Ran}R_\rho its range, synthesis with the analysis filter is the transpose S_\rho=R_\rho', (S_\rho\gamma)[g]=\langle\gamma,R_\rho g\rangle_{L^2(\lambda_\alpha)}.

Lean code for Definition3.2.1●9 definitions

abbrevdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

abbrev OperatorRidgelet.SpectralAntiDual.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] : Type u_1

abbrev OperatorRidgelet.SpectralAntiDual.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Type u_1

The continuous anti-dual `𝓔' = 𝒦 →L⋆[ℂ] ℂ` of `𝓔` (represented by `𝒦`): continuous
conjugate-linear functionals.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.antiDualConj.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] (F : E →L⋆[ℂ] ℂ) : E →L[ℂ] ℂ

def OperatorRidgelet.antiDualConj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] (F : E →L⋆[ℂ] ℂ) :
  E →L[ℂ] ℂ

The continuous linear functional `g ↦ conj (F g)` of a continuous conjugate-linear
functional `F`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.rieszMap.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [MeasurableSpace H] [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsFiniteMeasure μ] :
  ↥(OperatorRidgelet.spectralRange μ ν) →L[ℂ]
    OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.rieszMap.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  ↥(OperatorRidgelet.spectralRange μ
        ν) →L[ℂ]
    OperatorRidgelet.SpectralAntiDual μ ν

The Riesz map `J : 𝓔 → 𝓔'`, `J f [g] = ⟨f, g⟩_𝓔` (`eq:riesz-map`), linear in `f` and
conjugate linear in `g`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.rieszInv.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [MeasurableSpace H] [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsFiniteMeasure μ]
  (F : OperatorRidgelet.SpectralAntiDual μ ν) :
  ↥(OperatorRidgelet.spectralRange μ ν)

def OperatorRidgelet.rieszInv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (F :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  ↥(OperatorRidgelet.spectralRange μ ν)

The inverse Riesz map `J⁻¹ : 𝓔' → 𝓔`: the vector representing a continuous conjugate-linear
functional (Riesz representation theorem, through `InnerProductSpace.toDual`).

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.transposeEmbed.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (F : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.transposeEmbed.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (F : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  OperatorRidgelet.SpectralAntiDual μ ν

The anti-dual transpose `U' : L²(ν) → 𝓔'` of the unitary `U : 𝓔 → 𝒦 ⊆ L²(ν)`,
`U' F [g] = ⟨F, U g⟩_{L²(ν)}` (`eq:transpose-analysis`).

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.frameOperator.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.frameOperator.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.SpectralAntiDual μ ν

The frame operator `T = U' U : 𝓔 → 𝓔'`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.ridgeletExtension.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (ρ : ℝ → ℝ) :
  ↥(OperatorRidgelet.spectralRange μ ν) →L[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))

def OperatorRidgelet.ridgeletExtension.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (ρ : ℝ → ℝ) :
  ↥(OperatorRidgelet.spectralRange μ
        ν) →L[ℂ]
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))

The bounded extension `R_ρ : 𝓔 → L²(λ)` of Theorem `thm:B`(ii), represented on `𝒦`: the
continuous linear map that agrees `λ`-almost everywhere with `f ↦ R_ρ f` on `U(𝒟)`, when one
exists, and `0` otherwise.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.ridgeletRange.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (ρ : ℝ → ℝ) :
  Submodule ℂ
    ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))

def OperatorRidgelet.ridgeletRange.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (ρ : ℝ → ℝ) :
  Submodule ℂ
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))

The range `Ran R_ρ ⊆ L²(λ)` of the extended transform.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.synthesis.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [MeasurableSpace H] [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsFiniteMeasure μ]
  (ρ : ℝ → ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.synthesis.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (ρ : ℝ → ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

The synthesis operator `S_ρ = R_ρ' : L²(λ) → 𝓔'`, the anti-dual transpose of the extended
transform: `(S_ρ γ)[g] = ⟨γ, R_ρ g⟩_{L²(λ)}` (`eq:weak-synthesis`).

Definition3.2.2

Statement uses 4

Statement dependency previews

Preview

Definition 2.2.5

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Proposition 3.2.6

Loading preview

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

✓L∃∀N

For \gamma\in L^2(\lambda_\alpha), define the backprojection as \Lambda_\rho=W_\rho^*. By Lemma 2.2.8, it is represented by the ray average \Lambda_\rho\gamma(\xi)=\frac1{2\pi}\int_{\mathbb R}\overline{\widehat\rho(\omega)}\,|\omega|^{-\alpha}\,\widehat\gamma(-\xi/\omega,\omega)\,\mathrm d\omega, computed from any jointly strongly measurable partial Fourier representative supplied by Lemma 2.2.7. The integral converges absolutely for almost every \xi, and its L^2(\nu_\alpha) class is independent of the representative. With P_{\mathcal K_\alpha} the orthogonal projection onto \mathcal K_\alpha, the coefficient projection is \Pi_\rho=C^{-1}W_\rho P_{\mathcal K_\alpha}\Lambda_\rho.

Lean code for Definition3.2.2●4 definitions

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.backprojectionOf.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (α : ℝ) (ρ : ℝ → ℝ)
  (Φ : H → ℝ → ℂ) (ξ : H) : ℂ

def OperatorRidgelet.backprojectionOf.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (α : ℝ)
  (ρ : ℝ → ℝ) (Φ : H → ℝ → ℂ) (ξ : H) : ℂ

The backprojection (ray average, `eq:ray-average`) of a partial bias-Fourier representative
`Φ` of a coefficient: `Λ_ρ Φ (ξ) = (2π)⁻¹ ∫ conj(ρ̂(ω)) |ω|^{-α} Φ(-ξ/ω, ω) dω`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.backprojection.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (α : ℝ) (ν : MeasureTheory.Measure H) (ρ : ℝ → ℝ) (γ : H × ℝ → ℂ) :
  H → ℂ

def OperatorRidgelet.backprojection.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (α : ℝ)
  (ν : MeasureTheory.Measure H)
  (ρ : ℝ → ℝ) (γ : H × ℝ → ℂ) : H → ℂ

The backprojection `Λ_ρ γ` of a coefficient `γ`, computed from a jointly measurable partial
bias-Fourier representative of `γ` (`HasBiasFourier`), and `0` if there is none.

`HasBiasFourier` requires the representative to be square integrable along `ν`-almost every
ray, which pins it down up to a null set on almost every ray (`HasBiasFourier.ae_ae_eq`), and
the ray substitution `(a, ω) ↦ (-ωa, ω)` preserves null sets by homogeneity; hence the ray
average does not depend on the chosen representative as an element of `L²(ν)`
(`prop_coefficient_projection_ii`).  For `γ ∈ L²(λ)` a jointly measurable representative exists
(`exists_measurable_hasBiasFourier`), so the junk value is never taken on `L²(λ)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.backprojectionLp.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (α : ℝ) (ν : MeasureTheory.Measure H) (ρ : ℝ → ℝ) (γ : H × ℝ → ℂ) :
  ↥(MeasureTheory.Lp ℂ 2 ν)

def OperatorRidgelet.backprojectionLp.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (α : ℝ)
  (ν : MeasureTheory.Measure H)
  (ρ : ℝ → ℝ) (γ : H × ℝ → ℂ) :
  ↥(MeasureTheory.Lp ℂ 2 ν)

The backprojection `Λ_ρ γ` as an element of `L²(ν)` (`0` if it is not square
integrable).

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.coefficientProjection.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (α : ℝ) (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (ρ : ℝ → ℝ) (γ : H × ℝ → ℂ) :
  ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))

def OperatorRidgelet.coefficientProjection.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H] (α : ℝ)
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (ρ : ℝ → ℝ) (γ : H × ℝ → ℂ) :
  ↥(MeasureTheory.Lp ℂ 2
      (OperatorRidgelet.parameterMeasure
        ν))

The coefficient projection `Π_ρ = C⁻¹ W_ρ P_𝒦 Λ_ρ` (`eq:coefficient-projection`), with
`P_𝒦` the orthogonal projection of `L²(ν)` onto `𝒦`.

Definition3.2.3

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Lemma 3.2.5

Loading preview

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

✓L∃∀N

For f\in L^2(\mu_Q), \xi\ne0, and \tau(\xi)=\langle Q\xi,\xi\rangle^{1/2}, the analytic continuation z\mapsto\mathcal G_Qf(z\xi)=\int_Hf(x)e^{-iz\langle x,\xi\rangle}\mu_Q(\mathrm dx) and the entire function G_f(z\xi)=e^{z^2\tau(\xi)^2/2}\mathcal G_Qf(z\xi); the Hermite coefficients \mathbb E_{\mu_Q}[f\,\mathrm{He}_n(\langle x,\xi\rangle/\tau(\xi))] with the probabilists' Hermite polynomials; and \Delta_Q, the inverse of \mathcal G_Q on its range on \mathcal D_\alpha, chosen as the element of \mathcal D_\alpha with the given transform.

Lean code for Definition3.2.3●4 definitions

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.gaussFourierLine.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (f : H → ℂ) (ξ : H) (z : ℂ) : ℂ

def OperatorRidgelet.gaussFourierLine.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ : MeasureTheory.Measure H)
  (f : H → ℂ) (ξ : H) (z : ℂ) : ℂ

The analytic continuation `z ↦ 𝒢_μ f(zξ) = ∫ f(x) e^{-iz⟪x,ξ⟫} μ(dx)` of the weighted Fourier
transform along the ray through `ξ` to complex `z`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.hermiteExtension.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (Q : H →L[ℝ] H) (f : H → ℂ) (ξ : H)
  (z : ℂ) : ℂ

def OperatorRidgelet.hermiteExtension.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ : MeasureTheory.Measure H)
  (Q : H →L[ℝ] H) (f : H → ℂ) (ξ : H)
  (z : ℂ) : ℂ

The entire function `G_f(zξ) = e^{z²τ(ξ)²/2} 𝒢_μ f(zξ)` of Lemma `lem:hermite-totality`,
with `τ(ξ)² = ⟪Qξ,ξ⟫`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.hermiteCoefficient.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (Q : H →L[ℝ] H) (f : H → ℂ) (ξ : H)
  (n : ℕ) : ℂ

def OperatorRidgelet.hermiteCoefficient.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ : MeasureTheory.Measure H)
  (Q : H →L[ℝ] H) (f : H → ℂ) (ξ : H)
  (n : ℕ) : ℂ

The Hermite coefficient `E_μ[f(x) He_n(⟪x,ξ⟫/τ(ξ))]`, `τ(ξ) = ⟪Qξ,ξ⟫^{1/2}`, with the
probabilists' Hermite polynomials `Polynomial.hermite`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.gaussFourierInv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (G : H → ℂ) :
  ↥(MeasureTheory.Lp ℂ 2 μ)

def OperatorRidgelet.gaussFourierInv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (G : H → ℂ) : ↥(MeasureTheory.Lp ℂ 2 μ)

The inverse `Δ_Q` of `𝒢_μ` on its range on `𝒟`: the element `f ∈ 𝒟` with `𝒢_μ f = G` when
one exists (it is unique by Theorem `thm:C`(iv)), and `0` otherwise.

Lemma3.2.4

Statement uses 4

Statement dependency previews

Preview

Definition 1.1.2

Loading preview

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

used by 1✓L∃∀N

Let \rho\in\mathcal S(\mathbb R) be real and \gamma\in L^1(\lambda_\alpha)\cap L^2(\lambda_\alpha). Then the integral network S_\rho[\gamma\lambda_\alpha] is a bounded Borel function on H (i), and for every g\in\mathcal D_\alpha, \langle\gamma,R_\rho g\rangle_{L^2(\lambda_\alpha)}=\int_HS_\rho[\gamma\lambda_\alpha](x)\,\overline{g(x)}\,\mu_Q(\mathrm dx) (ii), so the synthesis functional S_\rho\gamma is the integral network paired with g through \mu_Q.

Lean code for Lemma3.2.4●2 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_weak_equals_strong_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hγ :
    MeasureTheory.Integrable (↑↑γ)
      (OperatorRidgelet.parameterMeasure ν)) :
  Measurable
      (OperatorRidgelet.integralNetworkDensity (fun t => ↑(ρ t))
        (OperatorRidgelet.parameterMeasure ν) ↑↑γ) ∧
    ∃ M,
      ∀ (x : H),
        ‖OperatorRidgelet.integralNetworkDensity (fun t => ↑(ρ t))
              (OperatorRidgelet.parameterMeasure ν) (↑↑γ) x‖ ≤
          M

theorem OperatorRidgelet.Paper.lem_weak_equals_strong_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (hγ :
    MeasureTheory.Integrable (↑↑γ)
      (OperatorRidgelet.parameterMeasure
        ν)) :
  Measurable
      (OperatorRidgelet.integralNetworkDensity
        (fun t => ↑(ρ t))
        (OperatorRidgelet.parameterMeasure
          ν)
        ↑↑γ) ∧
    ∃ M,
      ∀ (x : H),
        ‖OperatorRidgelet.integralNetworkDensity
              (fun t => ↑(ρ t))
              (OperatorRidgelet.parameterMeasure
                ν)
              (↑↑γ) x‖ ≤
          M

**Lemma [lem:weak-equals-strong]** Synthesis of an integrable coefficient is the integral
network.  For real Schwartz `ρ` and `γ ∈ L¹(λ_α) ∩ L²(λ_α)`, the integral network
`S_ρ[γ λ_α]` is a bounded Borel function on `H`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_weak_equals_strong_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hγ :
    MeasureTheory.Integrable (↑↑γ)
      (OperatorRidgelet.parameterMeasure ν))
  (g : ↥(OperatorRidgelet.spectralCore μ ν)) :
  ∫ (p : H × ℝ),
      ↑↑γ p *
        (starRingEnd ℂ)
          (OperatorRidgelet.ridgelet μ (⇑ρ) (↑↑↑g)
            p) ∂OperatorRidgelet.parameterMeasure ν =
    ∫ (x : H),
      OperatorRidgelet.integralNetworkDensity (fun t => ↑(ρ t))
          (OperatorRidgelet.parameterMeasure ν) (↑↑γ) x *
        (starRingEnd ℂ) (↑↑↑g x) ∂μ

theorem OperatorRidgelet.Paper.lem_weak_equals_strong_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (hγ :
    MeasureTheory.Integrable (↑↑γ)
      (OperatorRidgelet.parameterMeasure
        ν))
  (g :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  ∫ (p : H × ℝ),
      ↑↑γ p *
        (starRingEnd ℂ)
          (OperatorRidgelet.ridgelet μ
            (⇑ρ) (↑↑↑g)
            p) ∂OperatorRidgelet.parameterMeasure
        ν =
    ∫ (x : H),
      OperatorRidgelet.integralNetworkDensity
          (fun t => ↑(ρ t))
          (OperatorRidgelet.parameterMeasure
            ν)
          (↑↑γ) x *
        (starRingEnd ℂ) (↑↑↑g x) ∂μ

**Lemma [lem:weak-equals-strong]** Synthesis of an integrable coefficient is the integral
network.  For every `g ∈ 𝒟_α`, the synthesis functional `(S_ρ γ)[g] = ⟨γ, R_ρ g⟩_{L²(λ_α)}`
of `eq:weak-synthesis` equals `∫ S_ρ[γ λ_α](x) conj(g(x)) μ_Q(dx)`.

Proof for Lemma 3.2.4

uses 0

|S_\rho[\gamma\lambda_\alpha]|\le\|\gamma\|_{L^1}\|\rho\|_\infty, and the double integral of |\gamma||g||\rho(\langle a,x\rangle+c)| is at most \|\gamma\|_{L^1}\|\rho\|_\infty\|g\|_{L^1(\mu_Q)}, so Fubini applies; \rho is real.

Lemma3.2.5

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

For f\in L^2(\mu_Q) and \xi\ne0, the function z\mapsto G_f(z\xi) is entire (i), G_f(z\xi)=\sum_{n\ge0}\frac{(-iz\tau(\xi))^n}{n!}\mathbb E_{\mu_Q}[f\,\mathrm{He}_n(\langle x,\xi\rangle/\tau(\xi))] (ii) with locally uniform convergence (iii), |G_f(z\xi)|\le\|f\|_{L^2(\mu_Q)}e^{|z|^2\tau(\xi)^2/2} (iv), and the Hermite inversion formula \mathbb E_{\mu_Q}[f\,\mathrm{He}_n(\langle x,\xi\rangle/\tau(\xi))]=\frac{i^n}{\tau(\xi)^n}\frac{\mathrm d^n}{\mathrm dt^n}\bigl(e^{t^2\tau(\xi)^2/2}\mathcal G_Qf(t\xi)\bigr)\big|_{t=0} holds (v). The coefficients, over all \xi\ne0 and n, determine f in L^2(\mu_Q) (vi).

Lean code for Lemma3.2.5●6 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_hermite_totality_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H) (hξ : ξ ≠ 0) :
  Differentiable ℂ (OperatorRidgelet.hermiteExtension μ Q f ξ)

theorem OperatorRidgelet.Paper.lem_hermite_totality_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H)
  (hξ : ξ ≠ 0) :
  Differentiable ℂ
    (OperatorRidgelet.hermiteExtension μ Q
      f ξ)

**Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
For `f ∈ L²(μ_Q)` and `ξ ≠ 0`, `z ↦ G_f(zξ) = e^{z²τ(ξ)²/2} 𝒢_Q f(zξ)` is entire.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_hermite_totality_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H) (hξ : ξ ≠ 0) (z : ℂ) :
  HasSum
    (fun n =>
      (-(Complex.I * z * ↑√(inner ℝ (Q ξ) ξ))) ^ n / ↑n.factorial *
        OperatorRidgelet.hermiteCoefficient μ Q f ξ n)
    (OperatorRidgelet.hermiteExtension μ Q f ξ z)

theorem OperatorRidgelet.Paper.lem_hermite_totality_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H)
  (hξ : ξ ≠ 0) (z : ℂ) :
  HasSum
    (fun n =>
      (-(Complex.I * z *
                ↑√(inner ℝ (Q ξ) ξ))) ^
            n /
          ↑n.factorial *
        OperatorRidgelet.hermiteCoefficient
          μ Q f ξ n)
    (OperatorRidgelet.hermiteExtension μ Q
      f ξ z)

**Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite series `G_f(zξ) = ∑ₙ (-izτ(ξ))^n/n! E_{μ_Q}[f He_n(⟨x,ξ⟩/τ(ξ))]` converges for every
`z`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_hermite_totality_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H) (hξ : ξ ≠ 0) :
  TendstoLocallyUniformly
    (fun N z =>
      ∑ n ∈ Finset.range N,
        (-(Complex.I * z * ↑√(inner ℝ (Q ξ) ξ))) ^ n / ↑n.factorial *
          OperatorRidgelet.hermiteCoefficient μ Q f ξ n)
    (OperatorRidgelet.hermiteExtension μ Q f ξ) Filter.atTop

theorem OperatorRidgelet.Paper.lem_hermite_totality_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H)
  (hξ : ξ ≠ 0) :
  TendstoLocallyUniformly
    (fun N z =>
      ∑ n ∈ Finset.range N,
        (-(Complex.I * z *
                  ↑√(inner ℝ (Q ξ) ξ))) ^
              n /
            ↑n.factorial *
          OperatorRidgelet.hermiteCoefficient
            μ Q f ξ n)
    (OperatorRidgelet.hermiteExtension μ Q
      f ξ)
    Filter.atTop

**Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite series converges locally uniformly in `z`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_hermite_totality_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H) (hξ : ξ ≠ 0) (z : ℂ) :
  ‖OperatorRidgelet.hermiteExtension μ Q f ξ z‖ ≤
    √(∫ (x : H), ‖f x‖ ^ 2 ∂μ) *
      Real.exp (‖z‖ ^ 2 * inner ℝ (Q ξ) ξ / 2)

theorem OperatorRidgelet.Paper.lem_hermite_totality_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H)
  (hξ : ξ ≠ 0) (z : ℂ) :
  ‖OperatorRidgelet.hermiteExtension μ Q f
        ξ z‖ ≤
    √(∫ (x : H), ‖f x‖ ^ 2 ∂μ) *
      Real.exp
        (‖z‖ ^ 2 * inner ℝ (Q ξ) ξ / 2)

**Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The bound `|G_f(zξ)| ≤ ‖f‖_{L²(μ_Q)} e^{|z|²τ(ξ)²/2}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_hermite_totality_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H) (hξ : ξ ≠ 0) (n : ℕ) :
  OperatorRidgelet.hermiteCoefficient μ Q f ξ n =
    Complex.I ^ n / ↑√(inner ℝ (Q ξ) ξ) ^ n *
      iteratedDeriv n
        (fun t => OperatorRidgelet.hermiteExtension μ Q f ξ ↑t) 0

theorem OperatorRidgelet.Paper.lem_hermite_totality_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (ξ : H)
  (hξ : ξ ≠ 0) (n : ℕ) :
  OperatorRidgelet.hermiteCoefficient μ Q
      f ξ n =
    Complex.I ^ n /
        ↑√(inner ℝ (Q ξ) ξ) ^ n *
      iteratedDeriv n
        (fun t =>
          OperatorRidgelet.hermiteExtension
            μ Q f ξ ↑t)
        0

**Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite inversion formula `eq:hermite-inversion` holds for `f ∈ L²(μ_Q)` and `ξ ≠ 0`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_hermite_totality_vi.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  [Nontrivial H] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ) (g : H → ℂ) :
  MeasureTheory.MemLp g 2 μ →
    (∀ (ξ : H),
        ξ ≠ 0 →
          ∀ (n : ℕ),
            OperatorRidgelet.hermiteCoefficient μ Q f ξ n =
              OperatorRidgelet.hermiteCoefficient μ Q g ξ n) →
      f =ᵐ[μ] g

theorem OperatorRidgelet.Paper.lem_hermite_totality_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  [Nontrivial H] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ)
  (g : H → ℂ) :
  MeasureTheory.MemLp g 2 μ →
    (∀ (ξ : H),
        ξ ≠ 0 →
          ∀ (n : ℕ),
            OperatorRidgelet.hermiteCoefficient
                μ Q f ξ n =
              OperatorRidgelet.hermiteCoefficient
                μ Q g ξ n) →
      f =ᵐ[μ] g

**Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite coefficients over all `ξ ≠ 0` and `n` determine `f` in `L²(μ_Q)`.

Proof for Lemma 3.2.5

uses 0

The generating function e^{tY-t^2/2}=\sum_n\mathrm{He}_n(Y)t^n/n! of a standard normal Y converges in L^2 locally uniformly in t\in\mathbb C; pairing with f gives the series, the bound, and termwise differentiation. For totality, finite products of Hermite polynomials in independent coordinates form a complete orthogonal system (the Wiener–Itô chaos decomposition), and polarization of Wick powers expresses them through the directional Wick powers.

Proposition3.2.6

Statement uses 5

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

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

used by 1✓L∃∀N

Let \rho be \alpha-admissible with C=(\!(\rho,\rho)\!)_\alpha and \mathcal Y=L^2(\lambda_\alpha). The ray-average integral defining \Lambda_\rho\gamma converges absolutely for \nu_\alpha-almost every \xi (i), is independent as an L^2 class of the jointly measurable Fourier representative (ii), and satisfies \|\Lambda_\rho\gamma\|_{L^2(\nu_\alpha)}\le\sqrt C\|\gamma\|_{\mathcal Y} (iii); \Lambda_\rho is the Hilbert adjoint of W_\rho (iv) and \Lambda_\rho W_\rho=C\,\mathrm{Id} (v). The operator C^{-1}W_\rho\Lambda_\rho projects onto W_\rho L^2(\nu_\alpha). The operator \Pi_\rho=C^{-1}W_\rho P_{\mathcal K_\alpha}\Lambda_\rho is the orthogonal projection onto \operatorname{Ran}R_\rho (vi), the minimum-norm solution of S_\rho\gamma=F\in\mathcal E_\alpha' is C^{-1}R_\rho J_\alpha^{-1}F (vii), and all solutions differ from it by an element of (\operatorname{Ran}R_\rho)^\perp (viii).

Lean code for Proposition3.2.6●8 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (Φ : H → ℝ → ℂ) (hΦ : Measurable (Function.uncurry Φ))
  (hγΦ : OperatorRidgelet.HasBiasFourier ν (↑↑γ) Φ) :
  ∀ᵐ (ξ : H) ∂ν,
    MeasureTheory.Integrable
      (fun ω =>
        (starRingEnd ℂ) (OperatorRidgelet.filterFourier (⇑ρ) ω) *
            ↑(|ω| ^ (-α)) *
          Φ (-(ω⁻¹ • ξ)) ω)
      MeasureTheory.volume

theorem OperatorRidgelet.Paper.prop_coefficient_projection_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (Φ : H → ℝ → ℂ)
  (hΦ : Measurable (Function.uncurry Φ))
  (hγΦ :
    OperatorRidgelet.HasBiasFourier ν
      (↑↑γ) Φ) :
  ∀ᵐ (ξ : H) ∂ν,
    MeasureTheory.Integrable
      (fun ω =>
        (starRingEnd ℂ)
              (OperatorRidgelet.filterFourier
                (⇑ρ) ω) *
            ↑(|ω| ^ (-α)) *
          Φ (-(ω⁻¹ • ξ)) ω)
      MeasureTheory.volume

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  For `γ ∈ L²(λ_α)` and a jointly measurable partial bias-Fourier representative
`Φ` of `γ`, the ray-average integral `eq:ray-average` converges absolutely for `ν_α`-almost
every `ξ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (Φ Φ' : H → ℝ → ℂ) (hΦ : Measurable (Function.uncurry Φ))
  (hΦ' : Measurable (Function.uncurry Φ'))
  (hγΦ : OperatorRidgelet.HasBiasFourier ν (↑↑γ) Φ)
  (hγΦ' : OperatorRidgelet.HasBiasFourier ν (↑↑γ) Φ') :
  OperatorRidgelet.backprojectionOf α (⇑ρ) Φ =ᵐ[ν]
    OperatorRidgelet.backprojectionOf α (⇑ρ) Φ'

theorem OperatorRidgelet.Paper.prop_coefficient_projection_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (Φ Φ' : H → ℝ → ℂ)
  (hΦ : Measurable (Function.uncurry Φ))
  (hΦ' : Measurable (Function.uncurry Φ'))
  (hγΦ :
    OperatorRidgelet.HasBiasFourier ν
      (↑↑γ) Φ)
  (hγΦ' :
    OperatorRidgelet.HasBiasFourier ν
      (↑↑γ) Φ') :
  OperatorRidgelet.backprojectionOf α (⇑ρ)
      Φ =ᵐ[ν]
    OperatorRidgelet.backprojectionOf α
      (⇑ρ) Φ'

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  As an `L²(ν_α)` class, `Λ_ρ γ` does not depend on the jointly measurable
Fourier representative of `γ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  MeasureTheory.MemLp (OperatorRidgelet.backprojection α ν ⇑ρ ↑↑γ) 2 ν ∧
    ∫ (ξ : H),
        ‖OperatorRidgelet.backprojection α ν (⇑ρ) (↑↑γ) ξ‖ ^ 2 ∂ν ≤
      OperatorRidgelet.admissibilityConst α ⇑ρ * ‖γ‖ ^ 2

theorem OperatorRidgelet.Paper.prop_coefficient_projection_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  MeasureTheory.MemLp
      (OperatorRidgelet.backprojection α ν
        ⇑ρ ↑↑γ)
      2 ν ∧
    ∫ (ξ : H),
        ‖OperatorRidgelet.backprojection α
              ν (⇑ρ) (↑↑γ) ξ‖ ^
          2 ∂ν ≤
      OperatorRidgelet.admissibilityConst
          α ⇑ρ *
        ‖γ‖ ^ 2

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Λ_ρ γ ∈ L²(ν_α)` with `‖Λ_ρ γ‖_{L²(ν_α)} ≤ √C ‖γ‖_𝒴`, `C = C^{(α)}_ρ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (F : H → ℂ) :
  Measurable F →
    MeasureTheory.MemLp F 2 ν →
      ∫ (p : H × ℝ),
          ↑↑γ p *
            (starRingEnd ℂ)
              (↑↑(OperatorRidgelet.spectralCoefficient ν (⇑ρ) F)
                p) ∂OperatorRidgelet.parameterMeasure ν =
        ∫ (ξ : H),
          OperatorRidgelet.backprojection α ν (⇑ρ) (↑↑γ) ξ *
            (starRingEnd ℂ) (F ξ) ∂ν

theorem OperatorRidgelet.Paper.prop_coefficient_projection_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (F : H → ℂ) :
  Measurable F →
    MeasureTheory.MemLp F 2 ν →
      ∫ (p : H × ℝ),
          ↑↑γ p *
            (starRingEnd ℂ)
              (↑↑(OperatorRidgelet.spectralCoefficient
                      ν (⇑ρ) F)
                p) ∂OperatorRidgelet.parameterMeasure
            ν =
        ∫ (ξ : H),
          OperatorRidgelet.backprojection
              α ν (⇑ρ) (↑↑γ) ξ *
            (starRingEnd ℂ) (F ξ) ∂ν

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Λ_ρ` is the Hilbert adjoint of `W_ρ : L²(ν_α) → 𝒴`:
`⟨γ, W_ρ F⟩_{L²(λ_α)} = ⟨Λ_ρ γ, F⟩_{L²(ν_α)}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F : H → ℂ) :
  Measurable F →
    MeasureTheory.MemLp F 2 ν →
      OperatorRidgelet.backprojection α ν ⇑ρ
          ↑↑(OperatorRidgelet.spectralCoefficient ν (⇑ρ) F) =ᵐ[ν]
        fun ξ => ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) * F ξ

theorem OperatorRidgelet.Paper.prop_coefficient_projection_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F : H → ℂ) :
  Measurable F →
    MeasureTheory.MemLp F 2 ν →
      OperatorRidgelet.backprojection α ν
          ⇑ρ
          ↑↑(OperatorRidgelet.spectralCoefficient
                ν (⇑ρ) F) =ᵐ[ν]
        fun ξ =>
        ↑(OperatorRidgelet.admissibilityConst
              α ⇑ρ) *
          F ξ

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Λ_ρ W_ρ = C Id`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.coefficientProjection α μ ν ⇑ρ ↑↑γ ∈
      OperatorRidgelet.ridgeletRange μ ν ⇑ρ ∧
    γ - OperatorRidgelet.coefficientProjection α μ ν ⇑ρ ↑↑γ ∈
      (OperatorRidgelet.ridgeletRange μ ν ⇑ρ)ᗮ

theorem OperatorRidgelet.Paper.prop_coefficient_projection_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.coefficientProjection α
        μ ν ⇑ρ ↑↑γ ∈
      OperatorRidgelet.ridgeletRange μ ν
        ⇑ρ ∧
    γ -
        OperatorRidgelet.coefficientProjection
          α μ ν ⇑ρ ↑↑γ ∈
      (OperatorRidgelet.ridgeletRange μ ν
          ⇑ρ)ᗮ

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Π_ρ = C⁻¹ W_ρ P_{𝒦_α} Λ_ρ` is the orthogonal projection onto `Ran R_ρ`:
`Π_ρ γ ∈ Ran R_ρ` and `γ - Π_ρ γ ⊥ Ran R_ρ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_vii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F : OperatorRidgelet.SpectralAntiDual μ ν) :
  OperatorRidgelet.synthesis μ ν (⇑ρ)
        (↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
          (OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
            (OperatorRidgelet.rieszInv μ ν F)) =
      F ∧
    ∀
      (γ :
        ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))),
      OperatorRidgelet.synthesis μ ν (⇑ρ) γ = F →
        ‖↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
              (OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
                (OperatorRidgelet.rieszInv μ ν F)‖ ≤
          ‖γ‖

theorem OperatorRidgelet.Paper.prop_coefficient_projection_vii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  OperatorRidgelet.synthesis μ ν (⇑ρ)
        (↑(OperatorRidgelet.admissibilityConst
                α ⇑ρ)⁻¹ •
          (OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            (OperatorRidgelet.rieszInv μ ν
              F)) =
      F ∧
    ∀
      (γ :
        ↥(MeasureTheory.Lp ℂ 2
            (OperatorRidgelet.parameterMeasure
              ν))),
      OperatorRidgelet.synthesis μ ν (⇑ρ)
            γ =
          F →
        ‖↑(OperatorRidgelet.admissibilityConst
                    α ⇑ρ)⁻¹ •
              (OperatorRidgelet.ridgeletExtension
                  μ ν ⇑ρ)
                (OperatorRidgelet.rieszInv
                  μ ν F)‖ ≤
          ‖γ‖

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  The minimum-norm solution of `S_ρ γ = F ∈ 𝓔_α'` is `C⁻¹ R_ρ J_α⁻¹ F`: it solves
the equation, and every solution has at least its norm.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.prop_coefficient_projection_viii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F : OperatorRidgelet.SpectralAntiDual μ ν)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.synthesis μ ν (⇑ρ) γ = F ↔
    γ -
        ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
          (OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
            (OperatorRidgelet.rieszInv μ ν F) ∈
      (OperatorRidgelet.ridgeletRange μ ν ⇑ρ)ᗮ

theorem OperatorRidgelet.Paper.prop_coefficient_projection_viii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F :
    OperatorRidgelet.SpectralAntiDual μ ν)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.synthesis μ ν (⇑ρ) γ =
      F ↔
    γ -
        ↑(OperatorRidgelet.admissibilityConst
                α ⇑ρ)⁻¹ •
          (OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            (OperatorRidgelet.rieszInv μ ν
              F) ∈
      (OperatorRidgelet.ridgeletRange μ ν
          ⇑ρ)ᗮ

**Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  The solutions of `S_ρ γ = F` are exactly the coefficients that differ from the
minimum-norm solution by an element of `(Ran R_ρ)^⊥`.

Proof for Proposition 3.2.6

uses 0

The change of variables \xi=-\omega a gives \frac1{2\pi}\int\int|\omega|^{-\alpha}|\widehat\gamma(-\xi/\omega,\omega)|^2\mathrm d\omega\,\nu_\alpha(\mathrm d\xi)=\|\gamma\|_{\mathcal Y}^2, and weighted Cauchy–Schwarz in \omega proves absolute convergence, representative independence, the bound, and the adjoint identity. Since R_\rho=W_\rho U_\alpha with U_\alpha unitary onto \mathcal K_\alpha, C^{-1/2}W_\rho|_{\mathcal K_\alpha} is an isometry with closed image, and R_\rho'R_\rho=CJ_\alpha (the frame identity, which is the Plancherel identity read through the transpose) identifies the kernel of R_\rho' with (\operatorname{Ran}R_\rho)^\perp.

Theorem3.2.7

Statement uses 11

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Corollary 2.5.2

Loading preview

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

✓L∃∀N

Let \alpha>0 and let \rho be an \alpha-admissible Schwartz filter. (i) The frame operator T_\alpha=U_\alpha'U_\alpha equals the Riesz map J_\alpha, an isometric bijection \mathcal E_\alpha\to\mathcal E_\alpha', and S_\rho R_\rho f=(\!(\rho,\rho)\!)_\alphaT_\alpha f for f\in\mathcal E_\alpha. (ii) For f\in\mathcal E_\alpha and g\in\mathcal E_\alpha', f=((\!(\rho,\rho)\!)_\alpha)^{-1}T_\alpha^{-1}S_\rho R_\rho f and g=((\!(\rho,\rho)\!)_\alpha)^{-1}S_\rho(R_\rho T_\alpha^{-1}g). (iii) If f\in\mathcal D_\alpha and \mathcal G_Qf\in L^1(\nu_\alpha), then T_\alpha f is represented by g_{\mathcal G_Qf} against \mu_Q; conversely, for G\in\mathcal K_\alpha, R_\rho T_\alpha^{-1}U_\alpha'G=W_\rho G, and when G\in L^1(\nu_\alpha), U_\alpha'G is represented by g_G and the second reconstruction formula is the spectral synthesis identity of Theorem 3.1.5 (ii). (iv) The backprojection \Lambda_\rho is a bounded operator L^2(\lambda_\alpha)\to L^2(\nu_\alpha) with \Lambda_\rho W_\rho=(\!(\rho,\rho)\!)_\alpha\mathrm{Id}, and \Lambda_\rho R_\rho f=(\!(\rho,\rho)\!)_\alphaU_\alpha f holds in L^2(\nu_\alpha) for every f\in\mathcal E_\alpha. For a concrete core input, it holds pointwise with U_\alpha f=\mathcal G_Qf when the continuous Fourier-slice representative is used. The remaining inversion step uses Gaussian input: the Hermite formula at \xi\ne0 recovers the Hermite coefficients of f from \mathcal G_Qf, these coefficients determine f in L^2(\mu_Q), and f=\Delta_Q[((\!(\rho,\rho)\!)_\alpha)^{-1}\Lambda_\rho R_\rho f].

Lean code for Theorem3.2.7●18 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_i_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.frameOperator μ ν f =
    (OperatorRidgelet.rieszMap μ ν) f

theorem OperatorRidgelet.Paper.thm_C_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.frameOperator μ ν f =
    (OperatorRidgelet.rieszMap μ ν) f

**Theorem [thm:C]** Reconstruction and the frame operator.  The frame operator
`T_α = U_α' U_α` equals the Riesz map `J_α`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_i_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  Isometry ⇑(OperatorRidgelet.rieszMap μ ν)

theorem OperatorRidgelet.Paper.thm_C_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  Isometry
    ⇑(OperatorRidgelet.rieszMap μ ν)

**Theorem [thm:C]** Reconstruction and the frame operator.  The Riesz map `J_α` (hence the
frame operator) is an isometry `𝓔_α → 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_i_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  Function.Bijective ⇑(OperatorRidgelet.rieszMap μ ν)

theorem OperatorRidgelet.Paper.thm_C_i_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  Function.Bijective
    ⇑(OperatorRidgelet.rieszMap μ ν)

**Theorem [thm:C]** Reconstruction and the frame operator.  The Riesz map `J_α` (hence the
frame operator) is a bijection `𝓔_α → 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_i_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.synthesis μ ν (⇑ρ)
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) •
      OperatorRidgelet.frameOperator μ ν f

theorem OperatorRidgelet.Paper.thm_C_i_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.synthesis μ ν (⇑ρ)
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f) =
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) •
      OperatorRidgelet.frameOperator μ ν f

**Theorem [thm:C]** Reconstruction and the frame operator.  The frame identity
`S_ρ R_ρ f = C^{(α)}_ρ T_α f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_ii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  f =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.synthesis μ ν (⇑ρ)
          ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f))

theorem OperatorRidgelet.Paper.thm_C_ii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  f =
    ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ)⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.synthesis μ ν
          (⇑ρ)
          ((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f))

**Theorem [thm:C]** Reconstruction and the frame operator.  The first reconstruction
formula `f = (C^{(α)}_ρ)⁻¹ T_α⁻¹ S_ρ R_ρ f` for `f ∈ 𝓔_α` (`T_α⁻¹ = J_α⁻¹` by part (i)).

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_ii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (g : OperatorRidgelet.SpectralAntiDual μ ν) :
  g =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesis μ ν (⇑ρ)
        ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
          (OperatorRidgelet.rieszInv μ ν g))

theorem OperatorRidgelet.Paper.thm_C_ii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (g :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  g =
    ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesis μ ν (⇑ρ)
        ((OperatorRidgelet.ridgeletExtension
            μ ν ⇑ρ)
          (OperatorRidgelet.rieszInv μ ν
            g))

**Theorem [thm:C]** Reconstruction and the frame operator.  The second reconstruction
formula `g = (C^{(α)}_ρ)⁻¹ S_ρ (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralCore μ ν))
  (hG :
    MeasureTheory.Integrable (OperatorRidgelet.gaussFourier μ ↑↑↑f) ν)
  (g : ↥(OperatorRidgelet.spectralCore μ ν)) :
  (OperatorRidgelet.frameOperator μ ν
        (OperatorRidgelet.spectralEmbed μ ν f))
      (OperatorRidgelet.spectralEmbed μ ν g) =
    ∫ (x : H),
      OperatorRidgelet.spectralTarget ν
          (OperatorRidgelet.gaussFourier μ ↑↑↑f) x *
        (starRingEnd ℂ) (↑↑↑g x) ∂μ

theorem OperatorRidgelet.Paper.thm_C_iii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralCore μ ν))
  (hG :
    MeasureTheory.Integrable
      (OperatorRidgelet.gaussFourier μ
        ↑↑↑f)
      ν)
  (g :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  (OperatorRidgelet.frameOperator μ ν
        (OperatorRidgelet.spectralEmbed μ
          ν f))
      (OperatorRidgelet.spectralEmbed μ ν
        g) =
    ∫ (x : H),
      OperatorRidgelet.spectralTarget ν
          (OperatorRidgelet.gaussFourier μ
            ↑↑↑f)
          x *
        (starRingEnd ℂ) (↑↑↑g x) ∂μ

**Theorem [thm:C]** Reconstruction and the frame operator.  If `f ∈ 𝒟_α` and
`𝒢_Q f ∈ L¹(ν_α)`, then `T_α f` is represented by the bounded continuous function
`g_{𝒢_Q f}`: `T_α f [g] = ∫ g_{𝒢_Q f}(x) conj(g(x)) μ_Q(dx)` for `g ∈ 𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRange μ ν)) :
  (OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
      (OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.transposeEmbed μ ν ↑G)) =
    OperatorRidgelet.spectralCoefficient ν ⇑ρ ↑↑↑G

theorem OperatorRidgelet.Paper.thm_C_iii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  (OperatorRidgelet.ridgeletExtension μ ν
        ⇑ρ)
      (OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.transposeEmbed μ
          ν ↑G)) =
    OperatorRidgelet.spectralCoefficient ν
      ⇑ρ ↑↑↑G

**Theorem [thm:C]** Reconstruction and the frame operator.  Conversely, for `G ∈ 𝒦_α` the
functional `U_α' G ∈ 𝓔_α'` satisfies `R_ρ T_α⁻¹ U_α' G = W_ρ G`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iii_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRange μ ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    ∀ (g : ↥(OperatorRidgelet.spectralCore μ ν)),
      (OperatorRidgelet.transposeEmbed μ ν ↑G)
          (OperatorRidgelet.spectralEmbed μ ν g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget ν (↑↑↑G) x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ

theorem OperatorRidgelet.Paper.thm_C_iii_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            ν)),
      (OperatorRidgelet.transposeEmbed μ ν
            ↑G)
          (OperatorRidgelet.spectralEmbed
            μ ν g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              ν (↑↑↑G) x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ

**Theorem [thm:C]** Reconstruction and the frame operator.  When `G ∈ 𝒦_α ∩ L¹(ν_α)`, the
functional `U_α' G` is represented by `g_G`: `U_α' G [g] = ∫ g_G(x) conj(g(x)) μ_Q(dx)` for
`g ∈ 𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iii_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.transposeEmbed μ ν ↑G =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesis μ ν (⇑ρ)
        (OperatorRidgelet.spectralCoefficient ν ⇑ρ ↑↑↑G)

theorem OperatorRidgelet.Paper.thm_C_iii_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.transposeEmbed μ ν ↑G =
    ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesis μ ν (⇑ρ)
        (OperatorRidgelet.spectralCoefficient
          ν ⇑ρ ↑↑↑G)

**Theorem [thm:C]** Reconstruction and the frame operator.  For `G ∈ 𝒦_α` the second
reconstruction formula applied to `U_α' G` reads `U_α' G = (C^{(α)}_ρ)⁻¹ S_ρ W_ρ G`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iii_e.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRange μ ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    MeasureTheory.Integrable
        (OperatorRidgelet.coefficientFormula ⇑ρ ↑↑↑G)
        (OperatorRidgelet.parameterMeasure ν) →
      ∀ (g : ↥(OperatorRidgelet.spectralCore μ ν)),
        (OperatorRidgelet.transposeEmbed μ ν ↑G)
            (OperatorRidgelet.spectralEmbed μ ν g) =
          ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ *
            ∫ (x : H),
              OperatorRidgelet.integralNetworkDensity (fun t => ↑(ρ t))
                  (OperatorRidgelet.parameterMeasure ν)
                  (OperatorRidgelet.coefficientFormula ⇑ρ ↑↑↑G) x *
                (starRingEnd ℂ) (↑↑↑g x) ∂μ

theorem OperatorRidgelet.Paper.thm_C_iii_e.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    MeasureTheory.Integrable
        (OperatorRidgelet.coefficientFormula
          ⇑ρ ↑↑↑G)
        (OperatorRidgelet.parameterMeasure
          ν) →
      ∀
        (g :
          ↥(OperatorRidgelet.spectralCore
              μ ν)),
        (OperatorRidgelet.transposeEmbed μ
              ν ↑G)
            (OperatorRidgelet.spectralEmbed
              μ ν g) =
          ↑(OperatorRidgelet.admissibilityConst
                  α ⇑ρ)⁻¹ *
            ∫ (x : H),
              OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(ρ t))
                  (OperatorRidgelet.parameterMeasure
                    ν)
                  (OperatorRidgelet.coefficientFormula
                    ⇑ρ ↑↑↑G)
                  x *
                (starRingEnd ℂ)
                  (↑↑↑g x) ∂μ

**Theorem [thm:C]** Reconstruction and the frame operator.  When `G ∈ 𝒦_α ∩ L¹(ν_α)` and
`γ_G ∈ L¹(λ_α)`, the second reconstruction formula for `U_α' G` is the spectral synthesis
identity: paired with `g ∈ 𝒟_α`, `U_α' G [g] = (C^{(α)}_ρ)⁻¹ ∫ S_ρ[γ_G λ_α](x) conj(g(x)) μ_Q(dx)`
(Lemma `lem:weak-equals-strong`).

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  ∃ M,
    ∀
      (γ :
        ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))),
      MeasureTheory.MemLp (OperatorRidgelet.backprojection α ν ⇑ρ ↑↑γ) 2
          ν ∧
        ∫ (ξ : H),
            ‖OperatorRidgelet.backprojection α ν (⇑ρ) (↑↑γ) ξ‖ ^ 2 ∂ν ≤
          M * ‖γ‖ ^ 2

theorem OperatorRidgelet.Paper.thm_C_iv_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  ∃ M,
    ∀
      (γ :
        ↥(MeasureTheory.Lp ℂ 2
            (OperatorRidgelet.parameterMeasure
              ν))),
      MeasureTheory.MemLp
          (OperatorRidgelet.backprojection
            α ν ⇑ρ ↑↑γ)
          2 ν ∧
        ∫ (ξ : H),
            ‖OperatorRidgelet.backprojection
                  α ν (⇑ρ) (↑↑γ) ξ‖ ^
              2 ∂ν ≤
          M * ‖γ‖ ^ 2

**Theorem [thm:C]** Reconstruction and the frame operator.  The backprojection `Λ_ρ` is a
bounded operator `L²(λ_α) → L²(ν_α)`: `Λ_ρ γ` is square integrable with
`‖Λ_ρ γ‖²_{L²(ν_α)} ≤ M ‖γ‖²_{L²(λ_α)}` for a constant `M`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (F : H → ℂ) :
  Measurable F →
    MeasureTheory.MemLp F 2 ν →
      OperatorRidgelet.backprojection α ν ⇑ρ
          ↑↑(OperatorRidgelet.spectralCoefficient ν (⇑ρ) F) =ᵐ[ν]
        fun ξ => ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) * F ξ

theorem OperatorRidgelet.Paper.thm_C_iv_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F : H → ℂ) :
  Measurable F →
    MeasureTheory.MemLp F 2 ν →
      OperatorRidgelet.backprojection α ν
          ⇑ρ
          ↑↑(OperatorRidgelet.spectralCoefficient
                ν (⇑ρ) F) =ᵐ[ν]
        fun ξ =>
        ↑(OperatorRidgelet.admissibilityConst
              α ⇑ρ) *
          F ξ

**Theorem [thm:C]** Reconstruction and the frame operator.  `Λ_ρ W_ρ = C^{(α)}_ρ Id` on
`L²(ν_α)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralCore μ ν)) (ξ : H) :
  OperatorRidgelet.backprojectionOf α (⇑ρ)
      (OperatorRidgelet.biasFourier
        (OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f))
      ξ =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) *
      OperatorRidgelet.gaussFourier μ (↑↑↑f) ξ

theorem OperatorRidgelet.Paper.thm_C_iv_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralCore μ ν))
  (ξ : H) :
  OperatorRidgelet.backprojectionOf α (⇑ρ)
      (OperatorRidgelet.biasFourier
        (OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f))
      ξ =
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) *
      OperatorRidgelet.gaussFourier μ
        (↑↑↑f) ξ

**Theorem [thm:C]** Reconstruction and the frame operator.  For `f ∈ 𝒟_α` the identity
`Λ_ρ R_ρ f = C^{(α)}_ρ 𝒢_Q f` holds pointwise in `ξ`, with `Λ_ρ` computed from the continuous
Fourier-slice representative `(a,ω) ↦ \widehat{R_ρ f}(a,ω)` of the transform.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ)
  (f : ↥(OperatorRidgelet.spectralCore μ ν)) (ξ : H) :
  ξ ≠ 0 →
    ∀ (n : ℕ),
      OperatorRidgelet.hermiteCoefficient μ Q (↑↑↑f) ξ n =
        Complex.I ^ n / ↑√(inner ℝ (Q ξ) ξ) ^ n *
          iteratedDeriv n
            (fun t => OperatorRidgelet.hermiteExtension μ Q (↑↑↑f) ξ ↑t)
            0

theorem OperatorRidgelet.Paper.thm_C_iv_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f :
    ↥(OperatorRidgelet.spectralCore μ ν))
  (ξ : H) :
  ξ ≠ 0 →
    ∀ (n : ℕ),
      OperatorRidgelet.hermiteCoefficient
          μ Q (↑↑↑f) ξ n =
        Complex.I ^ n /
            ↑√(inner ℝ (Q ξ) ξ) ^ n *
          iteratedDeriv n
            (fun t =>
              OperatorRidgelet.hermiteExtension
                μ Q (↑↑↑f) ξ ↑t)
            0

**Theorem [thm:C]** Reconstruction and the frame operator.  The Hermite inversion formula
`E_{μ_Q}[f He_n(⟨x,ξ⟩/τ(ξ))] = i^n τ(ξ)^{-n} (d/dt)^n (e^{t²τ(ξ)²/2} 𝒢_Q f(tξ))|_{t=0}`,
`τ(ξ) = ⟨Qξ,ξ⟩^{1/2}`, for `f ∈ 𝒟_α` and `ξ ≠ 0`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_e.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ)
  (f g : ↥(OperatorRidgelet.spectralCore μ ν)) :
  (∀ (ξ : H),
      ξ ≠ 0 →
        ∀ (n : ℕ),
          OperatorRidgelet.hermiteCoefficient μ Q (↑↑↑f) ξ n =
            OperatorRidgelet.hermiteCoefficient μ Q (↑↑↑g) ξ n) →
    f = g

theorem OperatorRidgelet.Paper.thm_C_iv_e.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f g :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  (∀ (ξ : H),
      ξ ≠ 0 →
        ∀ (n : ℕ),
          OperatorRidgelet.hermiteCoefficient
              μ Q (↑↑↑f) ξ n =
            OperatorRidgelet.hermiteCoefficient
              μ Q (↑↑↑g) ξ n) →
    f = g

**Theorem [thm:C]** Reconstruction and the frame operator.  The Hermite coefficients over all
`ξ ≠ 0` and `n` determine `f ∈ 𝒟_α` in `L²(μ_Q)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_f.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ)
  (f : ↥(OperatorRidgelet.spectralCore μ ν)) :
  (OperatorRidgelet.gaussFourierInv μ ν fun ξ =>
      ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ *
        OperatorRidgelet.backprojectionOf α (⇑ρ)
          (OperatorRidgelet.biasFourier
            (OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f))
          ξ) =
    ↑f

theorem OperatorRidgelet.Paper.thm_C_iv_f.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (f :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  (OperatorRidgelet.gaussFourierInv μ ν
      fun ξ =>
      ↑(OperatorRidgelet.admissibilityConst
              α ⇑ρ)⁻¹ *
        OperatorRidgelet.backprojectionOf
          α (⇑ρ)
          (OperatorRidgelet.biasFourier
            (OperatorRidgelet.ridgelet μ
              ⇑ρ ↑↑↑f))
          ξ) =
    ↑f

**Theorem [thm:C]** Reconstruction and the frame operator.  Reconstruction by
backprojection: `f = Δ_Q[(C^{(α)}_ρ)⁻¹ Λ_ρ R_ρ f]` for `f ∈ 𝒟_α`, with `Δ_Q` the inverse of
`𝒢_Q` on its range on `𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_C_iv_completion.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.backprojection α ν ⇑ρ
      ↑↑((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =ᵐ[ν]
    fun ξ => ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) * ↑↑↑f ξ

theorem OperatorRidgelet.Paper.thm_C_iv_completion.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.backprojection α ν ⇑ρ
      ↑↑((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f) =ᵐ[ν]
    fun ξ =>
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) *
      ↑↑↑f ξ

**Theorem [thm:C]** Backprojection after analysis recovers the completed spectral density.

Proof for Theorem 3.2.7

uses 0

Since U_\alpha is unitary onto \mathcal K_\alpha, U_\alpha'U_\alpha f[g]=\langle U_\alpha f,U_\alpha g\rangle=\langle f,g\rangle_{\mathcal E_\alpha}, the Riesz representation theorem makes J_\alpha an isometric bijection, and the Plancherel identity gives (S_\rho R_\rho f)[g]=\langle R_\rho f,R_\rho g\rangle=(\!(\rho,\rho)\!)_\alphaJ_\alpha f[g]; (ii) follows by applying T_\alpha^{-1} or substituting f=T_\alpha^{-1}g. Part (iii) is a Fubini computation with u=J_\alpha^{-1}U_\alpha'G and Lemma 3.2.4, and (iv) first uses \Lambda_\rho W_\rho=(\!(\rho,\rho)\!)_\alpha\mathrm{Id} from Lemma 2.2.8 and R_\rho=W_\rho U_\alpha on the completion. The pointwise core formula uses the continuous Fourier-slice representative; only the final Hermite inversion invokes Lemma 3.2.5 and Gaussian input.

Corollary3.2.8

Statement uses 3

Statement dependency previews

Preview

Lemma 2.2.6

Loading preview

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

used by 0✓L∃∀N

Let \rho be \alpha-admissible, put C=(\!(\rho,\rho)\!)_\alpha>0, and define D_\rho=C^{-1}T_\alpha^{-1}S_\rho. Then D_\rho R_\rho=\mathrm{Id} and \|D_\rho\|\le C^{-1/2}. If f\in\mathcal E_\alpha, \gamma_\delta\in L^2(\lambda_\alpha), and \|\gamma_\delta-R_\rho f\|_2\le\delta, then \|D_\rho\gamma_\delta-f\|_{\mathcal E_\alpha}\le\delta/\sqrt C. This is an estimate in the completion norm, not an ambient L^2(\mu_Q) or pointwise estimate.

Lean code for Corollary3.2.8●4 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.cor_coefficient_stability_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (α : ℝ) (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] (ρ : ℝ → ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  (OperatorRidgelet.coefficientDecoder α μ ν ρ) γ =
    (↑(OperatorRidgelet.admissibilityConst α ρ))⁻¹ •
      OperatorRidgelet.rieszInv μ ν (OperatorRidgelet.synthesis μ ν ρ γ)

theorem OperatorRidgelet.Paper.cor_coefficient_stability_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (α : ℝ) (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : ℝ → ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  (OperatorRidgelet.coefficientDecoder α μ
        ν ρ)
      γ =
    (↑(OperatorRidgelet.admissibilityConst
            α ρ))⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.synthesis μ ν ρ
          γ)

**Corollary [cor:coefficient-stability]** The decoder is C⁻¹ T⁻¹ S.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.cor_coefficient_stability_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  (OperatorRidgelet.coefficientDecoder α μ ν ⇑ρ)
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =
    f

theorem OperatorRidgelet.Paper.cor_coefficient_stability_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  (OperatorRidgelet.coefficientDecoder α μ
        ν ⇑ρ)
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f) =
    f

**Corollary [cor:coefficient-stability]** The bounded decoder is a left inverse.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.cor_coefficient_stability_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  ‖OperatorRidgelet.coefficientDecoder α μ ν ⇑ρ‖ ≤
    (√(OperatorRidgelet.admissibilityConst α ⇑ρ))⁻¹

theorem OperatorRidgelet.Paper.cor_coefficient_stability_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  ‖OperatorRidgelet.coefficientDecoder α μ
        ν ⇑ρ‖ ≤
    (√(OperatorRidgelet.admissibilityConst
          α ⇑ρ))⁻¹

**Corollary [cor:coefficient-stability]** The decoder norm is at most 1/√C.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.cor_coefficient_stability_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν))
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  {δ : ℝ}
  (hδ : ‖γ - (OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f‖ ≤ δ) :
  ‖(OperatorRidgelet.coefficientDecoder α μ ν ⇑ρ) γ - f‖ ≤
    δ / √(OperatorRidgelet.admissibilityConst α ⇑ρ)

theorem OperatorRidgelet.Paper.cor_coefficient_stability_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ ν))
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  {δ : ℝ}
  (hδ :
    ‖γ -
          (OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f‖ ≤
      δ) :
  ‖(OperatorRidgelet.coefficientDecoder α
            μ ν ⇑ρ)
          γ -
        f‖ ≤
    δ /
      √(OperatorRidgelet.admissibilityConst
          α ⇑ρ)

**Corollary [cor:coefficient-stability]** Coefficient error δ gives spectral error δ/√C.

Proof for Corollary 3.2.8

uses 0

The left-inverse identity is Theorem 3.2.7 (ii). Since the transpose S_\rho has norm at most \sqrt C and T_\alpha^{-1} is an isometry, the decoder has norm at most C^{-1}\sqrt C=C^{-1/2}. Apply this bound to \gamma_\delta-R_\rho f.