5.3. Constructive universal approximation
Theorem5.3.1
used by 0✓L∃∀N
Associated Lean declarations
-
OperatorRidgelet.Paper.thm_D[complete] -
OperatorRidgelet.Paper.thm_D_dense[complete] -
OperatorRidgelet.Paper.thm_D_vec[complete]
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 in the abstract-weight version. Then there is a spectral density
G, regular along rays, 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 5.1.6.
Lean code for Theorem5.3.1●3 theorems
Associated Lean declarations
-
OperatorRidgelet.Paper.thm_D[complete]
-
OperatorRidgelet.Paper.thm_D_dense[complete]
-
OperatorRidgelet.Paper.thm_D_vec[complete]
Associated Lean declarations
-
OperatorRidgelet.Paper.thm_D[complete] -
OperatorRidgelet.Paper.thm_D_dense[complete] -
OperatorRidgelet.Paper.thm_D_vec[complete]
-
theoremdefined in OperatorRidgelet/Paper/Sampling.leancomplete
theorem OperatorRidgelet.Paper.thm_D.{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_D.{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:D]** Constructive universal approximation with 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:homogeneous-mixture` 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, and Theorem `thm:general-weights` deliberately does not extend `thm:D` to abstract weights. -
theoremdefined in OperatorRidgelet/Paper/Sampling.leancomplete
theorem OperatorRidgelet.Paper.thm_D_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_D_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:D]** Constructive universal approximation with 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:D`, under all of its hypotheses, and derives it from (ii) together with Lemma `lem:qualitative-sampling` (from (iii) when `β` is in addition globally Lipschitz); the Lean statement therefore carries the hypotheses of `thm_D`, including `hfin`.
-
theoremdefined in OperatorRidgelet/Paper/Sampling.leancomplete
theorem OperatorRidgelet.Paper.thm_D_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_D_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:D]** Constructive universal approximation with 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:lipschitz-barron`, together with a deterministic width-`N` realization. As in `thm_D`, the direction measure is assumed finite on bounded sets (`hfin`).
Proof for Theorem 5.3.1
uses 0
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. The sum G=\sum_jw_jG_j is regular along rays by
Lemma 5.2.2, and Theorem 3.1.5 (iii), Theorem 5.2.1, and
Theorem 5.1.6 give (ii) and (iii); the vector-valued case uses a partition
of unity and Theorem 3.3.2.