3.3. Vector-valued targets🔗

Definition3.3.1

Statement uses 6

Statement dependency previews

Preview

Definition 2.2.3

Loading preview

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

used by 1✓L∃∀N

Let Y be a separable complex Hilbert space. All objects above have Y-valued versions: L^2(\mu_Q;Y), the Bochner integral \mathcal G_Qf(\xi)=\int_Hf(x)e^{-i\langle x,\xi\rangle}\mu_Q(\mathrm dx)\in Y, the core \mathcal D_\alpha(Y), the completion \mathcal E_\alpha(Y) with inner product \int\langle\mathcal G_Qf,\mathcal G_Qg\rangle_Y\mathrm d\nu_\alpha, the transform R_\rho f\in L^2(\lambda_\alpha;Y), the coefficient W_\rho G of a density G\in L^2(\nu_\alpha;Y), the anti-dual, Riesz map, frame and synthesis operators, the backprojection, and the Hermite extension. The target g_G and regularity along rays are already polymorphic in the target.

Lean code for Definition3.3.1●27 definitions

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.gaussFourierVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ : MeasureTheory.Measure H) (f : H → Y) (ξ : H) : Y

def OperatorRidgelet.gaussFourierVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ : MeasureTheory.Measure H)
  (f : H → Y) (ξ : H) : Y

The `Y`-valued weighted Fourier transform `𝒢_μ f(ξ) = ∫ e^{-i⟪x,ξ⟫} f(x) μ(dx)`, a Bochner
integral.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.ridgeletVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ : MeasureTheory.Measure H) (ρ : ℝ → ℝ) (f : H → Y) (p : H × ℝ) : Y

def OperatorRidgelet.ridgeletVec.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ : MeasureTheory.Measure H)
  (ρ : ℝ → ℝ) (f : H → Y) (p : H × ℝ) : Y

The `Y`-valued ridgelet transform `R_ρ f(a,c) = ∫ ρ(⟪a,x⟫+c) f(x) μ(dx)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.coefficientFormulaVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (ρ : ℝ → ℝ) (G : H → Y)
  (p : H × ℝ) : Y

def OperatorRidgelet.coefficientFormulaVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ρ : ℝ → ℝ) (G : H → Y) (p : H × ℝ) : Y

The explicit `Y`-valued coefficient `γ_G(a,c) = (2π)⁻¹ ∫ ρ̂(ω) e^{iωc} G(-ωa) dω`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.biasFourierVec.{u_1, u_2} {H : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (γ : H × ℝ → Y) (a : H)
  (ω : ℝ) : Y

def OperatorRidgelet.biasFourierVec.{u_1, u_2}
  {H : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (γ : H × ℝ → Y) (a : H) (ω : ℝ) : Y

The partial Fourier transform in the bias of a `Y`-valued coefficient,
`γ̂(a,ω) = ∫ e^{-iωc} γ(a,c) dc`.

structure(2 fields)defined in OperatorRidgelet/Reconstruction/Defs.lean

complete

structure OperatorRidgelet.HasBiasFourierVec.{u_1, u_2} {H : Type u_1}
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (ν : MeasureTheory.Measure H) (γ : H × ℝ → Y)
  (Φ : H → ℝ → Y) : Prop

structure OperatorRidgelet.HasBiasFourierVec.{u_1,
    u_2}
  {H : Type u_1} [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (γ : H × ℝ → Y) (Φ : H → ℝ → Y) : Prop

`HasBiasFourierVec ν γ Φ`: the partial Fourier transform in the bias of the `Y`-valued
coefficient `γ` is `Φ`: for `ν`-almost every direction the ray function `Φ(a,·)` is square
integrable and Parseval's identity against Schwartz test functions holds (the `Y`-valued form
of `HasBiasFourier`, whose docstring explains the square-integrability clause).

Fields

memLp : ∀ᵐ (a : H) ∂ν, MeasureTheory.MemLp (Φ a) 2 MeasureTheory.volume

`Φ(a,·) ∈ L²(ℝ; Y)` for `ν`-almost every direction `a`.

parseval : ∀ᵐ (a : H) ∂ν,
  ∀ (φ : SchwartzMap ℝ ℂ),
    ∫ (c : ℝ), (starRingEnd ℂ) (φ c) • γ (a, c) =
      (2 * Real.pi)⁻¹ • ∫ (ω : ℝ), (starRingEnd ℂ) (OperatorRidgelet.lineFourier (⇑φ) ω) • Φ a ω

Parseval's identity against Schwartz test functions, for `ν`-almost every direction.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.spectralCoefficientVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (ρ : ℝ → ℝ) (G : H → Y) :
  ↥(MeasureTheory.Lp Y 2 (OperatorRidgelet.parameterMeasure ν))

def OperatorRidgelet.spectralCoefficientVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (ρ : ℝ → ℝ) (G : H → Y) :
  ↥(MeasureTheory.Lp Y 2
      (OperatorRidgelet.parameterMeasure
        ν))

The `Y`-valued coefficient operator `W_ρ G ∈ L²(λ; Y)`: the element whose partial Fourier
transform in the bias is `(a,ω) ↦ ρ̂(ω) G(-ωa)`, and `0` if there is none.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.spectralInnerVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H) (f g : H → Y) : ℂ

def OperatorRidgelet.spectralInnerVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H)
  (f g : H → Y) : ℂ

The `Y`-valued spectral inner product `⟨f,g⟩_{𝓔(Y)} = ∫ ⟨𝒢_μ f, 𝒢_μ g⟩_Y dν`, linear in the
first argument as in the manuscript (Mathlib's `inner` is conjugate linear in the first).

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.spectralCoreVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (Y : Type u_2) [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp Y 2 μ)

def OperatorRidgelet.spectralCoreVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (Y : Type u_2)
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp Y 2 μ)

The `Y`-valued core `𝒟(Y) = {f ∈ L²(μ; Y) : 𝒢_μ f ∈ L²(ν; Y)}`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.gaussFourierLpVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)) :
  ↥(MeasureTheory.Lp Y 2 ν)

def OperatorRidgelet.gaussFourierLpVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f :
    ↥(OperatorRidgelet.spectralCoreVec Y μ
        ν)) :
  ↥(MeasureTheory.Lp Y 2 ν)

`𝒢_μ f` as an element of `L²(ν; Y)`, for `f ∈ 𝒟(Y)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.spectralRangeVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (Y : Type u_2) [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp Y 2 ν)

def OperatorRidgelet.spectralRangeVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (Y : Type u_2)
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp Y 2 ν)

The closed subspace `𝒦(Y) = closure (𝒢_μ 𝒟(Y)) ⊆ L²(ν; Y)`, which represents `𝓔_α(Y)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.spectralEmbedVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)) :
  ↥(OperatorRidgelet.spectralRangeVec Y μ ν)

def OperatorRidgelet.spectralEmbedVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f :
    ↥(OperatorRidgelet.spectralCoreVec Y μ
        ν)) :
  ↥(OperatorRidgelet.spectralRangeVec Y μ
      ν)

The map `U : 𝒟(Y) → 𝒦(Y)`, `f ↦ 𝒢_μ f`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.ridgeletExtensionVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (Y : Type u_2) [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (ρ : ℝ → ℝ) :
  ↥(OperatorRidgelet.spectralRangeVec Y μ ν) →L[ℂ]
    ↥(MeasureTheory.Lp Y 2 (OperatorRidgelet.parameterMeasure ν))

def OperatorRidgelet.ridgeletExtensionVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (Y : Type u_2)
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (ρ : ℝ → ℝ) :
  ↥(OperatorRidgelet.spectralRangeVec Y μ
        ν) →L[ℂ]
    ↥(MeasureTheory.Lp Y 2
        (OperatorRidgelet.parameterMeasure
          ν))

The bounded extension `R_ρ : 𝓔(Y) → L²(λ; Y)`, represented on `𝒦(Y)`: the continuous linear
map agreeing almost everywhere with `f ↦ R_ρ f` on `U(𝒟(Y))`, when one exists, and `0`
otherwise.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

abbrevdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

abbrev OperatorRidgelet.SpectralAntiDualVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (Y : Type u_2) [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] : Type (max u_1 u_2)

abbrev OperatorRidgelet.SpectralAntiDualVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (Y : Type u_2)
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Type (max u_1 u_2)

The continuous anti-dual `𝓔(Y)' = 𝒦(Y) →L⋆[ℂ] ℂ`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.rieszMapVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (Y : Type u_2) [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  ↥(OperatorRidgelet.spectralRangeVec Y μ ν) →L[ℂ]
    OperatorRidgelet.SpectralAntiDualVec Y μ ν

def OperatorRidgelet.rieszMapVec.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (Y : Type u_2)
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  ↥(OperatorRidgelet.spectralRangeVec Y μ
        ν) →L[ℂ]
    OperatorRidgelet.SpectralAntiDualVec Y
      μ ν

The `Y`-valued Riesz map `J : 𝓔(Y) → 𝓔(Y)'`, `J f [g] = ⟨f, g⟩_{𝓔(Y)}`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.rieszInvVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsFiniteMeasure μ]
  (F : OperatorRidgelet.SpectralAntiDualVec Y μ ν) :
  ↥(OperatorRidgelet.spectralRangeVec Y μ ν)

def OperatorRidgelet.rieszInvVec.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (F :
    OperatorRidgelet.SpectralAntiDualVec Y
      μ ν) :
  ↥(OperatorRidgelet.spectralRangeVec Y μ
      ν)

The `Y`-valued inverse Riesz map `J⁻¹ : 𝓔(Y)' → 𝓔(Y)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued transpose `U' : L²(ν; Y) → 𝓔(Y)'`, `U' F [g] = ⟨F, U g⟩_{L²(ν;Y)}`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.frameOperatorVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  OperatorRidgelet.SpectralAntiDualVec Y μ ν

def OperatorRidgelet.frameOperatorVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  OperatorRidgelet.SpectralAntiDualVec Y μ
    ν

The `Y`-valued frame operator `T = U' U : 𝓔(Y) → 𝓔(Y)'`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued synthesis operator `S_ρ = R_ρ' : L²(λ; Y) → 𝓔(Y)'`,
`(S_ρ γ)[g] = ⟨γ, R_ρ g⟩_{L²(λ;Y)}`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.backprojectionOfVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (α : ℝ) (ρ : ℝ → ℝ)
  (Φ : H → ℝ → Y) (ξ : H) : Y

def OperatorRidgelet.backprojectionOfVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (α : ℝ) (ρ : ℝ → ℝ) (Φ : H → ℝ → Y)
  (ξ : H) : Y

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued backprojection `Λ_ρ γ`, computed from a jointly strongly measurable partial
bias-Fourier representative of `γ`, and `0` if there is none.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued backprojection `Λ_ρ γ` as an element of `L²(ν; Y)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued coefficient projection `Π_ρ = C⁻¹ W_ρ P_{𝒦(Y)} Λ_ρ`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The analytic continuation `z ↦ 𝒢_μ f(zξ)` of the `Y`-valued weighted Fourier transform along
the ray through `ξ`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued entire function `G_f(zξ) = e^{z²τ(ξ)²/2} 𝒢_μ f(zξ)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The `Y`-valued Hermite coefficient `E_μ[He_n(⟪x,ξ⟫/τ(ξ)) f(x)]`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The inverse `Δ_Q` of the `Y`-valued `𝒢_μ` on its range on `𝒟(Y)`.

Theorem3.3.2

Statement uses 8

Statement dependency previews

Preview

Lemma 2.2.7

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 5.3.1

Loading preview

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

✓L∃∀N

Theorem 3.1.5, Theorem 2.4.2, and Theorem 3.2.7 hold for Y-valued targets, with the same constants, with absolute values replaced by norms in Y, scalar integrals by Bochner integrals, and L^2 spaces by their Y-valued counterparts. The Riesz map and its inverse are isometries; their operator norms are one for Y\ne\{0\} and zero for Y=\{0\}. The L^1 input injectivity statement, admissible Schwartz synthesis and frame identities, completed L^2 backprojection, and jointly absolutely integrable tempered synthesis all retain the corresponding scalar assumptions. The Lean statements are one theorem per part of the three scalar theorems (Theorem 2.4.2 in the abstract-pair form of Theorem 2.4.1); the scalar existence claim of Theorem 3.1.5 (iii) is not repeated.

Lean code for Theorem3.3.2●35 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_i_a.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν) (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G x‖ ≤ ∫ (ξ : H), ‖G ξ‖ ∂ν

theorem OperatorRidgelet.Paper.thm_vector_valued_A_i_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G
        x‖ ≤
    ∫ (ξ : H), ‖G ξ‖ ∂ν

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(i) for `Y`-valued
densities: `‖g_G(x)‖_Y ≤ ‖G‖_{L¹(ν_α;Y)}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_i_b.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν) :
  Continuous (OperatorRidgelet.spectralTarget ν G)

theorem OperatorRidgelet.Paper.thm_vector_valued_A_i_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν) :
  Continuous
    (OperatorRidgelet.spectralTarget ν G)

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(i) for `Y`-valued
densities: `g_G` is continuous.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_i_c.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (h : OperatorRidgelet.spectralTarget ν G = 0) : G =ᵐ[ν] 0

theorem OperatorRidgelet.Paper.thm_vector_valued_A_i_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (h :
    OperatorRidgelet.spectralTarget ν G =
      0) :
  G =ᵐ[ν] 0

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(i) for `Y`-valued
densities: `g_G = 0` only if `G = 0` `ν_α`-almost everywhere.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_ii_a.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν) (hG₂ : MeasureTheory.MemLp G 2 ν)
  (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          ↑(ρ (inner ℝ a x + c)) •
            OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
      (fun a =>
        ∫ (c : ℝ),
          ↑(ρ (inner ℝ a x + c)) •
            OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c))
      ν

theorem OperatorRidgelet.Paper.thm_vector_valued_A_ii_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          ↑(ρ (inner ℝ a x + c)) •
            OperatorRidgelet.coefficientFormulaVec
              (⇑ρ) G (a, c))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
      (fun a =>
        ∫ (c : ℝ),
          ↑(ρ (inner ℝ a x + c)) •
            OperatorRidgelet.coefficientFormulaVec
              (⇑ρ) G (a, c))
      ν

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(ii) for `Y`-valued
densities: the iterated integral `∫ [∫ ρ(⟨a,x⟩+c) γ_G(a,c) dc] ν_α(da)` converges absolutely.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_ii_b.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν) (hG₂ : MeasureTheory.MemLp G 2 ν)
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        ↑(ρ (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c) ∂ν =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) •
      OperatorRidgelet.spectralTarget ν G x

theorem OperatorRidgelet.Paper.thm_vector_valued_A_ii_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        ↑(ρ (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G (a, c) ∂ν =
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) •
      OperatorRidgelet.spectralTarget ν G
        x

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(ii) for `Y`-valued
densities: the spectral synthesis identity with the same constant `C^{(α)}_ρ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_ii_c.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν) (hG₂ : MeasureTheory.MemLp G 2 ν)
  (hγ :
    MeasureTheory.Integrable
      (OperatorRidgelet.coefficientFormulaVec (⇑ρ) G)
      (OperatorRidgelet.parameterMeasure ν))
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        ↑(ρ (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c) ∂ν =
    OperatorRidgelet.integralNetworkDensity (fun t => ↑(ρ t))
      (OperatorRidgelet.parameterMeasure ν)
      (OperatorRidgelet.coefficientFormulaVec (⇑ρ) G) x

theorem OperatorRidgelet.Paper.thm_vector_valued_A_ii_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (hγ :
    MeasureTheory.Integrable
      (OperatorRidgelet.coefficientFormulaVec
        (⇑ρ) G)
      (OperatorRidgelet.parameterMeasure
        ν))
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        ↑(ρ (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G (a, c) ∂ν =
    OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(ρ t))
      (OperatorRidgelet.parameterMeasure
        ν)
      (OperatorRidgelet.coefficientFormulaVec
        (⇑ρ) G)
      x

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(ii) for `Y`-valued
densities: if `γ_G ∈ L¹(λ_α; Y)`, the left side is the `Y`-valued integral network
`S_ρ[γ_G λ_α](x)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_a.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → Y)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  ∀ᵐ (a : H) ∂ν,
    MeasureTheory.Integrable
      (fun c =>
        ↑(b (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c))
      MeasureTheory.volume

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → Y)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  ∀ᵐ (a : H) ∂ν,
    MeasureTheory.Integrable
      (fun c =>
        ↑(b (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G (a, c))
      MeasureTheory.volume

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(iii) for
`Y`-valued densities regular along rays (with `‖·‖_Y` in place of the absolute value): the
inner integral converges absolutely for `ν_α`-almost every `a`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_b.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → Y)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  MeasureTheory.Integrable
    (fun a =>
      ∫ (c : ℝ),
        ↑(b (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c))
    ν

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → Y)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  MeasureTheory.Integrable
    (fun a =>
      ∫ (c : ℝ),
        ↑(b (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G (a, c))
    ν

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(iii) for
`Y`-valued densities regular along rays: the outer integral converges absolutely.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_c.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → Y)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        ↑(b (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec (⇑ρ) G (a, c) ∂ν =
    OperatorRidgelet.temperedAdmissibilityConst α β ρ •
      OperatorRidgelet.spectralTarget ν G x

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → Y)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        ↑(b (inner ℝ a x + c)) •
          OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G (a, c) ∂ν =
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ •
      OperatorRidgelet.spectralTarget ν G
        x

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:A`(iii) for
`Y`-valued densities regular along rays: the tempered spectral synthesis identity with the
same constant `C^{(α)}_{β,ρ}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_i_a.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(MeasureTheory.Lp Y 2 μ))
  (hf : f ∈ OperatorRidgelet.spectralCoreVec Y μ ν) :
  MeasureTheory.MemLp (OperatorRidgelet.ridgeletVec μ ⇑ρ ↑↑f) 2
    (OperatorRidgelet.parameterMeasure ν)

theorem OperatorRidgelet.Paper.thm_vector_valued_B_i_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(MeasureTheory.Lp Y 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCoreVec Y μ
        ν) :
  MeasureTheory.MemLp
    (OperatorRidgelet.ridgeletVec μ ⇑ρ
      ↑↑f)
    2
    (OperatorRidgelet.parameterMeasure ν)

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(i) for `Y`-valued
targets: `R_ρ f ∈ L²(λ_α; Y)` for `f ∈ 𝒟_α(Y)` and `α`-admissible `ρ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_i_b.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ₁ ρ₂ : SchwartzMap ℝ ℝ) (hρ₁ : OperatorRidgelet.IsAdmissible α ρ₁)
  (hρ₂ : OperatorRidgelet.IsAdmissible α ρ₂)
  (f g : ↥(MeasureTheory.Lp Y 2 μ))
  (hf : f ∈ OperatorRidgelet.spectralCoreVec Y μ ν)
  (hg : g ∈ OperatorRidgelet.spectralCoreVec Y μ ν) :
  ∫ (p : H × ℝ),
      inner ℂ (OperatorRidgelet.ridgeletVec μ (⇑ρ₂) (↑↑g) p)
        (OperatorRidgelet.ridgeletVec μ (⇑ρ₁) (↑↑f)
          p) ∂OperatorRidgelet.parameterMeasure ν =
    OperatorRidgelet.crossAdmissibilityConst α ⇑ρ₁ ⇑ρ₂ *
      OperatorRidgelet.spectralInnerVec μ ν ↑↑f ↑↑g

theorem OperatorRidgelet.Paper.thm_vector_valued_B_i_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ₁ ρ₂ : SchwartzMap ℝ ℝ)
  (hρ₁ :
    OperatorRidgelet.IsAdmissible α ρ₁)
  (hρ₂ :
    OperatorRidgelet.IsAdmissible α ρ₂)
  (f g : ↥(MeasureTheory.Lp Y 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCoreVec Y μ
        ν)
  (hg :
    g ∈
      OperatorRidgelet.spectralCoreVec Y μ
        ν) :
  ∫ (p : H × ℝ),
      inner ℂ
        (OperatorRidgelet.ridgeletVec μ
          (⇑ρ₂) (↑↑g) p)
        (OperatorRidgelet.ridgeletVec μ
          (⇑ρ₁) (↑↑f)
          p) ∂OperatorRidgelet.parameterMeasure
        ν =
    OperatorRidgelet.crossAdmissibilityConst
        α ⇑ρ₁ ⇑ρ₂ *
      OperatorRidgelet.spectralInnerVec μ
        ν ↑↑f ↑↑g

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(i) for `Y`-valued
targets: the Plancherel identity
`⟨R_{ρ₁} f, R_{ρ₂} g⟩_{L²(λ_α;Y)} = C^{(α)}_{ρ₁,ρ₂} ⟨f,g⟩_{𝓔_α(Y)}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_a.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  ∃! R,
    ∀ (f : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbedVec μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure ν]
        OperatorRidgelet.ridgeletVec μ ⇑ρ ↑↑↑f

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  ∃! R,
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCoreVec
            Y μ ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbedVec
                μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          ν]
        OperatorRidgelet.ridgeletVec μ ⇑ρ
          ↑↑↑f

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(ii) for
`Y`-valued targets: an `α`-admissible `ρ` determines a unique bounded extension
`R_ρ : 𝓔_α(Y) → L²(λ_α; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_b.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  ‖(OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ) G‖ ^ 2 =
    OperatorRidgelet.admissibilityConst α ⇑ρ * ‖G‖ ^ 2

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  ‖(OperatorRidgelet.ridgeletExtensionVec
            Y μ ν ⇑ρ)
          G‖ ^
      2 =
    OperatorRidgelet.admissibilityConst α
        ⇑ρ *
      ‖G‖ ^ 2

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(ii) for
`Y`-valued targets: `‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_α(Y)}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_c.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  IsClosed (Set.range ⇑(OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ))

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  IsClosed
    (Set.range
      ⇑(OperatorRidgelet.ridgeletExtensionVec
          Y μ ν ⇑ρ))

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(ii) for
`Y`-valued targets: the range of `R_ρ` is closed.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_d.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  (OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ) G =
    OperatorRidgelet.spectralCoefficientVec ν ⇑ρ ↑↑↑G

theorem OperatorRidgelet.Paper.thm_vector_valued_B_ii_d.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  (OperatorRidgelet.ridgeletExtensionVec Y
        μ ν ⇑ρ)
      G =
    OperatorRidgelet.spectralCoefficientVec
      ν ⇑ρ ↑↑↑G

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(ii) for
`Y`-valued targets: `R_ρ = W_ρ U_α`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_B_iii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : H → Y) (hf : MeasureTheory.Integrable f μ)
  (h :
    OperatorRidgelet.ridgeletVec μ (⇑ρ)
        f =ᵐ[OperatorRidgelet.parameterMeasure ν]
      0) :
  f =ᵐ[μ] 0

theorem OperatorRidgelet.Paper.thm_vector_valued_B_iii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : H → Y)
  (hf : MeasureTheory.Integrable f μ)
  (h :
    OperatorRidgelet.ridgeletVec μ (⇑ρ)
        f =ᵐ[OperatorRidgelet.parameterMeasure
        ν]
      0) :
  f =ᵐ[μ] 0

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:B`(iii) for
`Y`-valued targets: `R_ρ f = 0` `λ_α`-a.e. implies `f = 0` `μ_Q`-a.e. for `f ∈ L¹(μ_Q; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_i_a.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  OperatorRidgelet.frameOperatorVec μ ν f =
    (OperatorRidgelet.rieszMapVec Y μ ν) f

theorem OperatorRidgelet.Paper.thm_vector_valued_C_i_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  OperatorRidgelet.frameOperatorVec μ ν
      f =
    (OperatorRidgelet.rieszMapVec Y μ ν) f

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(i) for `Y`-valued
targets: the frame operator `T_α = U_α' U_α` equals the Riesz map `J_α` of `𝓔_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(i) for `Y`-valued
targets: the Riesz map of `𝓔_α(Y)` is an isometry.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(i) for `Y`-valued
targets: the Riesz map of `𝓔_α(Y)` is a bijection onto `𝓔_α(Y)'`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_i_d.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  OperatorRidgelet.synthesisVec μ ν (⇑ρ)
      ((OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ) f) =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) •
      OperatorRidgelet.frameOperatorVec μ ν f

theorem OperatorRidgelet.Paper.thm_vector_valued_C_i_d.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  OperatorRidgelet.synthesisVec μ ν (⇑ρ)
      ((OperatorRidgelet.ridgeletExtensionVec
          Y μ ν ⇑ρ)
        f) =
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) •
      OperatorRidgelet.frameOperatorVec μ
        ν f

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(i) for `Y`-valued
targets: the frame identity `S_ρ R_ρ f = C^{(α)}_ρ T_α f`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_ii_a.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  f =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
      OperatorRidgelet.rieszInvVec μ ν
        (OperatorRidgelet.synthesisVec μ ν (⇑ρ)
          ((OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ) f))

theorem OperatorRidgelet.Paper.thm_vector_valued_C_ii_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  f =
    ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ)⁻¹ •
      OperatorRidgelet.rieszInvVec μ ν
        (OperatorRidgelet.synthesisVec μ ν
          (⇑ρ)
          ((OperatorRidgelet.ridgeletExtensionVec
              Y μ ν ⇑ρ)
            f))

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(ii) for
`Y`-valued targets: `f = (C^{(α)}_ρ)⁻¹ T_α⁻¹ S_ρ R_ρ f`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_ii_b.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (g : OperatorRidgelet.SpectralAntiDualVec Y μ ν) :
  g =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesisVec μ ν (⇑ρ)
        ((OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ)
          (OperatorRidgelet.rieszInvVec μ ν g))

theorem OperatorRidgelet.Paper.thm_vector_valued_C_ii_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (g :
    OperatorRidgelet.SpectralAntiDualVec Y
      μ ν) :
  g =
    ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesisVec μ ν
        (⇑ρ)
        ((OperatorRidgelet.ridgeletExtensionVec
            Y μ ν ⇑ρ)
          (OperatorRidgelet.rieszInvVec μ
            ν g))

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(ii) for
`Y`-valued targets: `g = (C^{(α)}_ρ)⁻¹ S_ρ (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α(Y)'`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_a.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralCoreVec Y μ ν))
  (hG :
    MeasureTheory.Integrable (OperatorRidgelet.gaussFourierVec μ ↑↑↑f)
      ν)
  (g : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)) :
  (OperatorRidgelet.frameOperatorVec μ ν
        (OperatorRidgelet.spectralEmbedVec μ ν f))
      (OperatorRidgelet.spectralEmbedVec μ ν g) =
    ∫ (x : H),
      inner ℂ (↑↑↑g x)
        (OperatorRidgelet.spectralTarget ν
          (OperatorRidgelet.gaussFourierVec μ ↑↑↑f) x) ∂μ

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralCoreVec Y μ
        ν))
  (hG :
    MeasureTheory.Integrable
      (OperatorRidgelet.gaussFourierVec μ
        ↑↑↑f)
      ν)
  (g :
    ↥(OperatorRidgelet.spectralCoreVec Y μ
        ν)) :
  (OperatorRidgelet.frameOperatorVec μ ν
        (OperatorRidgelet.spectralEmbedVec
          μ ν f))
      (OperatorRidgelet.spectralEmbedVec μ
        ν g) =
    ∫ (x : H),
      inner ℂ (↑↑↑g x)
        (OperatorRidgelet.spectralTarget ν
          (OperatorRidgelet.gaussFourierVec
            μ ↑↑↑f)
          x) ∂μ

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iii) for
`Y`-valued targets: for `f ∈ 𝒟_α(Y)` with `𝒢_Q f ∈ L¹(ν_α; Y)`, `T_α f` is represented by
`g_{𝒢_Q f}`: `T_α f [g] = ∫ ⟨g_{𝒢_Q f}(x), g(x)⟩_Y μ_Q(dx)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_b.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  (OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ)
      (OperatorRidgelet.rieszInvVec μ ν
        (OperatorRidgelet.transposeEmbedVec μ ν ↑G)) =
    OperatorRidgelet.spectralCoefficientVec ν ⇑ρ ↑↑↑G

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  (OperatorRidgelet.ridgeletExtensionVec Y
        μ ν ⇑ρ)
      (OperatorRidgelet.rieszInvVec μ ν
        (OperatorRidgelet.transposeEmbedVec
          μ ν ↑G)) =
    OperatorRidgelet.spectralCoefficientVec
      ν ⇑ρ ↑↑↑G

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iii) for
`Y`-valued targets: `R_ρ T_α⁻¹ U_α' G = W_ρ G` for `G ∈ 𝒦_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_c.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    ∀ (g : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)),
      (OperatorRidgelet.transposeEmbedVec μ ν ↑G)
          (OperatorRidgelet.spectralEmbedVec μ ν g) =
        ∫ (x : H),
          inner ℂ (↑↑↑g x)
            (OperatorRidgelet.spectralTarget ν (↑↑↑G) x) ∂μ

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCoreVec
            Y μ ν)),
      (OperatorRidgelet.transposeEmbedVec
            μ ν ↑G)
          (OperatorRidgelet.spectralEmbedVec
            μ ν g) =
        ∫ (x : H),
          inner ℂ (↑↑↑g x)
            (OperatorRidgelet.spectralTarget
              ν (↑↑↑G) x) ∂μ

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iii) for
`Y`-valued targets: when `G ∈ 𝒦_α(Y) ∩ L¹(ν_α; Y)`, `U_α' G` is represented by `g_G`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_d.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  OperatorRidgelet.transposeEmbedVec μ ν ↑G =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesisVec μ ν (⇑ρ)
        (OperatorRidgelet.spectralCoefficientVec ν ⇑ρ ↑↑↑G)

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_d.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  OperatorRidgelet.transposeEmbedVec μ ν
      ↑G =
    ↑(OperatorRidgelet.admissibilityConst
            α ⇑ρ)⁻¹ •
      OperatorRidgelet.synthesisVec μ ν
        (⇑ρ)
        (OperatorRidgelet.spectralCoefficientVec
          ν ⇑ρ ↑↑↑G)

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iii) for
`Y`-valued targets: `U_α' G = (C^{(α)}_ρ)⁻¹ S_ρ W_ρ G` for `G ∈ 𝒦_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_e.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    MeasureTheory.Integrable
        (OperatorRidgelet.coefficientFormulaVec ⇑ρ ↑↑↑G)
        (OperatorRidgelet.parameterMeasure ν) →
      ∀ (g : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)),
        (OperatorRidgelet.transposeEmbedVec μ ν ↑G)
            (OperatorRidgelet.spectralEmbedVec μ ν g) =
          ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ *
            ∫ (x : H),
              inner ℂ (↑↑↑g x)
                (OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(ρ t))
                  (OperatorRidgelet.parameterMeasure ν)
                  (OperatorRidgelet.coefficientFormulaVec ⇑ρ ↑↑↑G) x) ∂μ

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iii_e.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  MeasureTheory.Integrable (↑↑↑G) ν →
    MeasureTheory.Integrable
        (OperatorRidgelet.coefficientFormulaVec
          ⇑ρ ↑↑↑G)
        (OperatorRidgelet.parameterMeasure
          ν) →
      ∀
        (g :
          ↥(OperatorRidgelet.spectralCoreVec
              Y μ ν)),
        (OperatorRidgelet.transposeEmbedVec
              μ ν ↑G)
            (OperatorRidgelet.spectralEmbedVec
              μ ν g) =
          ↑(OperatorRidgelet.admissibilityConst
                  α ⇑ρ)⁻¹ *
            ∫ (x : H),
              inner ℂ (↑↑↑g x)
                (OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(ρ t))
                  (OperatorRidgelet.parameterMeasure
                    ν)
                  (OperatorRidgelet.coefficientFormulaVec
                    ⇑ρ ↑↑↑G)
                  x) ∂μ

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iii) for
`Y`-valued targets: when `G ∈ 𝒦_α(Y) ∩ L¹(ν_α; Y)` and `γ_G ∈ L¹(λ_α; Y)`, the second
reconstruction formula for `U_α' G` is the spectral synthesis identity paired with
`g ∈ 𝒟_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iv) for
`Y`-valued targets: the backprojection `Λ_ρ` is a bounded operator
`L²(λ_α; Y) → L²(ν_α; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_b.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (F : H → Y) :
  MeasureTheory.StronglyMeasurable F →
    MeasureTheory.MemLp F 2 ν →
      OperatorRidgelet.backprojectionVec α ν ⇑ρ
          ↑↑(OperatorRidgelet.spectralCoefficientVec ν (⇑ρ) F) =ᵐ[ν]
        fun ξ => ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) • F ξ

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (F : H → Y) :
  MeasureTheory.StronglyMeasurable F →
    MeasureTheory.MemLp F 2 ν →
      OperatorRidgelet.backprojectionVec α
          ν ⇑ρ
          ↑↑(OperatorRidgelet.spectralCoefficientVec
                ν (⇑ρ) F) =ᵐ[ν]
        fun ξ =>
        ↑(OperatorRidgelet.admissibilityConst
              α ⇑ρ) •
          F ξ

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iv) for
`Y`-valued targets: `Λ_ρ W_ρ = C^{(α)}_ρ Id` on `L²(ν_α; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_c.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralCoreVec Y μ ν)) (ξ : H) :
  OperatorRidgelet.backprojectionOfVec α (⇑ρ)
      (OperatorRidgelet.biasFourierVec
        (OperatorRidgelet.ridgeletVec μ ⇑ρ ↑↑↑f))
      ξ =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) •
      OperatorRidgelet.gaussFourierVec μ (↑↑↑f) ξ

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralCoreVec Y μ
        ν))
  (ξ : H) :
  OperatorRidgelet.backprojectionOfVec α
      (⇑ρ)
      (OperatorRidgelet.biasFourierVec
        (OperatorRidgelet.ridgeletVec μ ⇑ρ
          ↑↑↑f))
      ξ =
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) •
      OperatorRidgelet.gaussFourierVec μ
        (↑↑↑f) ξ

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iv) for
`Y`-valued targets: `Λ_ρ R_ρ f = C^{(α)}_ρ 𝒢_Q f` pointwise for `f ∈ 𝒟_α(Y)`, with `Λ_ρ`
computed from the Fourier-slice representative of `R_ρ f`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_d.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : 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.spectralCoreVec Y μ ν)) (ξ : H) :
  ξ ≠ 0 →
    ∀ (n : ℕ),
      OperatorRidgelet.hermiteCoefficientVec μ Q (↑↑↑f) ξ n =
        (Complex.I ^ n / ↑√(inner ℝ (Q ξ) ξ) ^ n) •
          iteratedDeriv n
            (fun t =>
              OperatorRidgelet.hermiteExtensionVec μ Q (↑↑↑f) ξ ↑t)
            0

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_d.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : 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.spectralCoreVec Y μ
        ν))
  (ξ : H) :
  ξ ≠ 0 →
    ∀ (n : ℕ),
      OperatorRidgelet.hermiteCoefficientVec
          μ Q (↑↑↑f) ξ n =
        (Complex.I ^ n /
            ↑√(inner ℝ (Q ξ) ξ) ^ n) •
          iteratedDeriv n
            (fun t =>
              OperatorRidgelet.hermiteExtensionVec
                μ Q (↑↑↑f) ξ ↑t)
            0

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iv) for
`Y`-valued targets: the Hermite inversion formula, applied componentwise, for `f ∈ 𝒟_α(Y)` and
`ξ ≠ 0`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_e.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : 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.spectralCoreVec Y μ ν)) :
  (∀ (ξ : H),
      ξ ≠ 0 →
        ∀ (n : ℕ),
          OperatorRidgelet.hermiteCoefficientVec μ Q (↑↑↑f) ξ n =
            OperatorRidgelet.hermiteCoefficientVec μ Q (↑↑↑g) ξ n) →
    f = g

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_e.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : 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.spectralCoreVec Y μ
        ν)) :
  (∀ (ξ : H),
      ξ ≠ 0 →
        ∀ (n : ℕ),
          OperatorRidgelet.hermiteCoefficientVec
              μ Q (↑↑↑f) ξ n =
            OperatorRidgelet.hermiteCoefficientVec
              μ Q (↑↑↑g) ξ n) →
    f = g

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iv) for
`Y`-valued targets: the Hermite coefficients over all `ξ ≠ 0` and `n` determine
`f ∈ 𝒟_α(Y)` in `L²(μ_Q; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_f.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (μ ν : 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.spectralCoreVec Y μ ν)) :
  (OperatorRidgelet.gaussFourierInvVec μ ν fun ξ =>
      ↑(OperatorRidgelet.admissibilityConst α ⇑ρ)⁻¹ •
        OperatorRidgelet.backprojectionOfVec α (⇑ρ)
          (OperatorRidgelet.biasFourierVec
            (OperatorRidgelet.ridgeletVec μ ⇑ρ ↑↑↑f))
          ξ) =
    ↑f

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_f.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : 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.spectralCoreVec Y μ
        ν)) :
  (OperatorRidgelet.gaussFourierInvVec μ ν
      fun ξ =>
      ↑(OperatorRidgelet.admissibilityConst
              α ⇑ρ)⁻¹ •
        OperatorRidgelet.backprojectionOfVec
          α (⇑ρ)
          (OperatorRidgelet.biasFourierVec
            (OperatorRidgelet.ridgeletVec
              μ ⇑ρ ↑↑↑f))
          ξ) =
    ↑f

**Theorem [thm:vector-valued]** Vector-valued extension.  Theorem `thm:C`(iv) for
`Y`-valued targets: `f = Δ_Q[(C^{(α)}_ρ)⁻¹ Λ_ρ R_ρ f]` for `f ∈ 𝒟_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_e.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → Y)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  MeasureTheory.Integrable
    (fun θ =>
      ↑(b (inner ℝ θ.1 x + θ.2)) •
        OperatorRidgelet.coefficientFormulaVec (⇑ρ) G θ)
    (OperatorRidgelet.parameterMeasure ν)

theorem OperatorRidgelet.Paper.thm_vector_valued_A_iii_e.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → Y)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  MeasureTheory.Integrable
    (fun θ =>
      ↑(b (inner ℝ θ.1 x + θ.2)) •
        OperatorRidgelet.coefficientFormulaVec
          (⇑ρ) G θ)
    (OperatorRidgelet.parameterMeasure ν)

**Theorem [thm:vector-valued]** Tempered synthesis is Bochner integrable on the product.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_completion.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  [SecondCountableTopology Y] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRangeVec Y μ ν)) :
  OperatorRidgelet.backprojectionVec α ν ⇑ρ
      ↑↑((OperatorRidgelet.ridgeletExtensionVec Y μ ν ⇑ρ) f) =ᵐ[ν]
    fun ξ => ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) • ↑↑↑f ξ

theorem OperatorRidgelet.Paper.thm_vector_valued_C_iv_completion.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRangeVec Y
        μ ν)) :
  OperatorRidgelet.backprojectionVec α ν
      ⇑ρ
      ↑↑((OperatorRidgelet.ridgeletExtensionVec
              Y μ ν ⇑ρ)
            f) =ᵐ[ν]
    fun ξ =>
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) •
      ↑↑↑f ξ

**Theorem [thm:vector-valued]** The completed vector spectral density is recovered in L².

Proof for Theorem 3.3.2

uses 0

Use Lemma 2.2.7 for jointly measurable Fourier representatives and Hilbert-valued Plancherel, Lemma 3.1.1 for spectral synthesis and uniqueness, and Lemma 3.1.3 for coefficient moments and joint absolute integrability. The vector adjoint identity and ray formula are Lemma 2.2.8. These common lemmas justify the Fubini and Parseval steps with the same constants. Completing the vector core and applying Riesz representation proves the frame and reconstruction statements; the Gaussian Hermite expansion is applied componentwise. If Y\ne\{0\}, a nonzero constant vector belongs to the Gaussian core by Lemma 2.3.3, so its Riesz isometries have norm one; when Y=\{0\}, both spaces and norms are zero. Tempered synthesis uses the fixed-support C^m Bochner argument and the distributional pairing tensored with the identity of Y.