Infinite-dimensional operator ridgelet transform

4.2. Integral representation🔗

DefinitionAux.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 5
Reverse dependency previews
Preview
Theorem 4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

This is the activation and distributional-pairing setup for Theorem 4.5(iii).

A tempered distribution \beta\in\mathcal S'(\mathbb R) that is a continuous function of polynomial growth is the pair of \beta and a continuous b:\mathbb R\to\mathbb R with |b(t)|\le C(1+|t|)^p and \langle\beta,\varphi\rangle=\int b\varphi. For a band-pass \rho the test filter \omega\mapsto\rho^\sharp(-\omega)|\omega|^{-\alpha} is a Schwartz function, and the distributional admissibility constant is C_{\beta,\rho}^{(\alpha)}=\frac1{2\pi}\langle\beta^\sharp,\rho^\sharp(-\,\cdot\,)|\cdot|^{-\alpha}\rangle.

Lean code for DefinitionAux.5●3 definitions
  • structure(3 fields)defined in OperatorRidgelet/Reconstruction/Defs.lean
    complete
    structure OperatorRidgelet.IsTemperedFunction (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ) : Prop
    structure OperatorRidgelet.IsTemperedFunction
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ) : Prop
    `β ∈ 𝒮'(ℝ)` is the continuous function `b` of polynomial growth: `b` is continuous,
`|b(t)| ≤ C (1+|t|)^p`, and `β` acts on test functions by integration against `b`.

    Fields

    continuous : Continuous b
    `b` is continuous. 
    polynomialGrowth : OperatorRidgelet.HasPolynomialGrowth b
    `b` has polynomial growth. 
    apply_eq : ∀ (φ : SchwartzMap ℝ ℂ), β φ = ∫ (t : ℝ), ↑(b t) * φ t
    `β` is integration against `b`.
  • defdefined in OperatorRidgelet/Tempered/Const.lean
    complete
    def OperatorRidgelet.temperedTestFilter (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  SchwartzMap ℝ ℂ
    def OperatorRidgelet.temperedTestFilter
  (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  SchwartzMap ℝ ℂ
    The test filter `ω ↦ ρ♯(-ω) |ω|^{-α}` as a Schwartz function, when one with these values
exists (in particular when `ρ` is band-pass); `0` otherwise.
  • defdefined in OperatorRidgelet/Tempered/Const.lean
    complete
    def OperatorRidgelet.temperedAdmissibilityConst (α : ℝ)
  (β : TemperedDistribution ℝ ℂ) (ρ : SchwartzMap ℝ ℝ) : ℂ
    def OperatorRidgelet.temperedAdmissibilityConst
  (α : ℝ) (β : TemperedDistribution ℝ ℂ)
  (ρ : SchwartzMap ℝ ℝ) : ℂ
    The distributional admissibility constant
`C^{(α)}_{β,ρ} = (2π)⁻¹ ⟨β♯, ρ♯(-·) |·|^{-α}⟩` of a tempered activation `β` and a filter `ρ`.
Theorem4.5
Statement uses 4
Statement dependency previews
Preview
Definition 2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Theorem 4.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let \alpha>0. Part (ii) assumes an \alpha-admissible Schwartz filter \rho; part (iii) assumes a band-pass filter. (i) For G\in L^1(\nu_\alpha), the function g_G is bounded with \|g_G\|_\infty\le\|G\|_{L^1(\nu_\alpha)} and continuous, and g_G=0 only if G=0 \nu_\alpha-almost everywhere. (ii) For G\in L^1(\nu_\alpha)\cap L^2(\nu_\alpha) and every x, the iterated integral \int_H[\int_{\mathbb R}\gamma_G(a,c)\rho(\langle a,x\rangle+c)\,\mathrm dc]\,\nu_\alpha(\mathrm da)=(\!(\rho,\rho)\!)_\alpha g_G(x) converges absolutely, and if \gamma_G\in L^1(\lambda_\alpha) its left side is the integral network S_\rho[\gamma_G\lambda_\alpha](x). (iii) For a tempered \beta that is a continuous function of polynomial growth and G satisfying Definition 4.2, the integrand \gamma_G(a,c)\beta(\langle a,x\rangle+c) is absolutely integrable on the product space. Its integral is the ordinary network with finite coefficient measure \gamma_G\lambda_\alpha and equals C_{\beta,\rho}^{(\alpha)}g_G(x). This identity allows a zero constant. Non-polynomiality is needed separately to choose a band-pass filter with a nonzero constant, then normalize it for reconstruction or universality. A polynomial activation has zero band-pass pairing.

Lean code for Theorem4.5●11 theorems
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_i_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (ν : MeasureTheory.Measure H) (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν) (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G x‖ ≤ ∫ (ξ : H), ‖G ξ‖ ∂ν
    theorem OperatorRidgelet.Paper.thm_4_5_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (ν : MeasureTheory.Measure H)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G
        x‖ ≤
    ∫ (ξ : H), ‖G ξ‖ ∂ν
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For
`G ∈ L¹(ν_α)` the target `g_G` is bounded by `‖G‖_{L¹(ν_α)}`.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_i_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν) :
  Continuous (OperatorRidgelet.spectralTarget ν G)
    theorem OperatorRidgelet.Paper.thm_4_5_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν) :
  Continuous
    (OperatorRidgelet.spectralTarget ν G)
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For
`G ∈ L¹(ν_α)` the target `g_G` is continuous.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_i_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (h : OperatorRidgelet.spectralTarget ν G = 0) : G =ᵐ[ν] 0
    theorem OperatorRidgelet.Paper.thm_4_5_i_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (h :
    OperatorRidgelet.spectralTarget ν G =
      0) :
  G =ᵐ[ν] 0
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For
`G ∈ L¹(ν_α)`, `g_G = 0` only if `G = 0` `ν_α`-almost everywhere.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_ii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν) (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
            ↑(ρ (inner ℝ a x + c)))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
      (fun a =>
        ∫ (c : ℝ),
          OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
            ↑(ρ (inner ℝ a x + c)))
      ν
    theorem OperatorRidgelet.Paper.thm_4_5_ii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          OperatorRidgelet.coefficientFormula
              (⇑ρ) G (a, c) *
            ↑(ρ (inner ℝ a x + c)))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
      (fun a =>
        ∫ (c : ℝ),
          OperatorRidgelet.coefficientFormula
              (⇑ρ) G (a, c) *
            ↑(ρ (inner ℝ a x + c)))
      ν
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For
`G ∈ L¹(ν_α) ∩ L²(ν_α)` and every `x`, the iterated integral
`∫ [∫ γ_G(a,c) ρ(⟨a,x⟩+c) dc] ν_α(da)` converges absolutely: the inner integral converges
absolutely for `ν_α`-almost every `a`, and the outer integrand is `ν_α`-integrable.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_ii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν) (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
          ↑(ρ (inner ℝ a x + c)) ∂ν =
    ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) *
      OperatorRidgelet.spectralTarget ν G x
    theorem OperatorRidgelet.Paper.thm_4_5_ii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula
            (⇑ρ) G (a, c) *
          ↑(ρ (inner ℝ a x + c)) ∂ν =
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) *
      OperatorRidgelet.spectralTarget ν G
        x
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For
`G ∈ L¹(ν_α) ∩ L²(ν_α)` the spectral synthesis identity
`∫ [∫ γ_G(a,c) ρ(⟨a,x⟩+c) dc] ν_α(da) = C^{(α)}_ρ g_G(x)` holds for every `x`.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_ii_c.{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 α ρ) (G : H → ℂ)
  (hG : Measurable G) (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (hγ :
    MeasureTheory.Integrable
      (OperatorRidgelet.coefficientFormula (⇑ρ) G)
      (OperatorRidgelet.parameterMeasure ν))
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
          ↑(ρ (inner ℝ a x + c)) ∂ν =
    OperatorRidgelet.integralNetworkDensity (fun t => ↑(ρ t))
      (OperatorRidgelet.parameterMeasure ν)
      (OperatorRidgelet.coefficientFormula (⇑ρ) G) x
    theorem OperatorRidgelet.Paper.thm_4_5_ii_c.{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 α ρ)
  (G : H → ℂ) (hG : Measurable G)
  (hG₁ : MeasureTheory.Integrable G ν)
  (hG₂ : MeasureTheory.MemLp G 2 ν)
  (hγ :
    MeasureTheory.Integrable
      (OperatorRidgelet.coefficientFormula
        (⇑ρ) G)
      (OperatorRidgelet.parameterMeasure
        ν))
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula
            (⇑ρ) G (a, c) *
          ↑(ρ (inner ℝ a x + c)) ∂ν =
    OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(ρ t))
      (OperatorRidgelet.parameterMeasure
        ν)
      (OperatorRidgelet.coefficientFormula
        (⇑ρ) G)
      x
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  If moreover
`γ_G ∈ L¹(λ_α)`, the left side of the spectral synthesis identity is the integral network
`S_ρ[γ_G λ_α](x)`.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_iii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  ∀ᵐ (a : H) ∂ν,
    MeasureTheory.Integrable
      (fun c =>
        OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
          ↑(b (inner ℝ a x + c)))
      MeasureTheory.volume
    theorem OperatorRidgelet.Paper.thm_4_5_iii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  ∀ᵐ (a : H) ∂ν,
    MeasureTheory.Integrable
      (fun c =>
        OperatorRidgelet.coefficientFormula
            (⇑ρ) G (a, c) *
          ↑(b (inner ℝ a x + c)))
      MeasureTheory.volume
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For a
tempered `β` that is a continuous function `b` of polynomial growth, and
`G` regular along rays, the inner integral `∫ γ_G(a,c) β(⟨a,x⟩+c) dc` converges absolutely for
`ν_α`-almost every `a`.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_iii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  MeasureTheory.Integrable
    (fun a =>
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
          ↑(b (inner ℝ a x + c)))
    ν
    theorem OperatorRidgelet.Paper.thm_4_5_iii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  MeasureTheory.Integrable
    (fun a =>
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula
            (⇑ρ) G (a, c) *
          ↑(b (inner ℝ a x + c)))
    ν
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For a
tempered `β` that is a continuous function `b` of polynomial growth, and
`G` regular along rays, the `ν_α`-integral of the inner integral converges absolutely.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_iii_c.{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.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula (⇑ρ) G (a, c) *
          ↑(b (inner ℝ a x + c)) ∂ν =
    OperatorRidgelet.temperedAdmissibilityConst α β ρ *
      OperatorRidgelet.spectralTarget ν G x
    theorem OperatorRidgelet.Paper.thm_4_5_iii_c.{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.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  ∫ (a : H),
      ∫ (c : ℝ),
        OperatorRidgelet.coefficientFormula
            (⇑ρ) G (a, c) *
          ↑(b (inner ℝ a x + c)) ∂ν =
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ *
      OperatorRidgelet.spectralTarget ν G
        x
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For a
tempered `β` that is a continuous function `b` of polynomial growth, and
`G` regular along rays, the tempered spectral synthesis identity
`∫ [∫ γ_G(a,c) β(⟨a,x⟩+c) dc] ν_α(da) = C^{(α)}_{β,ρ} g_G(x)` holds.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_iii_d {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b)
  (hb : ¬OperatorRidgelet.IsPolynomialFun b) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0
    theorem OperatorRidgelet.Paper.thm_4_5_iii_d
  {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (hb :
    ¬OperatorRidgelet.IsPolynomialFun b) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α β ρ ≠
        0
    **Theorem [thm:4.5]** Integral representation of targets with a spectral density.  For every
tempered `β` that is a continuous function of polynomial growth and not a polynomial, there is a
band-pass filter `ρ` with `C^{(α)}_{β,ρ} ≠ 0`.
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.thm_4_5_iii_e.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  MeasureTheory.Integrable
    (fun θ =>
      OperatorRidgelet.coefficientFormula (⇑ρ) G θ *
        ↑(b (inner ℝ θ.1 x + θ.2)))
    (OperatorRidgelet.parameterMeasure ν)
    theorem OperatorRidgelet.Paper.thm_4_5_iii_e.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  MeasureTheory.Integrable
    (fun θ =>
      OperatorRidgelet.coefficientFormula
          (⇑ρ) G θ *
        ↑(b (inner ℝ θ.1 x + θ.2)))
    (OperatorRidgelet.parameterMeasure ν)
    **Theorem [thm:4.5]** The network integrand is jointly absolutely integrable.
Proof for Theorem 4.5
Proof uses 4
Proof dependency previews
Preview
Lemma 3.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Part (i) is Lemma 4.1. Parseval in the bias turns the inner integral into a frequency integral of \rho^\sharp(\omega)G(-\omega a) against \rho^\sharp(-\omega)e^{-i\omega\langle a,x\rangle}, and the homogeneous substitution \xi=-\omega a separates the admissibility constant from g_G(x). For a tempered \beta the bias integral is a distributional pairing with a test function supported in -\operatorname{supp}\rho^\sharp; Definition 4.2 makes a\mapsto (test function) Bochner integrable in a C^m norm, so the pairing commutes with the direction integral. Joint absolute integrability follows independently from Lemma 4.3, choosing a moment at least as large as the activation's polynomial growth order. If every band-pass test function paired to zero with \beta^\sharp, its support would be \{0\} and \beta a polynomial.