3.3. Partial Fourier transformation and the coefficient operator🔗

We first construct the partial bias transform on the product L^2 space. The coefficient formula, its isometry, and the adjoint then follow in sequence.

Lemma3.6

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 3.9

Loading preview

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

✓L∃∀N

For a separable complex Hilbert space Y, partial Fourier transformation in the bias is a unitary map from L^2(\nu\otimes\mathrm dc;Y) onto L^2(\nu\otimes\mathrm d\omega/(2\pi);Y). Each transform admits a jointly strongly measurable representative agreeing with the one-dimensional Plancherel transform of c\mapsto\gamma(a,c) for almost every a. Such representatives agree almost everywhere.

Lean code for Lemma3.6●2 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_3_6.{u_1, u_2} {H : Type u_1}
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν] :
  ∃ U,
    ∀
      (γ :
        ↥(MeasureTheory.Lp Y 2 (OperatorRidgelet.parameterMeasure ν))),
      ∃ Φ,
        MeasureTheory.StronglyMeasurable (Function.uncurry Φ) ∧
          OperatorRidgelet.HasBiasFourierVec ν (↑↑γ) Φ ∧
            Function.uncurry
                Φ =ᵐ[ν.prod
                (ENNReal.ofReal (2 * Real.pi)⁻¹ • MeasureTheory.volume)]
              ↑↑(U γ)

theorem OperatorRidgelet.Paper.lem_3_6.{u_1, u_2}
  {H : Type u_1} [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] :
  ∃ U,
    ∀
      (γ :
        ↥(MeasureTheory.Lp Y 2
            (OperatorRidgelet.parameterMeasure
              ν))),
      ∃ Φ,
        MeasureTheory.StronglyMeasurable
            (Function.uncurry Φ) ∧
          OperatorRidgelet.HasBiasFourierVec
              ν (↑↑γ) Φ ∧
            Function.uncurry
                Φ =ᵐ[ν.prod
                (ENNReal.ofReal
                    (2 * Real.pi)⁻¹ •
                  MeasureTheory.volume)]
              ↑↑(U γ)

**Lemma [lem:3.6]** Bias Fourier transformation is a genuine unitary
with jointly measurable representatives and the angular normalization.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_3_6_uniqueness.{u_1, u_2} {H : Type u_1}
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  (γ : H × ℝ → Y) (Φ Φ' : H → ℝ → Y)
  (hΦ : OperatorRidgelet.HasBiasFourierVec ν γ Φ)
  (hΦ' : OperatorRidgelet.HasBiasFourierVec ν γ Φ') :
  ∀ᵐ (a : H) ∂ν, Φ a =ᵐ[MeasureTheory.volume] Φ' a

theorem OperatorRidgelet.Paper.lem_3_6_uniqueness.{u_1,
    u_2}
  {H : Type u_1} [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (γ : H × ℝ → Y) (Φ Φ' : H → ℝ → Y)
  (hΦ :
    OperatorRidgelet.HasBiasFourierVec ν γ
      Φ)
  (hΦ' :
    OperatorRidgelet.HasBiasFourierVec ν γ
      Φ') :
  ∀ᵐ (a : H) ∂ν,
    Φ a =ᵐ[MeasureTheory.volume] Φ' a

**Lemma [lem:3.6]** The Fourier representatives agree on almost every section.

Proof for Lemma 3.6

uses 0

Apply the one-dimensional Fourier unitary to the fibers of the product L^2 space. Its inverse on the fibers proves surjectivity; the product L^2 identification supplies joint measurability. Fiberwise uniqueness and Fubini prove independence of the representative.

Definition3.7

Statement uses 3

Statement dependency previews

Preview

Definition Aux.4

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Lemma 3.8

Loading preview

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

✓L∃∀N

For a function g on H, write g_a(\omega):=g(\omega a), \omega\in\mathbb R. For a\ne0 this is the restriction of g to the line through the origin spanned by a; for a=0 it is constant. We write G_a when the density is denoted by G. Let \rho be \alpha-admissible and G\in L^2(\nu_\alpha) Borel. The coefficient W_\rho G\in L^2(\lambda_\alpha) is the function whose partial Fourier transform in the bias is (W_\rho G)^\sharp(a,\omega)=\rho^\sharp(\omega)\,G_a(-\omega), characterized through Parseval's identity against Schwartz test functions in the bias. For every such G\in L^2(\nu_\alpha) and \nu_\alpha-almost every a, \gamma_G(a,c)=W_\rho G(a,c)=\frac1{2\pi}\int_{\mathbb R}\rho^\sharp(\omega)G(-\omega a)e^{i\omega c}\,\mathrm d\omega; the integral converges absolutely for every c. This formula is the theorem part of the definition.

Lean code for Definition3.7●4 declarations

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

complete

structure OperatorRidgelet.HasBiasFourier.{u_1} {H : Type u_1} [MeasurableSpace H]
  (ν : MeasureTheory.Measure H) (γ : H × ℝ → ℂ) (Φ : H → ℝ → ℂ) : Prop

structure OperatorRidgelet.HasBiasFourier.{u_1}
  {H : Type u_1} [MeasurableSpace H]
  (ν : MeasureTheory.Measure H)
  (γ : H × ℝ → ℂ) (Φ : H → ℝ → ℂ) : Prop

`HasBiasFourier ν γ Φ` says that the partial Fourier transform of `γ` in the bias is `Φ`:
for `ν`-almost every direction `a`, the function `ω ↦ Φ(a,ω)` is square integrable and
Parseval's identity `∫ γ(a,c) conj(φ(c)) dc = (2π)⁻¹ ∫ Φ(a,ω) conj(φ♯(ω)) dω` holds for every
Schwartz test function `φ` on `ℝ`.  This characterizes `Φ(a,·)` up to a null set as the `L²`
Fourier transform of `γ(a,·)` (`HasBiasFourier.ae_ae_eq`), and for `γ ∈ L²(λ)` such a
representative exists and can be chosen jointly measurable
(`exists_measurable_hasBiasFourier`).

The square-integrability clause is essential.  Parseval's identity alone says nothing about
`Φ(a,·)` where the integrand `Φ(a,ω) conj(φ♯(ω))` fails to be integrable, since Lean's Bochner
integral of a non-integrable function is `0`: without the clause an arbitrary non-integrable
function would be a "representative" of every coefficient, and the backprojection integral
`backprojectionOf` computed from it would be meaningless.  With the clause all representatives
of `γ` agree almost everywhere for almost every direction, so `backprojection` is independent
of the choice (Proposition `prop:B.1`(ii)).

Fields

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

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

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

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

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.coefficientFormula.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ → ℝ) (G : H → ℂ)
  (p : H × ℝ) : ℂ

def OperatorRidgelet.coefficientFormula.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (ρ : ℝ → ℝ)
  (G : H → ℂ) (p : H × ℝ) : ℂ

The explicit coefficient
`γ_G(a,c) = (2π)⁻¹ ∫ ρ♯(ω) G(-ωa) exp(iωc) dω` of a spectral density `G`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.def_3_7.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {α : ℝ}
  (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ↑↑(OperatorRidgelet.spectralCoefficient ν (⇑ρ)
          G) =ᵐ[OperatorRidgelet.parameterMeasure ν]
    OperatorRidgelet.coefficientFormula (⇑ρ) G

theorem OperatorRidgelet.Paper.def_3_7.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ↑↑(OperatorRidgelet.spectralCoefficient
          ν (⇑ρ)
          G) =ᵐ[OperatorRidgelet.parameterMeasure
      ν]
    OperatorRidgelet.coefficientFormula
      (⇑ρ) G

**Definition [def:3.7]** The coefficient operator.  For
`G ∈ L²(ν)` the coefficient `W_ρ G` is given by the explicit formula
`γ_G(a,c) = (2π)⁻¹ ∫ ρ♯(ω) G(-ωa) e^{iωc} dω`, `λ`-almost everywhere.

Lemma3.8

uses 1

Used by 6

Reverse dependency previews

Preview

Lemma 3.9

Loading preview

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

✓L∃∀N

W_\rho:L^2(\nu_\alpha)\to L^2(\lambda_\alpha) is well defined (i), independent of the Borel representative of G (ii), and \|W_\rho G\|_{L^2(\lambda_\alpha)}^2=(\!(\rho,\rho)\!)_\alpha\|G\|_{L^2(\nu_\alpha)}^2 (iii). If G\in L^1(\nu_\alpha), then \omega\mapsto G(-\omega a) is integrable on compact subsets of \mathbb R\setminus\{0\} for \nu_\alpha-almost every a (iv), and the explicit formula for \gamma_G holds already for G\in L^2(\nu_\alpha), with absolute convergence on almost every a and every bias. In this notation the Fourier-slice identity reads R_\rho f=W_\rho\,F_Qf.

Lean code for Lemma3.8●6 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_8_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {α : ℝ}
  (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ∃! γ,
    OperatorRidgelet.HasBiasFourier ν ↑↑γ fun a ω =>
      OperatorRidgelet.filterFourier (⇑ρ) ω * G (-(ω • a))

theorem OperatorRidgelet.Paper.lem_3_8_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ∃! γ,
    OperatorRidgelet.HasBiasFourier ν ↑↑γ
      fun a ω =>
      OperatorRidgelet.filterFourier (⇑ρ)
          ω *
        G (-(ω • a))

**Lemma [lem:3.8]** The coefficient operator is a scaled isometry.  `W_ρ G`
is well defined: there is exactly one element of `L²(λ)` whose partial Fourier transform in the
bias is `ρ♯(ω) G(-ωa)`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_8_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {α : ℝ}
  (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G G' : H → ℂ)
  (hG : Measurable G) (hG' : Measurable G')
  (hG₂ : MeasureTheory.MemLp G 2 ν) (hGG' : G =ᵐ[ν] G') :
  OperatorRidgelet.spectralCoefficient ν (⇑ρ) G =
    OperatorRidgelet.spectralCoefficient ν (⇑ρ) G'

theorem OperatorRidgelet.Paper.lem_3_8_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G G' : H → ℂ) (hG : Measurable G)
  (hG' : Measurable G')
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (hGG' : G =ᵐ[ν] G') :
  OperatorRidgelet.spectralCoefficient ν
      (⇑ρ) G =
    OperatorRidgelet.spectralCoefficient ν
      (⇑ρ) G'

**Lemma [lem:3.8]** The coefficient operator is a scaled isometry.  `W_ρ G`
does not depend on the Borel representative of `G`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_8_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {α : ℝ}
  (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ∫ (p : H × ℝ),
      ‖↑↑(OperatorRidgelet.spectralCoefficient ν (⇑ρ) G) p‖ ^
        2 ∂OperatorRidgelet.parameterMeasure ν =
    OperatorRidgelet.admissibilityConst α ⇑ρ * ∫ (ξ : H), ‖G ξ‖ ^ 2 ∂ν

theorem OperatorRidgelet.Paper.lem_3_8_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ∫ (p : H × ℝ),
      ‖↑↑(OperatorRidgelet.spectralCoefficient
                  ν (⇑ρ) G)
            p‖ ^
        2 ∂OperatorRidgelet.parameterMeasure
        ν =
    OperatorRidgelet.admissibilityConst α
        ⇑ρ *
      ∫ (ξ : H), ‖G ξ‖ ^ 2 ∂ν

**Lemma [lem:3.8]** The coefficient operator is a scaled isometry.
`‖W_ρ G‖²_{L²(λ)} = C^{(α)}_ρ ‖G‖²_{L²(ν)}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_8_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {α : ℝ}
  (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₁ : MeasureTheory.Integrable G ν) :
  ∀ᵐ (a : H) ∂ν,
    ∀ (I : Set ℝ),
      IsCompact I →
        0 ∉ I →
          MeasureTheory.IntegrableOn (fun ω => G (-(ω • a))) I
            MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_3_8_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν) :
  ∀ᵐ (a : H) ∂ν,
    ∀ (I : Set ℝ),
      IsCompact I →
        0 ∉ I →
          MeasureTheory.IntegrableOn
            (fun ω => G (-(ω • a))) I
            MeasureTheory.volume

**Lemma [lem:3.8]** The coefficient operator is a scaled isometry.  If
`G ∈ L¹(ν)`, then `ω ↦ G(-ωa)` is integrable on compact subsets of `ℝ ∖ {0}` for `ν`-almost
every `a`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.def_3_7.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {α : ℝ}
  (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ↑↑(OperatorRidgelet.spectralCoefficient ν (⇑ρ)
          G) =ᵐ[OperatorRidgelet.parameterMeasure ν]
    OperatorRidgelet.coefficientFormula (⇑ρ) G

theorem OperatorRidgelet.Paper.def_3_7.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ↑↑(OperatorRidgelet.spectralCoefficient
          ν (⇑ρ)
          G) =ᵐ[OperatorRidgelet.parameterMeasure
      ν]
    OperatorRidgelet.coefficientFormula
      (⇑ρ) G

**Definition [def:3.7]** The coefficient operator.  For
`G ∈ L²(ν)` the coefficient `W_ρ G` is given by the explicit formula
`γ_G(a,c) = (2π)⁻¹ ∫ ρ♯(ω) G(-ωa) e^{iωc} dω`, `λ`-almost everywhere.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_3_8_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {α : ℝ} (hα : 0 < α) (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ∀ᵐ (a : H) ∂ν,
    ∀ (c : ℝ),
      MeasureTheory.Integrable
        (fun ω =>
          OperatorRidgelet.filterFourier (⇑ρ) ω * G (-(ω • a)) *
            Complex.exp (↑(ω * c) * Complex.I))
        MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_3_8_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {α : ℝ} (hα : 0 < α)
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₂ : MeasureTheory.MemLp G 2 ν) :
  ∀ᵐ (a : H) ∂ν,
    ∀ (c : ℝ),
      MeasureTheory.Integrable
        (fun ω =>
          OperatorRidgelet.filterFourier
                (⇑ρ) ω *
              G (-(ω • a)) *
            Complex.exp
              (↑(ω * c) * Complex.I))
        MeasureTheory.volume

**Lemma [lem:3.8]** The L² inverse formula is absolutely integrable
for almost every direction, for every bias value.

Proof for Lemma 3.8

uses 1

(a,\omega)\mapsto G(-\omega a) is Borel, and the homogeneous change of variables with Tonelli gives \frac1{2\pi}\int\int|\rho^\sharp(\omega)|^2|G(-\omega a)|^2\,\nu_\alpha(\mathrm da)\,\mathrm d\omega=(\!(\rho,\rho)\!)_\alpha\|G\|^2_{L^2(\nu_\alpha)}; the same computation with |G| on a compact set gives local integrability, and the inverse Fourier transform in \omega for almost every a gives the formula.

Lemma3.9

Statement uses 2

Statement dependency previews

Preview

Lemma 3.6

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Theorem 4.8

Loading preview

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

✓L∃∀N

For an admissible Schwartz filter and a sigma-finite homogeneous direction measure, the backprojection W_\rho^* is the Hilbert adjoint of the coefficient operator, with values in the frequency space L^2(\nu_\alpha). It satisfies W_\rho^* W_\rho=(\!(\rho,\rho)\!)_\alpha\mathrm{Id} and \|W_\rho^*\gamma\|_2\le\sqrt{(\!(\rho,\rho)\!)_\alpha}\|\gamma\|_2. Its integral formula is W_\rho^*\gamma(\xi)=(2\pi)^{-1}\int_{\mathbb R\setminus\{0\}} \overline{\rho^\sharp(\omega)}\gamma^\sharp(-\xi/\omega,\omega)|\omega|^{-\alpha}\,\mathrm d\omega; this integral is absolutely convergent for almost every \xi and is independent of the jointly measurable Fourier representative.

Lean code for Lemma3.9●6 declarations

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_3_9_i.{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.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  ∃ W,
    (∀ (F : ↥(MeasureTheory.Lp Y 2 ν)),
        W F = OperatorRidgelet.spectralCoefficientVec ν ⇑ρ ↑↑F) ∧
      (∀
          (γ :
            ↥(MeasureTheory.Lp Y 2
                (OperatorRidgelet.parameterMeasure ν))),
          (ContinuousLinearMap.adjoint W) γ =
            OperatorRidgelet.backprojectionLpVec α ν ⇑ρ ↑↑γ) ∧
        ‖W‖ ≤ √(OperatorRidgelet.admissibilityConst α ⇑ρ) ∧
          (∀
              (γ :
                ↥(MeasureTheory.Lp Y 2
                    (OperatorRidgelet.parameterMeasure ν))),
              ‖OperatorRidgelet.backprojectionLpVec α ν ⇑ρ ↑↑γ‖ ≤
                √(OperatorRidgelet.admissibilityConst α ⇑ρ) * ‖γ‖) ∧
            ∀ (F : ↥(MeasureTheory.Lp Y 2 ν)),
              (ContinuousLinearMap.adjoint W) (W F) =
                ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) • F

theorem OperatorRidgelet.Paper.lem_3_9_i.{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.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  ∃ W,
    (∀ (F : ↥(MeasureTheory.Lp Y 2 ν)),
        W F =
          OperatorRidgelet.spectralCoefficientVec
            ν ⇑ρ ↑↑F) ∧
      (∀
          (γ :
            ↥(MeasureTheory.Lp Y 2
                (OperatorRidgelet.parameterMeasure
                  ν))),
          (ContinuousLinearMap.adjoint W)
              γ =
            OperatorRidgelet.backprojectionLpVec
              α ν ⇑ρ ↑↑γ) ∧
        ‖W‖ ≤
            √(OperatorRidgelet.admissibilityConst
                α ⇑ρ) ∧
          (∀
              (γ :
                ↥(MeasureTheory.Lp Y 2
                    (OperatorRidgelet.parameterMeasure
                      ν))),
              ‖OperatorRidgelet.backprojectionLpVec
                    α ν ⇑ρ ↑↑γ‖ ≤
                √(OperatorRidgelet.admissibilityConst
                      α ⇑ρ) *
                  ‖γ‖) ∧
            ∀
              (F :
                ↥(MeasureTheory.Lp Y 2
                    ν)),
              (ContinuousLinearMap.adjoint
                    W)
                  (W F) =
                ↑(OperatorRidgelet.admissibilityConst
                      α ⇑ρ) •
                  F

**Lemma [lem:3.9]** The coefficient operator has the bounded ray-average
adjoint and the scaled left-inverse identity.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_3_9_ii.{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.SigmaFinite ν] {α : ℝ}
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ : ↥(MeasureTheory.Lp Y 2 (OperatorRidgelet.parameterMeasure ν)))
  (Φ : H → ℝ → Y)
  (hΦ : MeasureTheory.StronglyMeasurable (Function.uncurry Φ))
  (hB : OperatorRidgelet.HasBiasFourierVec ν (↑↑γ) Φ) :
  ∀ᵐ (ξ : H) ∂ν,
    MeasureTheory.Integrable
      (fun ω =>
        ((starRingEnd ℂ) (OperatorRidgelet.filterFourier (⇑ρ) ω) *
            ↑(|ω| ^ (-α))) •
          Φ (-(ω⁻¹ • ξ)) ω)
      MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_3_9_ii.{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.SigmaFinite ν] {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (γ :
    ↥(MeasureTheory.Lp Y 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (Φ : H → ℝ → Y)
  (hΦ :
    MeasureTheory.StronglyMeasurable
      (Function.uncurry Φ))
  (hB :
    OperatorRidgelet.HasBiasFourierVec ν
      (↑↑γ) Φ) :
  ∀ᵐ (ξ : H) ∂ν,
    MeasureTheory.Integrable
      (fun ω =>
        ((starRingEnd ℂ)
              (OperatorRidgelet.filterFourier
                (⇑ρ) ω) *
            ↑(|ω| ^ (-α))) •
          Φ (-(ω⁻¹ • ξ)) ω)
      MeasureTheory.volume

**Lemma [lem:3.9]** The backprojection integral is absolutely convergent a.e.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_3_9_iii.{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.SigmaFinite ν] {α : ℝ}
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (γ : ↥(MeasureTheory.Lp Y 2 (OperatorRidgelet.parameterMeasure ν)))
  (Φ : H → ℝ → Y)
  (hΦ : MeasureTheory.StronglyMeasurable (Function.uncurry Φ))
  (hB : OperatorRidgelet.HasBiasFourierVec ν (↑↑γ) Φ) :
  OperatorRidgelet.backprojectionVec α ν ⇑ρ ↑↑γ =ᵐ[ν]
    OperatorRidgelet.backprojectionOfVec α (⇑ρ) Φ

theorem OperatorRidgelet.Paper.lem_3_9_iii.{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.SigmaFinite ν] {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (γ :
    ↥(MeasureTheory.Lp Y 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (Φ : H → ℝ → Y)
  (hΦ :
    MeasureTheory.StronglyMeasurable
      (Function.uncurry Φ))
  (hB :
    OperatorRidgelet.HasBiasFourierVec ν
      (↑↑γ) Φ) :
  OperatorRidgelet.backprojectionVec α ν
      ⇑ρ ↑↑γ =ᵐ[ν]
    OperatorRidgelet.backprojectionOfVec α
      (⇑ρ) Φ

**Lemma [lem:3.9]** Every measurable Fourier representative gives Λ.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

`HasBiasFourier` requires `ω ↦ Φ(a, ω)` to be square integrable for `ν`-almost every `a`.
It determines this frequency profile up to a null set (`HasBiasFourier.ae_ae_eq`). The
substitution `(a, ω) ↦ (-ωa, ω)` preserves null sets by homogeneity, so the backprojection
integral does not depend on the chosen representative as an element of `L²(ν)`
(`prop_B_1_ii`).  For `γ ∈ L²(λ)` a jointly measurable representative exists
(`exists_measurable_hasBiasFourier`), so the junk value is never taken on `L²(λ)`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

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

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

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

Proof for Lemma 3.9

Proof uses 2

Proof dependency previews

Preview

Lemma 3.6

Loading preview

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

Plancherel in the bias and the substitution \xi=-\omega a identify the inner product with the integral formula. Weighted Cauchy–Schwarz and Tonelli give its absolute convergence and norm bound; polarization of the coefficient isometry gives the left inverse identity.