4.4. Vector-valued targets🔗

DefinitionAux.7

Statement uses 6

Statement dependency previews

Preview

Definition 3.4

Loading preview

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

used by 1✓L∃∀N

These are the vector-valued objects introduced for Theorem 4.11 in Section 4.3.

Let Y be a separable complex Hilbert space. All objects above have Y-valued versions: L^2(\mu_Q;Y), the Bochner integral F_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 F_Qf,F_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 the condition in Definition 4.2 are already polymorphic in the target.

Lean code for DefinitionAux.7●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_μ 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 `a`, the 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_μ f, 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_μ 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_μ 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 (F_μ 𝒟(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 `F_Q : 𝒟(Y) → 𝒦(Y)`, `f ↦ 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 `F_Q(𝒟(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 `T : 𝓔(Y) → 𝓔(Y)'`, `T 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 `T⁻¹ : 𝓔(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 `F_Q' : L²(ν; Y) → 𝓔(Y)'`, `F_Q' F [g] = ⟨F, F_Q 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 = F_Q' F_Q : 𝓔(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 `Φ`:
`W_ρ^* Φ (ξ) = (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 `W_ρ^* γ`, 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 `W_ρ^* γ` 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)} W_ρ^*`.

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_μ f(zξ)` of the `Y`-valued weighted Fourier transform along
the line through `ξ` and the origin.

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_μ 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 `F_μ` on its range on `𝒟(Y)`.

Theorem4.11

Statement uses 4

Statement dependency previews

Preview

Theorem 3.14

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 6.8

Loading preview

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

✓L∃∀N

Theorem 4.5, Theorem 3.14, and Theorem 4.8 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, with general input and homogeneous direction measures where appropriate; the scalar existence claim of Theorem 4.5 (iii) is not repeated.

Lean code for Theorem4.11●35 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(i) for `Y`-valued
densities: `‖g_G(x)‖_Y ≤ ‖G‖_{L¹(ν_α;Y)}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(i) for `Y`-valued
densities: `g_G` is continuous.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(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_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(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_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(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_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(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_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(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_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(iii) for
`Y`-valued densities regular along rays: the outer integral converges absolutely.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_representation_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_4_11_representation_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:4.11]** Vector-valued extension.  Theorem `thm:4.5`(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_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(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_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(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_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(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_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(ii) for
`Y`-valued targets: `‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_α(Y)}`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(ii) for
`Y`-valued targets: the range of `R_ρ` is closed.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(ii) for
`Y`-valued targets: `R_ρ = W_ρ F_Q`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_plancherel_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_4_11_plancherel_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:4.11]** Vector-valued extension.  Theorem `thm:3.14`(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_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(i) for `Y`-valued
targets: the frame operator `T_α = F_Q' F_Q` is the Riesz map of `𝓔_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(i) for `Y`-valued
targets: the Riesz map of `𝓔_α(Y)` is an isometry.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(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_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(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_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(ii) for
`Y`-valued targets: `f = (C^{(α)}_ρ)⁻¹ T_α⁻¹ S_ρ R_ρ f`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(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_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iii) for
`Y`-valued targets: for `f ∈ 𝒟_α(Y)` with `F_Q f ∈ L¹(ν_α; Y)`, `T_α f` is represented by
`g_{F_Q f}`: `T_α f [g] = ∫ ⟨g_{F_Q f}(x), g(x)⟩_Y μ_Q(dx)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iii) for
`Y`-valued targets: `R_ρ T_α⁻¹ F_Q' G = W_ρ G` for `G ∈ 𝒦_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iii) for
`Y`-valued targets: when `G ∈ 𝒦_α(Y) ∩ L¹(ν_α; Y)`, `F_Q' G` is represented by `g_G`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iii) for
`Y`-valued targets: `F_Q' G = (C^{(α)}_ρ)⁻¹ S_ρ W_ρ G` for `G ∈ 𝒦_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iii) for
`Y`-valued targets: when `G ∈ 𝒦_α(Y) ∩ L¹(ν_α; Y)` and `γ_G ∈ L¹(λ_α; Y)`, the second
reconstruction formula for `F_Q' G` is the spectral synthesis identity paired with
`g ∈ 𝒟_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iv) for
`Y`-valued targets: the backprojection `W_ρ^*` is a bounded operator
`L²(λ_α; Y) → L²(ν_α; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iv) for
`Y`-valued targets: `W_ρ^* W_ρ = C^{(α)}_ρ Id` on `L²(ν_α; Y)`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iv) for
`Y`-valued targets: `W_ρ^* R_ρ f = C^{(α)}_ρ F_Q f` pointwise for `f ∈ 𝒟_α(Y)`, with `W_ρ^*`
computed from the Fourier-slice representative of `R_ρ f`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(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_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(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_4_11_frame_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_4_11_frame_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:4.11]** Vector-valued extension.  Theorem `thm:4.8`(iv) for
`Y`-valued targets: `f = Δ_Q[(C^{(α)}_ρ)⁻¹ W_ρ^* R_ρ f]` for `f ∈ 𝒟_α(Y)`.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_representation_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_4_11_representation_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:4.11]** The network integrand is Bochner integrable on the product.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_4_11_frame_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_4_11_frame_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:4.11]** The completed vector spectral density is recovered in L².

Proof for Theorem 4.11

Proof uses 4

Proof dependency previews

Preview

Lemma 3.6

Loading preview

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

Use Lemma 3.6 for jointly measurable Fourier representatives and Hilbert-valued Plancherel, Lemma 4.1 for spectral synthesis and uniqueness, and Lemma 4.3 for coefficient moments and joint absolute integrability. The vector adjoint identity and integral formula are Lemma 3.9. 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 3.12, so its Riesz isometries have norm one; when Y=\{0\}, both spaces and norms are zero. The integral representation with a continuous activation of polynomial growth uses the fixed-support C^m Bochner argument and the distributional pairing tensored with the identity of Y.