6.3. Finite variation and moments from a spectral density🔗

Theorem6.6

Statement uses 4

Statement dependency previews

Preview

Definition 3.7

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Example 5.6

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 satisfy Definition 4.2. 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 Theorem6.6●5 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_6_6_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_6_6_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:6.6]** Finite total variation and moments of the coefficient measure.  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_6_6_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_6_6_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:6.6]** Finite total variation and moments of the coefficient measure.  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_6_6_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_6_6_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:6.6]** Finite total variation and moments of the coefficient measure.
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_6_6_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_6_6_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:6.6]** Finite total variation and moments of the coefficient measure.  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_6_6_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_6_6_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:6.6]** All parameter moments are bounded, also for vector-valued densities.

Proof for Theorem 6.6

Proof uses 4

Proof dependency previews

Preview

Lemma 3.2

Loading preview

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

Apply Lemma 4.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 4.5 (iii) and Theorem 6.5 for synthesis and sampling.