Appendix B. Coefficient projections and minimum-norm solutions🔗

The coefficient adjoint and reconstruction theorem have already been proved in the main text. This appendix derives further range, orthogonal projection, and minimum-norm coefficient formulas from them.

PropositionB.1

Statement uses 3

Statement dependency previews

Preview

Lemma 3.9

Loading preview

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

used by 0✓L∃∀N

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

Lean code for PropositionB.1●9 declarations

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

**Proposition [prop:B.1]** Bounded backprojection and orthogonal range
projection.  `W_ρ^* W_ρ = C Id`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

Proof for Proposition B.1

Proof uses 3

Proof dependency previews

Preview

Lemma 3.2

Loading preview

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

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

Remark B.2 (Range of the analysis operator).

The closed range is R_\rho\mathcal E_\alpha=W_\rho\mathcal K_\alpha, which is contained in the closed space W_\rho L^2(\nu_\alpha). Their orthogonal projections are respectively C^{-1}W_\rho P_{\mathcal K_\alpha}W_\rho^* and C^{-1}W_\rho W_\rho^*. Retaining the closed spectral subspace distinguishes coefficients obtained by analysis from arbitrary synthesis coefficients. The preceding result also identifies the minimum-norm coefficient and the kernel of synthesis.