3.1. Targets with a spectral density🔗

Lemma3.1.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 3.1.5

Loading preview

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

✓L∃∀N

Let \nu be a Borel measure on H, let Y be a separable complex Hilbert space, and let G\in L^1(\nu;Y). Then g_G(x)=\int_H e^{i\langle x,\xi\rangle}G(\xi)\,\nu(\mathrm d\xi) belongs to C_b(H;Y), satisfies \|g_G\|_\infty\le\|G\|_{L^1(\nu;Y)}, and determines G up to \nu-almost-everywhere equality. No input weight, filter, homogeneity, or full-support assumption is needed.

Lean code for Lemma3.1.1●3 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_spectral_target_basic_i.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] (ν : MeasureTheory.Measure H) (G : H → Y)
  (_hG : MeasureTheory.Integrable G ν) (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G x‖ ≤ ∫ (ξ : H), ‖G ξ‖ ∂ν

theorem OperatorRidgelet.Paper.lem_spectral_target_basic_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (_hG : MeasureTheory.Integrable G ν)
  (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G
        x‖ ≤
    ∫ (ξ : H), ‖G ξ‖ ∂ν

**Lemma [lem:spectral-target-basic]** The spectral target has the uniform L¹ norm bound.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_spectral_target_basic_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]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.Integrable G ν) :
  Continuous (OperatorRidgelet.spectralTarget ν G)

theorem OperatorRidgelet.Paper.lem_spectral_target_basic_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]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG : MeasureTheory.Integrable G ν) :
  Continuous
    (OperatorRidgelet.spectralTarget ν G)

**Lemma [lem:spectral-target-basic]** An integrable spectral density has a continuous target.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_spectral_target_basic_iii.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.Integrable G ν)
  (hzero : OperatorRidgelet.spectralTarget ν G = 0) : G =ᵐ[ν] 0

theorem OperatorRidgelet.Paper.lem_spectral_target_basic_iii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG : MeasureTheory.Integrable G ν)
  (hzero :
    OperatorRidgelet.spectralTarget ν G =
      0) :
  G =ᵐ[ν] 0

**Lemma [lem:spectral-target-basic]** A spectral density is determined by its target.

Proof for Lemma 3.1.1

uses 0

The integral triangle inequality gives the norm bound, and dominated convergence with majorant \|G(\xi)\|_Y gives continuity. If g_G=0, pair the finite vector measure G\nu with vectors in a countable dense subset of Y. Fourier uniqueness makes each resulting scalar measure zero: finite-dimensional Fourier uniqueness determines all cylinder sets, which generate the Borel sigma-algebra of H. Intersect the countably many full-measure sets and use continuity of the pairing to obtain G=0 almost everywhere. Apply the argument to a difference for uniqueness.

The coefficient operator W_\rho G and its almost-everywhere absolutely convergent inverse Fourier formula require only G\in L^2(\nu_\alpha) (Lemma 2.2.6). The additional L^1 assumption below defines the continuous spectral target and justifies its synthesis.

Definition3.1.2

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.2

Loading preview

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

Used by 7

Reverse dependency previews

Preview

Lemma 3.1.3

Loading preview

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

✓L∃∀N

Fix a symmetric compact set I\subset\mathbb R\setminus\{0\} containing \operatorname{supp}\widehat\rho (a frequency window). A bounded Borel G:H\to\mathbb C is regular along rays if for every a\in H the function \omega\mapsto G(\omega a) is C^\infty on a neighbourhood of I and M_m(G)=\int_H(1+\|a\|)^{m+2}\max_{k\le m}\sup_{\omega\in I}|\partial_\omega^kG(\omega a)|\,\nu_\alpha(\mathrm da)<\infty for every integer m\ge0. Such a G belongs to L^1(\nu_\alpha)\cap L^2(\nu_\alpha) (the theorem part of the definition).

Lean code for Definition3.1.2●6 declarations

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

complete

structure OperatorRidgelet.IsFrequencyWindow (ρ : ℝ → ℝ) (I : Set ℝ) : Prop

structure OperatorRidgelet.IsFrequencyWindow
  (ρ : ℝ → ℝ) (I : Set ℝ) : Prop

The frequency window fixed before Definition `def:ray-regular`: a symmetric compact set
`I ⊆ ℝ ∖ {0}` containing the support of `ρ̂`.

Fields

isCompact : IsCompact I

`I` is compact.

zero_notMem : 0 ∉ I

`I` stays away from the origin.

neg_mem : ∀ ω ∈ I, -ω ∈ I

`I` is symmetric.

tsupport_subset : tsupport (OperatorRidgelet.filterFourier ρ) ⊆ I

`I` contains the support of `ρ̂`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.rayDerivBound.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (I : Set ℝ) (G : H → Y)
  (m : ℕ) (a : H) : ENNReal

def OperatorRidgelet.rayDerivBound.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (I : Set ℝ) (G : H → Y) (m : ℕ)
  (a : H) : ENNReal

The ray-derivative bound `max_{k ≤ m} sup_{ω ∈ I} ‖∂_ω^k G(ωa)‖` of a density `G` at the
direction `a`, in `ℝ≥0∞`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.rayMoment.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (I : Set ℝ) (G : H → Y) (m : ℕ) :
  ENNReal

def OperatorRidgelet.rayMoment.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) (G : H → Y) (m : ℕ) :
  ENNReal

The ray moment `M_m(G) = ∫ (1+‖a‖)^{m+2} max_{k ≤ m} sup_{ω ∈ I} ‖∂_ω^k G(ωa)‖ ν(da)`
(`eq:ray-regularity`), in `ℝ≥0∞`.

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

complete

structure OperatorRidgelet.IsRegularAlongRays.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (I : Set ℝ) (G : H → Y) : Prop

structure OperatorRidgelet.IsRegularAlongRays.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) (G : H → Y) : Prop

**Definition [def:ray-regular]** A bounded Borel density `G` is regular along rays (with
respect to the direction measure `ν` and the frequency window `I`) if for every direction `a`
the map `ω ↦ G(ωa)` is `C^∞` on a neighbourhood of `I` and every ray moment `M_m(G)` is
finite.

Fields

stronglyMeasurable : MeasureTheory.StronglyMeasurable G

`G` is Borel.

bounded : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M

`G` is bounded.

contDiffOn : ∀ (a : H), ∃ U, IsOpen U ∧ I ⊆ U ∧ ContDiffOn ℝ (↑⊤) (fun ω => G (ω • a)) U

`ω ↦ G(ωa)` is `C^∞` on an open neighbourhood of `I`, for every direction `a`.

rayMoment_lt_top : ∀ (m : ℕ), OperatorRidgelet.rayMoment ν I G m < ⊤

`M_m(G) < ∞` for every `m`.

defdefined in OperatorRidgelet/Reconstruction/Defs.lean

complete

def OperatorRidgelet.spectralTarget.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (G : H → Y) (x : H) : Y

def OperatorRidgelet.spectralTarget.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y) (x : H) : Y

The target with spectral density `G` with respect to `ν`,
`g_G(x) = ∫ e^{i⟪x,ξ⟫} G(ξ) ν(dξ)` (`eq:spectral-target`), the Fourier transform of the finite
measure `G ν`; for a scalar density `•` is the product.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.def_ray_regular.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) :
  MeasureTheory.Integrable G ν ∧ MeasureTheory.MemLp G 2 ν

theorem OperatorRidgelet.Paper.def_ray_regular.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G) :
  MeasureTheory.Integrable G ν ∧
    MeasureTheory.MemLp G 2 ν

**Definition [def:ray-regular]** Regularity along rays.  A density that is regular along
rays belongs to `L¹(ν_α) ∩ L²(ν_α)` (homogeneity with a fixed `ω ∈ I`).

Lemma3.1.3

Statement uses 5

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 3.1.5

Loading preview

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

✓L∃∀N

Fix a band-pass \rho, a symmetric compact frequency window I away from zero, and an integer r\ge0. Let Y be a separable complex Hilbert space and let G:H\to Y be bounded and Borel, with \omega\mapsto G(\omega a) of class C^{r+2} near I for every a. Write D_m(a)=\max_{k\le m}\sup_{\omega\in I}\|\partial_\omega^kG(\omega a)\|_Y and A_{m,r}(G)=\int_H(1+\|a\|)^rD_m(a)\,\nu_\alpha(\mathrm da). If A_{r+2,r}(G)<\infty, then G\in L^1(\nu_\alpha;Y)\cap L^2(\nu_\alpha;Y), and the inverse Fourier integral is a jointly measurable representative \gamma_G of W_\rho G. Moreover, (1+|c|)^{r+2}\|\gamma_G(a,c)\|_Y\le C_{\rho,I,r}D_{r+2}(a) and \int_{H\times\mathbb R}(1+\|a\|+|c|)^r\|\gamma_G(a,c)\|_Y\,\mathrm d\lambda_\alpha\le c_{\rho,I,r}A_{r+2,r}(G). The constants do not depend on G or the dimension of Y.

Lean code for Lemma3.1.3●5 theorems

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_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]
  (ν : MeasureTheory.Measure H) {α : ℝ}
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M) (r : ℕ)
  (hM : OperatorRidgelet.finiteRayMoment ν I G (r + 2) r < ⊤) :
  MeasureTheory.Integrable G ν ∧ MeasureTheory.MemLp G 2 ν

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_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]
  (ν : MeasureTheory.Measure H) {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (r : ℕ)
  (hM :
    OperatorRidgelet.finiteRayMoment ν I G
        (r + 2) r <
      ⊤) :
  MeasureTheory.Integrable G ν ∧
    MeasureTheory.MemLp G 2 ν

**Lemma [lem:coefficient-finite-order]** A bounded density with a finite ray moment is L¹∩L².

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_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α : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M) (r : ℕ)
  (hM : OperatorRidgelet.finiteRayMoment ν I G (r + 2) r < ⊤) :
  MeasureTheory.StronglyMeasurable
      (OperatorRidgelet.coefficientFormulaVec (⇑ρ) G) ∧
    ↑↑(OperatorRidgelet.spectralCoefficientVec ν (⇑ρ)
            G) =ᵐ[OperatorRidgelet.parameterMeasure ν]
      OperatorRidgelet.coefficientFormulaVec (⇑ρ) G

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_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α : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (r : ℕ)
  (hM :
    OperatorRidgelet.finiteRayMoment ν I G
        (r + 2) r <
      ⊤) :
  MeasureTheory.StronglyMeasurable
      (OperatorRidgelet.coefficientFormulaVec
        (⇑ρ) G) ∧
    ↑↑(OperatorRidgelet.spectralCoefficientVec
            ν (⇑ρ)
            G) =ᵐ[OperatorRidgelet.parameterMeasure
        ν]
      OperatorRidgelet.coefficientFormulaVec
        (⇑ρ) G

**Lemma [lem:coefficient-finite-order]** The inverse integral represents the coefficient.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_iii.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (r : ℕ) :
  0 < OperatorRidgelet.finiteCoefficientDecayConstant ρ (r + 2) ∧
    OperatorRidgelet.finiteCoefficientDecayConstant ρ (r + 2) < ⊤ ∧
      ∀ (G : H → Y),
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2)) (fun ω => G (ω • a)) U) →
          ∀ (a : H) (c : ℝ),
            ENNReal.ofReal ((1 + |c|) ^ (r + 2)) *
                ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
                    (a, c)‖ₑ ≤
              OperatorRidgelet.finiteCoefficientDecayConstant ρ
                  (r + 2) *
                OperatorRidgelet.rayDerivBound I G (r + 2) a

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_iii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (r : ℕ) :
  0 <
      OperatorRidgelet.finiteCoefficientDecayConstant
        ρ (r + 2) ∧
    OperatorRidgelet.finiteCoefficientDecayConstant
          ρ (r + 2) <
        ⊤ ∧
      ∀ (G : H → Y),
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2))
                    (fun ω => G (ω • a))
                    U) →
          ∀ (a : H) (c : ℝ),
            ENNReal.ofReal
                  ((1 + |c|) ^ (r + 2)) *
                ‖OperatorRidgelet.coefficientFormulaVec
                    (⇑ρ) G (a, c)‖ₑ ≤
              OperatorRidgelet.finiteCoefficientDecayConstant
                  ρ (r + 2) *
                OperatorRidgelet.rayDerivBound
                  I G (r + 2) a

**Lemma [lem:coefficient-finite-order]** Finitely many ray derivatives give pointwise decay.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_iv.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (r : ℕ) :
  OperatorRidgelet.finiteCoefficientMomentConstant ρ r ≠ ⊤ ∧
    ∀ (G : H → Y),
      MeasureTheory.StronglyMeasurable G →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2)) (fun ω => G (ω • a)) U) →
          ∫⁻ (θ : H × ℝ),
              ENNReal.ofReal ((1 + ‖θ.1‖ + |θ.2|) ^ r) *
                ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
                    θ‖ₑ ∂OperatorRidgelet.parameterMeasure ν ≤
            OperatorRidgelet.finiteCoefficientMomentConstant ρ r *
              OperatorRidgelet.finiteRayMoment ν I G (r + 2) r

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_iv.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (r : ℕ) :
  OperatorRidgelet.finiteCoefficientMomentConstant
        ρ r ≠
      ⊤ ∧
    ∀ (G : H → Y),
      MeasureTheory.StronglyMeasurable G →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2))
                    (fun ω => G (ω • a))
                    U) →
          ∫⁻ (θ : H × ℝ),
              ENNReal.ofReal
                  ((1 + ‖θ.1‖ + |θ.2|) ^
                    r) *
                ‖OperatorRidgelet.coefficientFormulaVec
                    (⇑ρ) G
                    θ‖ₑ ∂OperatorRidgelet.parameterMeasure
                ν ≤
            OperatorRidgelet.finiteCoefficientMomentConstant
                ρ r *
              OperatorRidgelet.finiteRayMoment
                ν I G (r + 2) r

**Lemma [lem:coefficient-finite-order]** The parameter moment is bounded by A_{r+2,r}.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_v.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G) (r : ℕ)
  (hGs :
    ∀ (a : H),
      ∃ U,
        IsOpen U ∧
          I ⊆ U ∧ ContDiffOn ℝ (↑(r + 2)) (fun ω => G (ω • a)) U)
  (hM : OperatorRidgelet.finiteRayMoment ν I G (r + 2) r < ⊤) :
  MeasureTheory.Integrable
    (fun θ =>
      (1 + ‖θ.1‖ + |θ.2|) ^ r *
        ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G θ‖)
    (OperatorRidgelet.parameterMeasure ν)

theorem OperatorRidgelet.Paper.lem_coefficient_finite_order_v.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (r : ℕ)
  (hGs :
    ∀ (a : H),
      ∃ U,
        IsOpen U ∧
          I ⊆ U ∧
            ContDiffOn ℝ (↑(r + 2))
              (fun ω => G (ω • a)) U)
  (hM :
    OperatorRidgelet.finiteRayMoment ν I G
        (r + 2) r <
      ⊤) :
  MeasureTheory.Integrable
    (fun θ =>
      (1 + ‖θ.1‖ + |θ.2|) ^ r *
        ‖OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G θ‖)
    (OperatorRidgelet.parameterMeasure ν)

**Lemma [lem:coefficient-finite-order]** Finite ray data imply a finite parameter moment.

Proof for Lemma 3.1.3

uses 0

Difference quotients and countable dense subsets of I give measurability of D_m. Homogeneity at one fixed nonzero frequency gives G\in L^1; boundedness gives G\in L^2. Set m=r+2 and h_a(\omega)=\widehat\rho(\omega)G(-\omega a). Leibniz' rule bounds \|h_a\|_1+\|h_a^{(m)}\|_1 by a filter-dependent constant times D_m(a). The function h_a is compactly supported and C^m; the derivatives of the filter vanish at its support boundary. Bound the inverse Fourier integral directly for |c|\le1, and integrate by parts m times for |c|>1. This proves the decay estimate. Finally use 1+\|a\|+|c|\le(1+\|a\|)(1+|c|) and \int_{\mathbb R}(1+|c|)^{-2}\,\mathrm dc=2 to obtain the moment bound by Tonelli. No synthesis identity enters this argument.

This is the coefficient estimate placed before the representation proof in Appendix B. In particular, C^4 ray regularity and A_{4,2}(G)<\infty suffice for a second parameter moment. Full regularity along rays gives A_{r+2,r}(G)\le M_{r+2}(G) and hence moments of all orders. The finite-order estimate alone does not assert tempered synthesis.

Definition3.1.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 3.1.5

Loading preview

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

✓L∃∀N

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\widehat\rho(-\omega)|\omega|^{-\alpha} is a Schwartz function, and the distributional admissibility constant is C_{\beta,\rho}^{(\alpha)}=\frac1{2\pi}\langle\widehat\beta,\widehat\rho(-\,\cdot\,)|\cdot|^{-\alpha}\rangle.

Lean code for Definition3.1.4●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 `ρ`.

Theorem3.1.5

Statement uses 8

Statement dependency previews

Preview

Definition 1.1.2

Loading preview

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

Used by 7

Reverse dependency previews

Preview

Theorem 3.3.2

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)\!)_\alphag_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 regular along rays, 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 Theorem3.1.5●11 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.thm_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_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_A_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:A]** 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_A_iii_d {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b)
  (hb : ¬OperatorRidgelet.IsPolynomialFun b) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0

theorem OperatorRidgelet.Paper.thm_A_iii_d {α : ℝ}
  (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (hb :
    ¬OperatorRidgelet.IsPolynomialFun b) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α β ρ ≠
        0

**Theorem [thm:A]** 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_A_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_A_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:A]** Tempered synthesis is jointly absolutely integrable.

Proof for Theorem 3.1.5

uses 0

Part (i) is Lemma 3.1.1. Parseval in the bias turns the inner integral into a frequency integral of \widehat\rho(\omega)G(-\omega a) against \widehat\rho(-\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}\widehat\rho; regularity along rays 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 3.1.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 \widehat\beta, its support would be \{0\} and \beta a polynomial.