6.4. Constructive universal approximation🔗

Lemma6.7

Statement uses 3

Statement dependency previews

Preview

Definition 2.2

Loading preview

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

used by 1✓L∃∀N

Let \beta:\mathbb R\to\mathbb C be continuous, K\subset H compact, and \int\|\beta(\langle a,\cdot\rangle+c)\|_{C(K)}\,\mathrm d|\Gamma|(a,c)<\infty. Then for every \varepsilon>0 there is a finite atomic complex measure \Gamma_\varepsilon with \|S_\beta\Gamma_\varepsilon-S_\beta\Gamma\|_{C(K)}<\varepsilon.

Lean code for Lemma6.7●1 theorem

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.lem_6_7.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {β : ℝ → ℂ} (hβ : Continuous β)
  (Γ : MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γ)]
  {K : Set H} (hK : IsCompact K)
  (hint :
    MeasureTheory.Integrable
      (fun θ =>
        OperatorRidgelet.compactSupNorm K fun x =>
          β (inner ℝ θ.1 x + θ.2))
      (MeasureTheory.VectorMeasure.variation Γ))
  {ε : ℝ} (hε : 0 < ε) :
  ∃ n w θ,
    (OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.integralNetwork β
            (OperatorRidgelet.atomicMeasure w θ) x -
          OperatorRidgelet.integralNetwork β Γ x) <
      ε

theorem OperatorRidgelet.Paper.lem_6_7.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℂ} (hβ : Continuous β)
  (Γ :
    MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γ)]
  {K : Set H} (hK : IsCompact K)
  (hint :
    MeasureTheory.Integrable
      (fun θ =>
        OperatorRidgelet.compactSupNorm K
          fun x =>
          β (inner ℝ θ.1 x + θ.2))
      (MeasureTheory.VectorMeasure.variation
        Γ))
  {ε : ℝ} (hε : 0 < ε) :
  ∃ n w θ,
    (OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.integralNetwork β
            (OperatorRidgelet.atomicMeasure
              w θ)
            x -
          OperatorRidgelet.integralNetwork
            β Γ x) <
      ε

**Lemma [lem:6.7]** Qualitative finite-atomic approximation.  For
continuous `β`, compact `K`, and `∫ ‖β(⟪a,·⟫ + c)‖_{C(K)} d|Γ| < ∞`, for every `ε > 0` there
is a finite atomic complex measure `Γ_ε = ∑_j w_j δ_{θ_j}` with
`‖S_β Γ_ε − S_β Γ‖_{C(K)} < ε`.

Proof for Lemma 6.7

uses 0

The atom map is continuous into the separable Banach space C(K), so Y(a,c)=h(a,c)\beta(\langle a,\cdot\rangle+c)|_K is Bochner integrable and its mean lies in the closed convex hull of its essential range by Hahn–Banach separation; approximate the mean by a finite convex combination of essential-range values.

Theorem6.8

Statement uses 4

Statement dependency previews

Preview

Definition 2.1

Loading preview

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

used by 0✓L∃∀N

Let \beta:\mathbb R\to\mathbb R be continuous, of polynomial growth, and not a polynomial, let \rho be a band-pass filter with C_{\beta,\rho}^{(\alpha)}=1, let f:H\to\mathbb C be continuous, K\subset H compact, and \varepsilon>0. The direction measure has full support and is finite on bounded sets; these properties hold for \nu_\alpha and are required for general input and direction measures. Then there is a spectral density G satisfying Definition 4.2, smooth and vanishing outside a bounded set, such that (i) \|f-g_G\|_{C(K)}<\varepsilon; (ii) g_G=S_\beta[\gamma_G\lambda_\alpha] is an integral network whose coefficient measure is finite with finite moments of all orders; (iii) if \beta is globally Lipschitz, the sampled network f_N of \gamma_G\lambda_\alpha satisfies \mathbb E\|f-f_N\|_{C(K)}\le\varepsilon+\frac{8V}{\sqrt N}(|\beta(0)|+\operatorname{Lip}(\beta)R_KM_2), and one deterministic width-N network satisfies the same bound. In particular the finite-width networks with activation \beta are dense in C(H) for the compact-open topology, and the same statements hold for continuous f:H\to Y with C(K;Y) norms and the same explicit rate in (iii), by the Hilbert-valued Theorem 6.5.

Lean code for Theorem6.8●3 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_6_8.{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 α ν)
  (hfin : ∀ (R : ℝ), ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b)
  (hpoly : ¬OperatorRidgelet.IsPolynomialFun b) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ = 1)
  (I : Set ℝ) (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  {f : H → ℂ} (hf : Continuous f) {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ G,
    OperatorRidgelet.IsRegularAlongRays ν I G ∧
      ContDiff ℝ (↑⊤) G ∧
        (∃ R, ∀ (ξ : H), R < ‖ξ‖ → G ξ = 0) ∧
          (OperatorRidgelet.compactSupNorm K fun x =>
                f x - OperatorRidgelet.spectralTarget ν G x) <
              ε ∧
            OperatorRidgelet.spectralTarget ν G =
                OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(b t))
                  (OperatorRidgelet.parameterMeasure ν)
                  (OperatorRidgelet.coefficientFormula (⇑ρ) G) ∧
              (∀ (m : ℕ),
                  MeasureTheory.Integrable
                    (fun θ =>
                      (1 + ‖θ.1‖ + |θ.2|) ^ m *
                        ‖OperatorRidgelet.coefficientFormula (⇑ρ) G θ‖)
                    (OperatorRidgelet.parameterMeasure ν)) ∧
                ∀ (L : NNReal),
                  LipschitzWith L b →
                    ∀ (N : ℕ),
                      0 < N →
                        ∫ (θ : Fin N → H × ℝ),
                              OperatorRidgelet.compactSupNorm K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun t => ↑(b t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormula
                                      (⇑ρ) 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)))) ∧
                          ∃ θ,
                            (OperatorRidgelet.compactSupNorm K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun t => ↑(b t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormula
                                      (⇑ρ) G)
                                    θ x) ≤
                              ε +
                                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_6_8.{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 α ν)
  (hfin :
    ∀ (R : ℝ),
      ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialFun b)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ =
      1)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  {f : H → ℂ} (hf : Continuous f)
  {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ G,
    OperatorRidgelet.IsRegularAlongRays ν
        I G ∧
      ContDiff ℝ (↑⊤) G ∧
        (∃ R,
            ∀ (ξ : H),
              R < ‖ξ‖ → G ξ = 0) ∧
          (OperatorRidgelet.compactSupNorm
                K fun x =>
                f x -
                  OperatorRidgelet.spectralTarget
                    ν G x) <
              ε ∧
            OperatorRidgelet.spectralTarget
                  ν G =
                OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(b t))
                  (OperatorRidgelet.parameterMeasure
                    ν)
                  (OperatorRidgelet.coefficientFormula
                    (⇑ρ) G) ∧
              (∀ (m : ℕ),
                  MeasureTheory.Integrable
                    (fun θ =>
                      (1 + ‖θ.1‖ +
                            |θ.2|) ^
                          m *
                        ‖OperatorRidgelet.coefficientFormula
                            (⇑ρ) G θ‖)
                    (OperatorRidgelet.parameterMeasure
                      ν)) ∧
                ∀ (L : NNReal),
                  LipschitzWith L b →
                    ∀ (N : ℕ),
                      0 < N →
                        ∫ (θ :
                              Fin N →
                                H × ℝ),
                              OperatorRidgelet.compactSupNorm
                                K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun
                                        t =>
                                      ↑(b
                                          t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormula
                                      (⇑ρ)
                                      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)))) ∧
                          ∃ θ,
                            (OperatorRidgelet.compactSupNorm
                                K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun
                                        t =>
                                      ↑(b
                                          t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormula
                                      (⇑ρ)
                                      G)
                                    θ x) ≤
                              ε +
                                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:6.8]** Constructive universal approximation with approximation rates.  For a
continuous,
polynomially growing, non-polynomial real `β` (the function `b` of the tempered `β`), a
band-pass `ρ` with `C^{(α)}_{β,ρ} = 1`, a continuous `f : H → ℂ`, a compact `K`, and `ε > 0`,
there is a spectral density `G`, regular along rays, smooth, and vanishing outside a bounded
set, such that (i) `‖f − g_G‖_{C(K)} < ε`; (ii) `g_G = S_β[γ_G λ_α]` with a coefficient
measure `γ_G λ_α` that is finite with finite moments of all orders; (iii) if `β` is globally
Lipschitz, the sampled network of `γ_G λ_α` satisfies
`𝔼‖f − f_N‖_{C(K)} ≤ ε + (8V/√N)(|β(0)| + Lip(β) R_K M₂)` with `V = ‖γ_G‖_{L¹(λ_α)}` and
`M₂` the second moment of `|γ_G| λ_α / V`, and at least one deterministic width-`N` network
satisfies the same bound.  The direction measure is assumed finite on bounded sets (`hfin`),
which Lemma `lem:3.2` supplies for the Gaussian mixture `ν_α` in infinite
dimension and which the manuscript uses throughout, since it states the theorem for `ν_α`
only; the abstract hypotheses (σ-finite, full support, homogeneous of degree `α > 0`) do not
imply it, so `hfin` is retained explicitly in the Lean statement.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_6_8_dense.{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 α ν)
  (hfin : ∀ (R : ℝ), ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b)
  (hpoly : ¬OperatorRidgelet.IsPolynomialFun b) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ = 1)
  (I : Set ℝ) (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  {f : H → ℂ} (hf : Continuous f) {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ N v a c,
    (OperatorRidgelet.compactSupNorm K fun x =>
        f x -
          OperatorRidgelet.finiteNetwork (fun t => ↑(b t)) v a c x) <
      ε

theorem OperatorRidgelet.Paper.thm_6_8_dense.{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 α ν)
  (hfin :
    ∀ (R : ℝ),
      ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialFun b)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ =
      1)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  {f : H → ℂ} (hf : Continuous f)
  {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ N v a c,
    (OperatorRidgelet.compactSupNorm K
        fun x =>
        f x -
          OperatorRidgelet.finiteNetwork
            (fun t => ↑(b t)) v a c x) <
      ε

**Theorem [thm:6.8]** Constructive universal approximation with approximation rates.
In particular, under the hypotheses of the theorem, the finite-width networks with the continuous,
polynomially
growing, non-polynomial real activation `β` are dense in `C(H)` for the compact-open topology:
every continuous `f : H → ℂ` is approximated within `ε` on every compact `K` by a network of
some finite width `N`.  The manuscript states the sentence inside Theorem `thm:6.8`, under all
of its hypotheses, and derives it from (ii) together with Lemma `lem:6.7`
(from (iii) when `β` is in addition globally Lipschitz); the Lean statement therefore carries
the hypotheses of `thm_6_8`, including `hfin`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_6_8_vec.{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) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (hfin : ∀ (R : ℝ), ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b)
  (hpoly : ¬OperatorRidgelet.IsPolynomialFun b) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ = 1)
  (I : Set ℝ) (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  {f : H → Y} (hf : Continuous f) {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ G,
    OperatorRidgelet.IsRegularAlongRays ν I G ∧
      ContDiff ℝ (↑⊤) G ∧
        (∃ R, ∀ (ξ : H), R < ‖ξ‖ → G ξ = 0) ∧
          (OperatorRidgelet.compactSupNorm K fun x =>
                f x - OperatorRidgelet.spectralTarget ν G x) <
              ε ∧
            OperatorRidgelet.spectralTarget ν G =
                OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(b t))
                  (OperatorRidgelet.parameterMeasure ν)
                  (OperatorRidgelet.coefficientFormulaVec (⇑ρ) G) ∧
              (∀ (m : ℕ),
                  MeasureTheory.Integrable
                    (fun θ =>
                      (1 + ‖θ.1‖ + |θ.2|) ^ m *
                        ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
                            θ‖)
                    (OperatorRidgelet.parameterMeasure ν)) ∧
                ∀ (L : NNReal),
                  LipschitzWith L b →
                    ∀ (N : ℕ),
                      0 < N →
                        ∫ (θ : Fin N → H × ℝ),
                              OperatorRidgelet.compactSupNorm K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun t => ↑(b t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormulaVec
                                      (⇑ρ) G)
                                    θ
                                    x ∂OperatorRidgelet.sampleLaw N
                                (OperatorRidgelet.densityLaw
                                  (OperatorRidgelet.parameterMeasure ν)
                                  (OperatorRidgelet.coefficientFormulaVec
                                    (⇑ρ) G)) ≤
                            ε +
                              8 *
                                    OperatorRidgelet.densityWeight
                                      (OperatorRidgelet.parameterMeasure
                                        ν)
                                      (OperatorRidgelet.coefficientFormulaVec
                                        (⇑ρ) G) /
                                  √↑N *
                                (|b 0| +
                                  ↑L *
                                      OperatorRidgelet.compactRadius K *
                                    √(OperatorRidgelet.secondMoment
                                        (OperatorRidgelet.densityLaw
                                          (OperatorRidgelet.parameterMeasure
                                            ν)
                                          (OperatorRidgelet.coefficientFormulaVec
                                            (⇑ρ) G)))) ∧
                          ∃ θ,
                            (OperatorRidgelet.compactSupNorm K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun t => ↑(b t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormulaVec
                                      (⇑ρ) G)
                                    θ x) ≤
                              ε +
                                8 *
                                      OperatorRidgelet.densityWeight
                                        (OperatorRidgelet.parameterMeasure
                                          ν)
                                        (OperatorRidgelet.coefficientFormulaVec
                                          (⇑ρ) G) /
                                    √↑N *
                                  (|b 0| +
                                    ↑L *
                                        OperatorRidgelet.compactRadius
                                          K *
                                      √(OperatorRidgelet.secondMoment
                                          (OperatorRidgelet.densityLaw
                                            (OperatorRidgelet.parameterMeasure
                                              ν)
                                            (OperatorRidgelet.coefficientFormulaVec
                                              (⇑ρ) G))))

theorem OperatorRidgelet.Paper.thm_6_8_vec.{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)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (hfin :
    ∀ (R : ℝ),
      ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialFun b)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ =
      1)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  {f : H → Y} (hf : Continuous f)
  {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ G,
    OperatorRidgelet.IsRegularAlongRays ν
        I G ∧
      ContDiff ℝ (↑⊤) G ∧
        (∃ R,
            ∀ (ξ : H),
              R < ‖ξ‖ → G ξ = 0) ∧
          (OperatorRidgelet.compactSupNorm
                K fun x =>
                f x -
                  OperatorRidgelet.spectralTarget
                    ν G x) <
              ε ∧
            OperatorRidgelet.spectralTarget
                  ν G =
                OperatorRidgelet.integralNetworkDensity
                  (fun t => ↑(b t))
                  (OperatorRidgelet.parameterMeasure
                    ν)
                  (OperatorRidgelet.coefficientFormulaVec
                    (⇑ρ) G) ∧
              (∀ (m : ℕ),
                  MeasureTheory.Integrable
                    (fun θ =>
                      (1 + ‖θ.1‖ +
                            |θ.2|) ^
                          m *
                        ‖OperatorRidgelet.coefficientFormulaVec
                            (⇑ρ) G θ‖)
                    (OperatorRidgelet.parameterMeasure
                      ν)) ∧
                ∀ (L : NNReal),
                  LipschitzWith L b →
                    ∀ (N : ℕ),
                      0 < N →
                        ∫ (θ :
                              Fin N →
                                H × ℝ),
                              OperatorRidgelet.compactSupNorm
                                K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun
                                        t =>
                                      ↑(b
                                          t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormulaVec
                                      (⇑ρ)
                                      G)
                                    θ
                                    x ∂OperatorRidgelet.sampleLaw
                                N
                                (OperatorRidgelet.densityLaw
                                  (OperatorRidgelet.parameterMeasure
                                    ν)
                                  (OperatorRidgelet.coefficientFormulaVec
                                    (⇑ρ)
                                    G)) ≤
                            ε +
                              8 *
                                    OperatorRidgelet.densityWeight
                                      (OperatorRidgelet.parameterMeasure
                                        ν)
                                      (OperatorRidgelet.coefficientFormulaVec
                                        (⇑ρ)
                                        G) /
                                  √↑N *
                                (|b 0| +
                                  ↑L *
                                      OperatorRidgelet.compactRadius
                                        K *
                                    √(OperatorRidgelet.secondMoment
                                        (OperatorRidgelet.densityLaw
                                          (OperatorRidgelet.parameterMeasure
                                            ν)
                                          (OperatorRidgelet.coefficientFormulaVec
                                            (⇑ρ)
                                            G)))) ∧
                          ∃ θ,
                            (OperatorRidgelet.compactSupNorm
                                K fun x =>
                                f x -
                                  OperatorRidgelet.densitySampledNetwork
                                    (fun
                                        t =>
                                      ↑(b
                                          t))
                                    (OperatorRidgelet.parameterMeasure
                                      ν)
                                    (OperatorRidgelet.coefficientFormulaVec
                                      (⇑ρ)
                                      G)
                                    θ x) ≤
                              ε +
                                8 *
                                      OperatorRidgelet.densityWeight
                                        (OperatorRidgelet.parameterMeasure
                                          ν)
                                        (OperatorRidgelet.coefficientFormulaVec
                                          (⇑ρ)
                                          G) /
                                    √↑N *
                                  (|b 0| +
                                    ↑L *
                                        OperatorRidgelet.compactRadius
                                          K *
                                      √(OperatorRidgelet.secondMoment
                                          (OperatorRidgelet.densityLaw
                                            (OperatorRidgelet.parameterMeasure
                                              ν)
                                            (OperatorRidgelet.coefficientFormulaVec
                                              (⇑ρ)
                                              G))))

**Theorem [thm:6.8]** Constructive universal approximation with approximation rates.  The same
statements
hold for continuous `f : H → Y` with values in a separable complex Hilbert space: there is a
`Y`-valued spectral density `G`, regular along rays, smooth, and vanishing outside a bounded
set, with (i) `‖f − g_G‖_{C(K;Y)} < ε`, (ii) `g_G = S_β[γ_G λ_α]` with a finite coefficient
measure with finite moments of all orders, and (iii), for globally Lipschitz `β`, the same
explicit rate `𝔼‖f − f_N‖_{C(K;Y)} ≤ ε + (8V/√N)(|β(0)| + Lip(β) R_K M₂)` as in the scalar
case, by the Hilbert-valued Theorem `thm:6.5`, together with a deterministic
width-`N` realization.  As in `thm_6_8`, the direction measure is assumed finite on bounded sets
(`hfin`).

Proof for Theorem 6.8

Proof uses 6

Proof dependency previews

Preview

Lemma 4.4

Loading preview

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

Finite sums of characters e^{i\langle x,\xi\rangle} form a self-conjugate algebra containing the constants and separating points, so Stone–Weierstrass gives a trigonometric approximant on K; each character is within r_K\delta of g_{G_j} for a normalized smooth bump G_j supported in the ball of radius \delta around \xi_j. Full support makes its normalizing integral positive, and finiteness on bounded sets makes it finite. By Lemma 4.4, the sum G=\sum_jw_jG_j satisfies Definition 4.2. Then Theorem 4.5 (iii), Theorem 6.6, and Theorem 6.5 give (ii) and (iii); the vector-valued case uses a partition of unity and Theorem 4.11.