3.2. Filters, the ridgelet transform, and the Fourier slice🔗

DefinitionAux.4

uses 0

Used by 16

Reverse dependency previews

Preview

Lemma 3.2

Loading preview

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

✓L∃∀N

These are the Fourier and bias conventions fixed in the preliminaries and used throughout Section 3.

The Fourier convention is h^\sharp(\omega)=\int_{\mathbb R}h(t)e^{-it\omega}\,\mathrm dt for functions on the line (for a real filter \rho this is \rho^\sharp), and the partial Fourier transform in the bias of a coefficient is \gamma^\sharp(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. The Lean network uses \langle a,x\rangle+c; the manuscript bias is b=-c, so a coefficient written in b has its bias Fourier transform reflected in \omega relative to the coefficient written in c.

Lean code for DefinitionAux.4●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♯(ω) = ∫ 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_ω)_# ν = |ω|^{-α} ν`.

Definition3.3

uses 1

Used by 11

Reverse dependency previews

Preview

Definition 3.7

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}|\rho^\sharp(\omega)|^2|\omega|^{-\alpha}\,\mathrm d\omega<\infty. It is a band-pass filter if moreover \rho^\sharp\in C_c^\infty(\mathbb R\setminus\{0\}) (and \rho\ne0): band-pass here specifies compact Fourier support away from zero. Such a filter is \alpha-admissible for every \alpha>0. For two admissible filters, (\!(\rho_1,\rho_2)\!)_\alpha=\frac1{2\pi}\int_{\mathbb R}\rho_1^\sharp(\omega)\overline{\rho_2^\sharp(\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 Definition3.3●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_3_3 (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (α : ℝ) :
  0 < α → OperatorRidgelet.IsAdmissible α ρ

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

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

Definition3.4

Statement uses 3

Statement dependency previews

Preview

Definition Aux.2

Loading preview

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

Used by 8

Reverse dependency previews

Preview

Lemma 3.5

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, F_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 F_\mu f.

Lean code for Definition3.4●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 (ξ) = ∫ f(x) exp(-i⟪x,ξ⟫) dμ(x)`, the Fourier
transform of the finite complex measure `f μ`; for `μ = μ_Q` this is the manuscript's `F_Q`.

Lemma3.5

Statement uses 2

Statement dependency previews

Preview

Definition Aux.4

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Theorem 3.14

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, (R_\rho f)^\sharp(a,\omega)=\rho^\sharp(\omega)\,F_\mu f(-\omega a) (v).

Lean code for Lemma3.5●5 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_5_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_3_5_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:3.5]** Fourier-slice identity.  `R_ρ f` is bounded on `H × ℝ`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_5_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_3_5_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:3.5]** Fourier-slice identity.  `R_ρ f` is jointly continuous on
`H × ℝ`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_3_5_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_3_5_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:3.5]** 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_3_5_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_3_5_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:3.5]** 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_3_5_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_3_5_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:3.5]** Fourier-slice identity.  The partial Fourier transform in the
bias is `(R_ρ f)^\sharp(a,ω) = ρ♯(ω) F_μ f(-ωa)`.

Proof for Lemma 3.5

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. For nonzero a, the function \omega\mapsto F_\mu f(\omega a) is the restriction of F_\mu f to the line through the origin spanned by a.