2.2. Admissible filters, the transform, and the Fourier slice🔗

Definition2.2.1

uses 0

Used by 18

Reverse dependency previews

Preview

Lemma 2.1.4

Loading preview

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

✓L∃∀N

The Fourier convention is \widehat h(\omega)=\int_{\mathbb R}h(t)e^{-it\omega}\,\mathrm dt for functions on the line (for a real filter \rho this is \widehat\rho), and the partial Fourier transform in the bias of a coefficient is \widehat\gamma(a,\omega)=\int_{\mathbb R}\gamma(a,c)e^{-i\omega c}\,\mathrm dc; the analysis character on H is x\mapsto e^{-i\langle x,\xi\rangle}. A measure \nu on H is homogeneous of degree \alpha when (D_\omega)_\#\nu=|\omega|^{-\alpha}\nu for every \omega\ne0.

Lean code for Definition2.2.1●5 definitions

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.character.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (ξ x : H) : ℂ

def OperatorRidgelet.character.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (ξ x : H) : ℂ

The character `x ↦ exp(-i⟪x,ξ⟫)` used by the analysis map.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.lineFourier (h : ℝ → ℂ) (ω : ℝ) : ℂ

def OperatorRidgelet.lineFourier (h : ℝ → ℂ)
  (ω : ℝ) : ℂ

The one-dimensional Fourier transform of a complex function in the convention of the
manuscript, `ĥ(ω) = ∫ h(t) exp(-itω) dt`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.filterFourier (ρ : ℝ → ℝ) (ω : ℝ) : ℂ

def OperatorRidgelet.filterFourier (ρ : ℝ → ℝ)
  (ω : ℝ) : ℂ

The Fourier transform `ρ̂(ω) = ∫ ρ(t) exp(-itω) dt` of a real filter.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.biasFourier.{u_1} {H : Type u_1} (γ : H × ℝ → ℂ)
  (a : H) (ω : ℝ) : ℂ

def OperatorRidgelet.biasFourier.{u_1}
  {H : Type u_1} (γ : H × ℝ → ℂ) (a : H)
  (ω : ℝ) : ℂ

The partial Fourier transform in the bias variable,
`γ̂(a,ω) = ∫ γ(a,c) exp(-iωc) dc`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.IsHomogeneous.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (α : ℝ) (ν : MeasureTheory.Measure H) : Prop

def OperatorRidgelet.IsHomogeneous.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (α : ℝ)
  (ν : MeasureTheory.Measure H) : Prop

A measure on `H` is homogeneous of degree `α` when every dilation `D_ω a = ω a`, `ω ≠ 0`,
scales it by `|ω|^(-α)`: `(D_ω)_# ν = |ω|^{-α} ν`.

Definition2.2.2

uses 1

Used by 12

Reverse dependency previews

Preview

Definition 2.2.5

Loading preview

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

✓L∃∀N

A real \rho\in\mathcal S(\mathbb R) is \alpha-admissible if 0<(\!(\rho,\rho)\!)_\alpha=\frac1{2\pi}\int_{\mathbb R}|\widehat\rho(\omega)|^2|\omega|^{-\alpha}\,\mathrm d\omega<\infty. It is a band-pass filter if moreover \widehat\rho\in C_c^\infty(\mathbb R\setminus\{0\}) (and \rho\ne0), in which case it is \alpha-admissible for every \alpha>0. For two admissible filters, (\!(\rho_1,\rho_2)\!)_\alpha=\frac1{2\pi}\int_{\mathbb R}\widehat\rho_1(\omega)\overline{\widehat\rho_2(\omega)}|\omega|^{-\alpha}\,\mathrm d\omega; self-admissibility is the case \rho_1=\rho_2=\rho of this pairing, since \rho is real.

Lean code for Definition2.2.2●5 declarations

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

complete

structure OperatorRidgelet.IsAdmissible (α : ℝ) (ρ : SchwartzMap ℝ ℝ) : Prop

structure OperatorRidgelet.IsAdmissible (α : ℝ)
  (ρ : SchwartzMap ℝ ℝ) : Prop

A real Schwartz function `ρ` is `α`-admissible if `0 < C^{(α)}_ρ < ∞`; finiteness is the
integrability of `|ρ̂(ω)|² |ω|^{-α}`.

Fields

integrable : MeasureTheory.Integrable (fun ω => ‖OperatorRidgelet.filterFourier (⇑ρ) ω‖ ^ 2 * |ω| ^ (-α)) MeasureTheory.volume

`C^{(α)}_ρ < ∞`.

pos : 0 < OperatorRidgelet.admissibilityConst α ⇑ρ

`0 < C^{(α)}_ρ`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.admissibilityConst (α : ℝ) (ρ : ℝ → ℝ) : ℝ

def OperatorRidgelet.admissibilityConst
  (α : ℝ) (ρ : ℝ → ℝ) : ℝ

The admissibility constant `C^{(α)}_ρ = (2π)⁻¹ ∫ |ρ̂(ω)|² |ω|^{-α} dω`.

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

complete

structure OperatorRidgelet.IsBandPass (ρ : SchwartzMap ℝ ℝ) : Prop

structure OperatorRidgelet.IsBandPass
  (ρ : SchwartzMap ℝ ℝ) : Prop

A band-pass filter: a nonzero real Schwartz function whose Fourier transform lies in
`C_c^∞(ℝ ∖ {0})`.  (An analysis filter is admissible, hence nonzero; the nonvanishing is part
of the notion so that band-pass filters are `α`-admissible for every `α > 0`.)

Fields

ne_zero : ρ ≠ 0

`ρ ≠ 0`.

contDiff : ContDiff ℝ (↑⊤) (OperatorRidgelet.filterFourier ⇑ρ)

`ρ̂` is smooth.

hasCompactSupport : HasCompactSupport (OperatorRidgelet.filterFourier ⇑ρ)

`ρ̂` has compact support.

zero_notMem_tsupport : 0 ∉ tsupport (OperatorRidgelet.filterFourier ⇑ρ)

The support of `ρ̂` stays away from the origin.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.crossAdmissibilityConst (α : ℝ) (ρ₁ ρ₂ : ℝ → ℝ) : ℂ

def OperatorRidgelet.crossAdmissibilityConst
  (α : ℝ) (ρ₁ ρ₂ : ℝ → ℝ) : ℂ

The cross admissibility constant
`C^{(α)}_{ρ₁,ρ₂} = (2π)⁻¹ ∫ ρ̂₁(ω) conj(ρ̂₂(ω)) |ω|^{-α} dω`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.def_admissible_filter (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (α : ℝ) :
  0 < α → OperatorRidgelet.IsAdmissible α ρ

theorem OperatorRidgelet.Paper.def_admissible_filter
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (α : ℝ) :
  0 < α →
    OperatorRidgelet.IsAdmissible α ρ

**Definition [def:admissible-filter]** Admissible analysis filter.  A band-pass filter is
`α`-admissible for every `α > 0`.

Definition2.2.3

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

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

Used by 9

Reverse dependency previews

Preview

Lemma 2.2.4

Loading preview

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

✓L∃∀N

For f\in L^1(H,\mu_Q) and \rho\in\mathcal S(\mathbb R), the Gaussian-weighted ridgelet transform is R_\rho f(a,c)=\int_Hf(x)\rho(\langle a,x\rangle+c)\,\mu_Q(\mathrm dx), and \lambda_\alpha=\nu_\alpha\otimes\mathrm dc is the parameter measure on H\times\mathbb R. The analogue of the Fourier transform of f is the Fourier transform of the finite measure f\mu_Q, \mathcal G_Qf(\xi)=\int_Hf(x)e^{-i\langle x,\xi\rangle}\,\mu_Q(\mathrm dx), which is bounded and continuous; for a general input measure \mu it is written \mathcal G_\mu f.

Lean code for Definition2.2.3●3 definitions

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

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

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

The weighted ridgelet transform `R_ρ f (a,c) = ∫ f(x) ρ(⟪a,x⟫ + c) dμ(x)`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.parameterMeasure.{u_1} {H : Type u_1}
  [MeasurableSpace H] (ν : MeasureTheory.Measure H) :
  MeasureTheory.Measure (H × ℝ)

def OperatorRidgelet.parameterMeasure.{u_1}
  {H : Type u_1} [MeasurableSpace H]
  (ν : MeasureTheory.Measure H) :
  MeasureTheory.Measure (H × ℝ)

The parameter measure `λ = ν ⊗ dc` on `H × ℝ`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

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

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

The weighted Fourier transform `𝒢_μ f (ξ) = ∫ f(x) exp(-i⟪x,ξ⟫) dμ(x)`, the Fourier
transform of the finite complex measure `f μ`; for `μ = μ_Q` this is the manuscript's `𝒢_Q`.

Lemma2.2.4

Statement uses 2

Statement dependency previews

Preview

Definition 2.2.1

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Theorem 2.4.1

Loading preview

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

✓L∃∀N

Let f\in L^1(H,\mu) and \rho\in\mathcal S(\mathbb R). Then R_\rho f is bounded (i) and jointly continuous (ii) on H\times\mathbb R, and for every a, \|R_\rho f(a,\cdot)\|_{L^1(\mathbb R)}\le\|f\|_{L^1(\mu)}\|\rho\|_{L^1} (iii) and \|R_\rho f(a,\cdot)\|_{L^2(\mathbb R)}^2\le\|f\|_{L^2(\mu)}^2\|\rho\|_{L^2}^2 if f\in L^2(\mu) (iv). For every a\in H and \omega\in\mathbb R, \widehat{R_\rho f}(a,\omega)=\widehat\rho(\omega)\,\mathcal G_\mu f(-\omega a) (v).

Lean code for Lemma2.2.4●5 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_fourier_slice_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ) :
  ∃ M, ∀ (p : H × ℝ), ‖OperatorRidgelet.ridgelet μ (⇑ρ) f p‖ ≤ M

theorem OperatorRidgelet.Paper.lem_fourier_slice_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ) :
  ∃ M,
    ∀ (p : H × ℝ),
      ‖OperatorRidgelet.ridgelet μ (⇑ρ) f
            p‖ ≤
        M

**Lemma [lem:fourier-slice]** Fourier-slice identity.  `R_ρ f` is bounded on `H × ℝ`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_fourier_slice_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ) :
  Continuous (OperatorRidgelet.ridgelet μ (⇑ρ) f)

theorem OperatorRidgelet.Paper.lem_fourier_slice_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ) :
  Continuous
    (OperatorRidgelet.ridgelet μ (⇑ρ) f)

**Lemma [lem:fourier-slice]** Fourier-slice identity.  `R_ρ f` is jointly continuous on
`H × ℝ`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_fourier_slice_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ) (hf : MeasureTheory.Integrable f μ)
  (a : H) :
  MeasureTheory.Integrable
      (fun c => OperatorRidgelet.ridgelet μ (⇑ρ) f (a, c))
      MeasureTheory.volume ∧
    ∫ (c : ℝ), ‖OperatorRidgelet.ridgelet μ (⇑ρ) f (a, c)‖ ≤
      (∫ (x : H), ‖f x‖ ∂μ) * ∫ (t : ℝ), ‖ρ t‖

theorem OperatorRidgelet.Paper.lem_fourier_slice_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (a : H) :
  MeasureTheory.Integrable
      (fun c =>
        OperatorRidgelet.ridgelet μ (⇑ρ) f
          (a, c))
      MeasureTheory.volume ∧
    ∫ (c : ℝ),
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            f (a, c)‖ ≤
      (∫ (x : H), ‖f x‖ ∂μ) *
        ∫ (t : ℝ), ‖ρ t‖

**Lemma [lem:fourier-slice]** Fourier-slice identity.  For every direction `a`, the bias
function `R_ρ f (a, ·)` is integrable with `‖R_ρ f(a,·)‖_{L¹} ≤ ‖f‖_{L¹(μ)} ‖ρ‖_{L¹}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_fourier_slice_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ) (hf : MeasureTheory.Integrable f μ)
  (hf₂ : MeasureTheory.MemLp f 2 μ) (a : H) :
  MeasureTheory.MemLp
      (fun c => OperatorRidgelet.ridgelet μ (⇑ρ) f (a, c)) 2
      MeasureTheory.volume ∧
    ∫ (c : ℝ), ‖OperatorRidgelet.ridgelet μ (⇑ρ) f (a, c)‖ ^ 2 ≤
      (∫ (x : H), ‖f x‖ ^ 2 ∂μ) * ∫ (t : ℝ), ‖ρ t‖ ^ 2

theorem OperatorRidgelet.Paper.lem_fourier_slice_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (hf₂ : MeasureTheory.MemLp f 2 μ)
  (a : H) :
  MeasureTheory.MemLp
      (fun c =>
        OperatorRidgelet.ridgelet μ (⇑ρ) f
          (a, c))
      2 MeasureTheory.volume ∧
    ∫ (c : ℝ),
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
              f (a, c)‖ ^
          2 ≤
      (∫ (x : H), ‖f x‖ ^ 2 ∂μ) *
        ∫ (t : ℝ), ‖ρ t‖ ^ 2

**Lemma [lem:fourier-slice]** Fourier-slice identity.  If moreover `f ∈ L²(μ)`, then for every
direction `a` the bias function is square integrable with
`‖R_ρ f(a,·)‖²_{L²} ≤ ‖f‖²_{L²(μ)} ‖ρ‖²_{L²}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_fourier_slice_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ) (hf : MeasureTheory.Integrable f μ)
  (a : H) (ω : ℝ) :
  OperatorRidgelet.biasFourier (OperatorRidgelet.ridgelet μ (⇑ρ) f) a
      ω =
    OperatorRidgelet.filterFourier (⇑ρ) ω *
      OperatorRidgelet.gaussFourier μ f (-(ω • a))

theorem OperatorRidgelet.Paper.lem_fourier_slice_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ρ : SchwartzMap ℝ ℝ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (a : H) (ω : ℝ) :
  OperatorRidgelet.biasFourier
      (OperatorRidgelet.ridgelet μ (⇑ρ) f)
      a ω =
    OperatorRidgelet.filterFourier (⇑ρ)
        ω *
      OperatorRidgelet.gaussFourier μ f
        (-(ω • a))

**Lemma [lem:fourier-slice]** Fourier-slice identity.  The partial Fourier transform in the
bias is `\widehat{R_ρ f}(a,ω) = ρ̂(ω) 𝒢_μ f(-ωa)`.

Proof for Lemma 2.2.4

uses 0

Boundedness is |R_\rho f|\le\|f\|_1\|\rho\|_\infty, joint continuity is dominated convergence, the bounds are Cauchy–Schwarz and Tonelli in the probability measure \mu, and the substitution u=\langle a,x\rangle+c in the inner Fourier transform gives the slice identity.

Definition2.2.5

Statement uses 3

Statement dependency previews

Preview

Definition 2.2.1

Loading preview

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

Used by 6

Reverse dependency previews

Preview

Lemma 2.2.6

Loading preview

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

✓L∃∀N

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 \widehat{W_\rho G}(a,\omega)=\widehat\rho(\omega)\,G(-\omega a), 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}\widehat\rho(\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 Definition2.2.5●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 ray 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 ray average
`backprojectionOf` computed from it would be meaningless.  With the clause all representatives
of `γ` agree almost everywhere on almost every ray, so that `backprojection` does not depend on
the choice (Proposition `prop:coefficient-projection`(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_spectral_coefficient.{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_spectral_coefficient.{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:spectral-coefficient]** 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.

Lemma2.2.6

Statement uses 2

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

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

Used by 7

Reverse dependency previews

Preview

Lemma 2.2.8

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 ray for every bias. In this notation the Fourier-slice identity reads R_\rho f=W_\rho\,\mathcal G_Qf.

Lean code for Lemma2.2.6●6 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_isometry_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_coefficient_isometry_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:coefficient-isometry]** 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_coefficient_isometry_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_coefficient_isometry_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:coefficient-isometry]** 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_coefficient_isometry_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_coefficient_isometry_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:coefficient-isometry]** The coefficient operator is a scaled isometry.
`‖W_ρ G‖²_{L²(λ)} = C^{(α)}_ρ ‖G‖²_{L²(ν)}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_isometry_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_coefficient_isometry_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:coefficient-isometry]** 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_spectral_coefficient.{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_spectral_coefficient.{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:spectral-coefficient]** 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_coefficient_isometry_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_coefficient_isometry_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:coefficient-isometry]** The L² inverse formula is absolutely integrable
on almost every ray, for every bias value.

Proof for Lemma 2.2.6

uses 0

(a,\omega)\mapsto G(-\omega a) is Borel, and the homogeneous change of variables with Tonelli gives \frac1{2\pi}\int\int|\widehat\rho(\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.

Lemma2.2.7

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 2.2.8

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 on almost every ray. Such representatives agree almost everywhere.

Lean code for Lemma2.2.7●2 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_partial_fourier_l2.{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_partial_fourier_l2.{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:partial-fourier-l2]** 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_partial_fourier_l2_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_partial_fourier_l2_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:partial-fourier-l2]** The Fourier representatives agree on almost every section.

Proof for Lemma 2.2.7

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.

Lemma2.2.8

Statement uses 2

Statement dependency previews

Preview

Lemma 2.2.6

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Definition 3.2.2

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 is \Lambda_\rho=W_\rho^*. It satisfies \Lambda_\rho W_\rho=(\!(\rho,\rho)\!)_\alpha\mathrm{Id} and \|\Lambda_\rho\gamma\|_2\le\sqrt{(\!(\rho,\rho)\!)_\alpha}\|\gamma\|_2. Its ray formula is \Lambda_\rho\gamma(\xi)=(2\pi)^{-1}\int\overline{\widehat\rho(\omega)}\widehat\gamma(-\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 Lemma2.2.8●3 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_adjoint_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_coefficient_adjoint_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:coefficient-adjoint]** 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_coefficient_adjoint_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_coefficient_adjoint_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:coefficient-adjoint]** The ray-average integral is absolutely convergent a.e.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_adjoint_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_coefficient_adjoint_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:coefficient-adjoint]** Every measurable Fourier representative gives Λ.

Proof for Lemma 2.2.8

uses 0

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