5.2. Finite variation from the spectral density🔗

Theorem5.2.1

Statement uses 8

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Proposition 4.2.3

Loading preview

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

✓L∃∀N

Let \rho be a band-pass filter with frequency window I, and let G be regular along rays. For every integer r\ge0 there is a finite constant c_{\rho,r} such that \int_{H\times\mathbb R}(1+\|a\|+|c|)^r\|\gamma_G(a,c)\|\,\mathrm d\lambda_\alpha\le c_{\rho,r}M_{r+2}(G)<\infty. The same constant works for every Hilbert output space Y; it depends only on the filter and the order. In particular, \int(1+\|a\|^2+|c|^2)|\gamma_G(a,c)|\,\mathrm d\lambda_\alpha\le c_{\rho,2}M_4(G)<\infty. For every real globally Lipschitz \beta, the target C_{\beta,\rho}^{(\alpha)}g_G is the integral network S_\beta[\gamma_G\lambda_\alpha]. Its sampled network satisfies \mathbb E\|f_N-C_{\beta,\rho}^{(\alpha)}g_G\|_{C(K)}\le\frac{8V}{\sqrt N}(|\beta(0)|+\operatorname{Lip}(\beta)R_KM_2) for every compact K, where V=\|\gamma_G\|_{L^1} and M_2 is computed under |\gamma_G|\lambda_\alpha/V. If V=0, use the zero network.

Lean code for Theorem5.2.1●5 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_E_i.{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) :
  ∃ c,
    c ≠ ⊤ ∧
      ∀ (G : H → ℂ),
        OperatorRidgelet.IsRegularAlongRays ν I G →
          ∫⁻ (θ : H × ℝ),
              ENNReal.ofReal (1 + ‖θ.1‖ ^ 2 + |θ.2| ^ 2) *
                ‖OperatorRidgelet.coefficientFormula (⇑ρ) G
                    θ‖ₑ ∂OperatorRidgelet.parameterMeasure ν ≤
            c * OperatorRidgelet.rayMoment ν I G 4

theorem OperatorRidgelet.Paper.thm_E_i.{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) :
  ∃ c,
    c ≠ ⊤ ∧
      ∀ (G : H → ℂ),
        OperatorRidgelet.IsRegularAlongRays
            ν I G →
          ∫⁻ (θ : H × ℝ),
              ENNReal.ofReal
                  (1 + ‖θ.1‖ ^ 2 +
                    |θ.2| ^ 2) *
                ‖OperatorRidgelet.coefficientFormula
                    (⇑ρ) G
                    θ‖ₑ ∂OperatorRidgelet.parameterMeasure
                ν ≤
            c *
              OperatorRidgelet.rayMoment ν
                I G 4

**Theorem [thm:E]** Finite variation and moments of the coefficient.  For a band-pass `ρ`
with frequency window `I` there is a finite constant `c_ρ`, depending only on `ρ` and `α`,
such that every `G` regular along rays satisfies
`∫ (1 + ‖a‖² + |c|²) |γ_G| dλ_α ≤ c_ρ M₄(G)`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_E_ii.{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) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) :
  MeasureTheory.Integrable
    (fun θ =>
      (1 + ‖θ.1‖ ^ 2 + |θ.2| ^ 2) *
        ‖OperatorRidgelet.coefficientFormula (⇑ρ) G θ‖)
    (OperatorRidgelet.parameterMeasure ν)

theorem OperatorRidgelet.Paper.thm_E_ii.{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)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G) :
  MeasureTheory.Integrable
    (fun θ =>
      (1 + ‖θ.1‖ ^ 2 + |θ.2| ^ 2) *
        ‖OperatorRidgelet.coefficientFormula
            (⇑ρ) G θ‖)
    (OperatorRidgelet.parameterMeasure ν)

**Theorem [thm:E]** Finite variation and moments of the coefficient.  For `G` regular along
rays, `∫ (1 + ‖a‖² + |c|²) |γ_G| dλ_α < ∞`: the coefficient measure `γ_G λ_α` is finite with
finite second moment.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_E_iii.{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) {L : NNReal}
  (hb : LipschitzWith L b) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  OperatorRidgelet.temperedAdmissibilityConst α β ρ *
      OperatorRidgelet.spectralTarget ν G x =
    OperatorRidgelet.integralNetworkDensity (fun t => ↑(b t))
      (OperatorRidgelet.parameterMeasure ν)
      (OperatorRidgelet.coefficientFormula (⇑ρ) G) x

theorem OperatorRidgelet.Paper.thm_E_iii.{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)
  {L : NNReal} (hb : LipschitzWith L b)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  OperatorRidgelet.temperedAdmissibilityConst
        α β ρ *
      OperatorRidgelet.spectralTarget ν G
        x =
    OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(b t))
      (OperatorRidgelet.parameterMeasure
        ν)
      (OperatorRidgelet.coefficientFormula
        (⇑ρ) G)
      x

**Theorem [thm:E]** Finite variation and moments of the coefficient.  Consequently, for every
real `β` that is globally Lipschitz (a tempered activation that is the
function `b`), the target `C^{(α)}_{β,ρ} g_G` is the integral network `S_β[γ_G λ_α]`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_E_iv.{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) {L : NNReal}
  (hb : LipschitzWith L b) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) {K : Set H}
  (hK : IsCompact K) {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.densitySampledNetwork (fun t => ↑(b t))
            (OperatorRidgelet.parameterMeasure ν)
            (OperatorRidgelet.coefficientFormula (⇑ρ) G) θ x -
          OperatorRidgelet.temperedAdmissibilityConst α β ρ *
            OperatorRidgelet.spectralTarget ν G
              x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure ν)
          (OperatorRidgelet.coefficientFormula (⇑ρ) G)) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure ν)
            (OperatorRidgelet.coefficientFormula (⇑ρ) G) /
        √↑N *
      (|b 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure ν)
                (OperatorRidgelet.coefficientFormula (⇑ρ) G))))

theorem OperatorRidgelet.Paper.thm_E_iv.{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)
  {L : NNReal} (hb : LipschitzWith L b)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.densitySampledNetwork
            (fun t => ↑(b t))
            (OperatorRidgelet.parameterMeasure
              ν)
            (OperatorRidgelet.coefficientFormula
              (⇑ρ) G)
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst
              α β ρ *
            OperatorRidgelet.spectralTarget
              ν G
              x ∂OperatorRidgelet.sampleLaw
        N
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            ν)
          (OperatorRidgelet.coefficientFormula
            (⇑ρ) G)) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              ν)
            (OperatorRidgelet.coefficientFormula
              (⇑ρ) G) /
        √↑N *
      (|b 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  ν)
                (OperatorRidgelet.coefficientFormula
                  (⇑ρ) G))))

**Theorem [thm:E]** Finite variation and moments of the coefficient.  For real globally
Lipschitz `β`, the sampled network `eq:polar-network` of `γ_G λ_α`, with
`V = ‖γ_G‖_{L¹(λ_α)}` and `M₂` the second moment of `p = |γ_G| λ_α / V`, satisfies
`𝔼‖f_N − C^{(α)}_{β,ρ} g_G‖_{C(K)} ≤ (8V/√N)(|β(0)| + Lip(β) R_K M₂)` for every compact
`K`.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_E_moments.{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),
      OperatorRidgelet.IsRegularAlongRays ν I G →
        ∫⁻ (θ : H × ℝ),
            ENNReal.ofReal ((1 + ‖θ.1‖ + |θ.2|) ^ r) *
              ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
                  θ‖ₑ ∂OperatorRidgelet.parameterMeasure ν ≤
          OperatorRidgelet.finiteCoefficientMomentConstant ρ r *
            OperatorRidgelet.rayMoment ν I G (r + 2)

theorem OperatorRidgelet.Paper.thm_E_moments.{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),
      OperatorRidgelet.IsRegularAlongRays
          ν I G →
        ∫⁻ (θ : H × ℝ),
            ENNReal.ofReal
                ((1 + ‖θ.1‖ + |θ.2|) ^
                  r) *
              ‖OperatorRidgelet.coefficientFormulaVec
                  (⇑ρ) G
                  θ‖ₑ ∂OperatorRidgelet.parameterMeasure
              ν ≤
          OperatorRidgelet.finiteCoefficientMomentConstant
              ρ r *
            OperatorRidgelet.rayMoment ν I
              G (r + 2)

**Theorem [thm:E]** All parameter moments are bounded, also for vector-valued densities.

Proof for Theorem 5.2.1

uses 0

Apply Lemma 3.1.3 and A_{r+2,r}(G)\le M_{r+2}(G). The coefficient decays as (1+|c|)^{-r-2}; two powers give an integrable bias weight and the other r powers control the parameter moment. The scalar constant is independent of Y. Use 1+\|a\|^2+|c|^2\le(1+\|a\|+|c|)^2 for the second moment, then Theorem 3.1.5 (iii) and Theorem 5.1.6 for synthesis and sampling.

Lemma5.2.2

Statement uses 3

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 5.3.1

Loading preview

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

✓L∃∀N

The following functions are regular along rays for every band-pass \rho. (a) G(\xi)=q(\xi)e^{-\kappa(\xi)/2}, where \kappa(\xi)=\langle S\xi,\xi\rangle, S is bounded and positive, S\ge\theta Q for some \theta>0, and q is a polynomial in \kappa and finitely many bounded linear functionals \ell_i satisfying |\ell_i(\xi)|^2\le C_i\kappa(\xi) for every \xi. Equivalently, \ell_i=\langle S^{1/2}v_i,\cdot\rangle for some v_i\in H. A polynomial in \kappa alone requires no further condition. (b) G(\xi)=\varphi(\|\xi-\xi_0\|^2) for \varphi\in C_c^\infty(\mathbb R); more generally, bounded densities smooth along rays, with bounded support and \sup_{\omega\in I}|\partial_\omega^kG(\omega a)|\le C_k(1+\|a\|)^{p_k} for every k. (c) Finite linear combinations, and Bochner integrals G=\int_\Omega G_y\,m(\mathrm dy) of uniformly bounded measurable families over a finite measure, subject to these neighbourhood bounds: there is an open U\supset I where every ray of every G_y is smooth, and finite-valued Borel h_k:H\to[0,\infty) such that \sup_{\omega\in U}|\partial_\omega^kG_y(\omega a)|\le h_k(a) for every y,a,k, and \int_H(1+\|a\|)^{m+2}\max_{k\le m}h_k(a)\,\nu_\alpha(\mathrm da)<\infty for every m. The bounds hold on the open neighbourhood and for every direction.

Lean code for Lemma5.2.2●5 theorems

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (S : H →L[ℝ] H) (hS : IsSelfAdjoint S) {θ : ℝ}
  (hθ : 0 < θ) (hSQ : ∀ (ξ : H), θ * inner ℝ (Q ξ) ξ ≤ inner ℝ (S ξ) ξ)
  {k : ℕ} (ℓ : Fin k → H →L[ℝ] ℝ)
  (hℓ :
    ∀ (i : Fin k), ∃ C, ∀ (ξ : H), (ℓ i) ξ ^ 2 ≤ C * inner ℝ (S ξ) ξ)
  (q : MvPolynomial (Option (Fin k)) ℂ) (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture N α) I fun ξ =>
          (MvPolynomial.eval fun o =>
                o.elim ↑(inner ℝ (S ξ) ξ) fun i => ↑((ℓ i) ξ))
              q *
            Complex.exp (-↑(inner ℝ (S ξ) ξ / 2))

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (S : H →L[ℝ] H)
  (hS : IsSelfAdjoint S) {θ : ℝ}
  (hθ : 0 < θ)
  (hSQ :
    ∀ (ξ : H),
      θ * inner ℝ (Q ξ) ξ ≤
        inner ℝ (S ξ) ξ)
  {k : ℕ} (ℓ : Fin k → H →L[ℝ] ℝ)
  (hℓ :
    ∀ (i : Fin k),
      ∃ C,
        ∀ (ξ : H),
          (ℓ i) ξ ^ 2 ≤
            C * inner ℝ (S ξ) ξ)
  (q : MvPolynomial (Option (Fin k)) ℂ)
  (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow
          (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture
            N α)
          I fun ξ =>
          (MvPolynomial.eval fun o =>
                o.elim ↑(inner ℝ (S ξ) ξ)
                  fun i => ↑((ℓ i) ξ))
              q *
            Complex.exp
              (-↑(inner ℝ (S ξ) ξ / 2))

**Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Gaussian-type
densities `G(ξ) = q(ξ) e^{-κ(ξ)/2}`, `κ(ξ) = ⟨Sξ,ξ⟩` with `S` a bounded positive operator with
`S ≥ θQ`, `θ > 0`, and `q` a polynomial in `κ(ξ)` and in finitely many bounded linear
functionals `ℓ_i` of `ξ` dominated by the quadratic form, `|ℓ_i(ξ)|² ≤ C_i κ(ξ)`, are regular
along rays for every band-pass `ρ` (and every frequency window of `ρ`).

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_b_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (ξ₀ : H) (φ : ℝ → ℂ) (hφ : ContDiff ℝ (↑⊤) φ)
  (hφc : HasCompactSupport φ) (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture N α) I fun ξ =>
          φ (‖ξ - ξ₀‖ ^ 2)

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_b_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (ξ₀ : H)
  (φ : ℝ → ℂ) (hφ : ContDiff ℝ (↑⊤) φ)
  (hφc : HasCompactSupport φ)
  (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow
          (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture
            N α)
          I fun ξ => φ (‖ξ - ξ₀‖ ^ 2)

**Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Radial bumps
`G(ξ) = φ(‖ξ - ξ₀‖²)` with `φ ∈ C_c^∞(ℝ)` are regular along rays for every band-pass `ρ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_b_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (hH : ¬FiniteDimensional ℝ H) {P : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (G : H → ℂ) (hG : Measurable G)
  (hGb : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (hG0 : ∃ R₀, ∀ (ξ : H), R₀ < ‖ξ‖ → G ξ = 0) (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧ ContDiffOn ℝ (↑⊤) (fun ω => G (ω • a)) U) →
          (∀ (k : ℕ),
              ∃ C p,
                ∀ (a : H),
                  ∀ ω ∈ I,
                    ‖iteratedDeriv k (fun ω => G (ω • a)) ω‖ ≤
                      C * (1 + ‖a‖) ^ p) →
            OperatorRidgelet.IsRegularAlongRays
              (OperatorRidgelet.gaussianMixture N α) I G

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_b_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (G : H → ℂ)
  (hG : Measurable G)
  (hGb : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (hG0 :
    ∃ R₀, ∀ (ξ : H), R₀ < ‖ξ‖ → G ξ = 0)
  (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow
          (⇑ρ) I →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑⊤)
                    (fun ω => G (ω • a))
                    U) →
          (∀ (k : ℕ),
              ∃ C p,
                ∀ (a : H),
                  ∀ ω ∈ I,
                    ‖iteratedDeriv k
                          (fun ω =>
                            G (ω • a))
                          ω‖ ≤
                      C * (1 + ‖a‖) ^ p) →
            OperatorRidgelet.IsRegularAlongRays
              (OperatorRidgelet.gaussianMixture
                N α)
              I G

**Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  More generally,
a bounded Borel `G` that is `C^∞` along rays (on a neighbourhood of the frequency window),
vanishes outside a bounded set, and satisfies `sup_{ω ∈ I} |∂_ω^k G(ωa)| ≤ C_k (1+‖a‖)^{p_k}`
for all `k`, is regular along rays for every band-pass `ρ`.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_c_i.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H) (I : Set ℝ)
  {ι : Type u_2} (s : Finset ι) (c : ι → ℂ) (G : ι → H → ℂ)
  (hG : ∀ i ∈ s, OperatorRidgelet.IsRegularAlongRays ν I (G i)) :
  OperatorRidgelet.IsRegularAlongRays ν I fun ξ => ∑ i ∈ s, c i * G i ξ

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_c_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) {ι : Type u_2}
  (s : Finset ι) (c : ι → ℂ)
  (G : ι → H → ℂ)
  (hG :
    ∀ i ∈ s,
      OperatorRidgelet.IsRegularAlongRays
        ν I (G i)) :
  OperatorRidgelet.IsRegularAlongRays ν I
    fun ξ => ∑ i ∈ s, c i * G i ξ

**Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Finite linear
combinations of densities that are regular along rays are regular along rays.

theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean

complete

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_c_ii.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (ν : MeasureTheory.Measure H) (I : Set ℝ)
  {Ω : Type u_2} [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (G : Ω → H → ℂ)
  (hGm : Measurable (Function.uncurry G))
  (hG : ∀ (y : Ω), OperatorRidgelet.IsRegularAlongRays ν I (G y))
  (hGb : ∃ M, ∀ (y : Ω) (ξ : H), ‖G y ξ‖ ≤ M) (U : Set ℝ)
  (hU : IsOpen U) (hIU : I ⊆ U)
  (hsmooth :
    ∀ (y : Ω) (a : H), ContDiffOn ℝ (↑⊤) (fun ω => G y (ω • a)) U)
  (hunif :
    ∀ (k : ℕ),
      ∃ h,
        ∫⁻ (a : H), ENNReal.ofReal ((1 + ‖a‖) ^ (k + 2)) * ↑(h a) ∂ν <
            ⊤ ∧
          ∀ (y : Ω) (a : H),
            OperatorRidgelet.rayDerivBound U (G y) k a ≤ ↑(h a)) :
  OperatorRidgelet.IsRegularAlongRays ν I fun ξ => ∫ (y : Ω), G y ξ ∂m

theorem OperatorRidgelet.Paper.lem_ray_regular_examples_c_ii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) {Ω : Type u_2}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (G : Ω → H → ℂ)
  (hGm : Measurable (Function.uncurry G))
  (hG :
    ∀ (y : Ω),
      OperatorRidgelet.IsRegularAlongRays
        ν I (G y))
  (hGb :
    ∃ M, ∀ (y : Ω) (ξ : H), ‖G y ξ‖ ≤ M)
  (U : Set ℝ) (hU : IsOpen U)
  (hIU : I ⊆ U)
  (hsmooth :
    ∀ (y : Ω) (a : H),
      ContDiffOn ℝ (↑⊤)
        (fun ω => G y (ω • a)) U)
  (hunif :
    ∀ (k : ℕ),
      ∃ h,
        ∫⁻ (a : H),
              ENNReal.ofReal
                  ((1 + ‖a‖) ^ (k + 2)) *
                ↑(h a) ∂ν <
            ⊤ ∧
          ∀ (y : Ω) (a : H),
            OperatorRidgelet.rayDerivBound
                U (G y) k a ≤
              ↑(h a)) :
  OperatorRidgelet.IsRegularAlongRays ν I
    fun ξ => ∫ (y : Ω), G y ξ ∂m

**Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Bochner
integrals `∫ G_y m(dy)` of a measurable family of densities that are regular along rays, over
a finite measure `m`, are regular along rays when the densities are uniformly bounded and the
weights of `eq:ray-regularity` have a `ν_α`-integrable majorant that is uniform in `y`.

Proof for Lemma 5.2.2

uses 0

For (a), domination of the linear functionals gives |q(\xi)|\le C(1+\kappa(\xi))^p, so G is bounded. Ray derivatives are polynomials times e^{-\omega^2\kappa(a)/2}; on I\subset\{r\le|\omega|\le R\} their bound is C_k(1+\|a\|)^{p_k}e^{-r^2\theta\langle Qa,a\rangle/2}. Apply Lemma 2.3.3. For (b), derivatives vanish outside a bounded set of directions, on which \nu_\alpha is finite. For (c), the finite neighbourhood bounds justify differentiation under the Bochner integral for each direction. The triangle inequality and Tonelli give M_m(G)\le m(\Omega)\int_H(1+\|a\|)^{m+2}\max_{k\le m}h_k(a)\,\nu_\alpha(\mathrm da)<\infty.