4.3. Synthesis, Hermite recovery, and reconstruction🔗

DefinitionAux.6

Statement uses 2

Statement dependency previews

Preview

Definition 3.10

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Lemma 4.6

Loading preview

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

✓L∃∀N

These are the anti-dual, transpose, and frame-operator definitions preceding Theorem 4.8 in Section 4.2.

Let \mathcal E_\alpha' be the continuous anti-dual of \mathcal E_\alpha, represented as the continuous conjugate-linear functionals on \mathcal K_\alpha. The Riesz map is T_\alpha f[g]=\langle f,g\rangle_{\mathcal E_\alpha}, with inverse T_\alpha^{-1} from the Riesz representation theorem; the transpose of F_Q is F_Q'F[g]=\langle F,F_Q g\rangle_{L^2(\nu_\alpha)} for F\in L^2(\nu_\alpha), and the frame operator is T_\alpha=F_Q'F_Q. With R_\rho:\mathcal E_\alpha\to L^2(\lambda_\alpha) the bounded extension of Theorem 3.14 (ii) and \operatorname{Ran}R_\rho its range, synthesis with the analysis filter is the transpose S_\rho=R_\rho', (S_\rho\gamma)[g]=\langle\gamma,R_\rho g\rangle_{L^2(\lambda_\alpha)}. Here F_Q':L^2(\nu_\alpha)\to\mathcal E_\alpha' is formed from the completed input space. The prime denotes transpose into the anti-dual, while the star denotes the Hilbert adjoint. No adjoint into the ambient L^2(\mu_Q) is asserted. With C=(\!(\rho,\rho)\!)_\alpha, the Plancherel identity gives R_\rho^*R_\rho=C I_{\mathcal E_\alpha} and R_\rho'R_\rho=CT_\alpha.

Lean code for DefinitionAux.6●9 definitions

abbrevdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

Lemma4.6

Statement uses 4

Statement dependency previews

Preview

Definition 2.2

Loading preview

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

used by 1✓L∃∀N

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

Lean code for Lemma4.6●2 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

Proof for Lemma 4.6

uses 0

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

Lemma4.7

Statement uses 3

Statement dependency previews

Preview

Definition Aux.2

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 4.8

Loading preview

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

✓L∃∀N

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

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

Lean code for Lemma4.7●10 declarations

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

The analytic continuation `z ↦ F_μ f(zξ) = ∫ f(x) e^{-iz⟪x,ξ⟫} μ(dx)` of the weighted Fourier
transform on the line through `ξ` and the origin to complex `z`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

Proof for Lemma 4.7

uses 0

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

Theorem4.8

Statement uses 4

Statement dependency previews

Preview

Lemma 3.9

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Corollary 4.9

Loading preview

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

✓L∃∀N

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

Lean code for Theorem4.8●18 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

**Theorem [thm:4.8]** Reconstruction and the frame operator.  The frame operator
`T_α = F_Q' F_Q` is the Riesz map.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

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

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

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

Proof for Theorem 4.8

Proof uses 6

Proof dependency previews

Preview

Lemma 3.2

Loading preview

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

Since F_Q is unitary onto \mathcal K_\alpha, F_Q'F_Q f[g]=\langle F_Q f,F_Q g\rangle=\langle f,g\rangle_{\mathcal E_\alpha}, the Riesz representation theorem makes T_\alpha an isometric bijection, and the Plancherel identity gives (S_\rho R_\rho f)[g]=\langle R_\rho f,R_\rho g\rangle=(\!(\rho,\rho)\!)_\alpha T_\alpha f[g]; (ii) follows by applying T_\alpha^{-1} or substituting f=T_\alpha^{-1}g. For (iii), |G(\xi)||v(x)| is integrable against \nu_\alpha\otimes\mu_Q when G\in L^1(\nu_\alpha) and v\in\mathcal D_\alpha, so Fubini identifies F_Q'G with the functional represented by g_G. For u=T_\alpha^{-1}F_Q'G, unitarity gives F_Q u=G, hence R_\rho u=W_\rho G. When also \gamma_G\in L^1(\lambda_\alpha), Lemma 4.6 identifies weak synthesis with the ordinary network integral. Part (iv) first uses W_\rho^* W_\rho=(\!(\rho,\rho)\!)_\alpha\mathrm{Id} from Lemma 3.9 and R_\rho=W_\rho F_Q on the completion. The pointwise core formula uses the continuous Fourier-slice representative; only the final Hermite inversion invokes Lemma 4.7 and Gaussian input.

Corollary4.9

uses 1used by 0✓L∃∀N

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

Lean code for Corollary4.9●4 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

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

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

**Corollary [cor:4.9]** The decoder is C⁻¹ T⁻¹ S.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

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

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

**Corollary [cor:4.9]** The bounded decoder is a left inverse.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

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

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

**Corollary [cor:4.9]** Coefficient error δ gives spectral error δ/√C.

Proof for Corollary 4.9

Proof uses 2

Proof dependency previews

Preview

Lemma 3.8

Loading preview

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

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

Remark 4.10 (Which inverse is bounded).

The inverse T_\alpha^{-1}:\mathcal E_\alpha'\to\mathcal E_\alpha is bounded with norm one. This is the Hilbert-space norm of the construction; no bounded inverse in the ambient L^2(\mu_Q) norm is asserted. On the core, inversion factors through F_Qf, Fourier uniqueness of f\mu_Q, and the Radon–Nikodym derivative. The Hermite expansion makes the last two steps constructive.