6.2. A Gaussian target with a closed-form transform🔗

Proposition6.2.1

Statement uses 9

Statement dependency previews

Preview

Lemma 2.1.3

Loading preview

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

used by 1✓L∃∀N

Let W be bounded, positive, injective, self-adjoint with M=Q^{1/2}WQ^{1/2} trace class, f_W(x)=e^{-\langle Wx,x\rangle/2}, D=\det(I+M), and \kappa_W(\xi)=\langle Q^{1/2}(I+M)^{-1}Q^{1/2}\xi,\xi\rangle. For every \alpha>0 and band-pass \rho: (i) \mathcal G_Qf_W(\xi)=D^{-1/2}e^{-\kappa_W(\xi)/2} and R_\rho f_W(a,c)=D^{-1/2}(\rho*\phi_{\kappa_W(a)})(c), so f_W\in\mathcal D_\alpha, and f_W is not cylindrical when W has infinite rank. (ii) G=\mathcal G_Qf_W is regular along rays and T_\alpha f_W is represented by g_G(x)=D^{-1/2}\int_0^\infty\det(I+2sP^{1/2}S_WP^{1/2})^{-1/2}\exp(-\tfrac12\langle\Sigma_sx,x\rangle)\,s^{\alpha/2-1}\,\mathrm ds. (iii) For every real, globally Lipschitz, non-polynomial \beta, the coefficient R_\rho f_W=\gamma_G has finite variation and second moment, S_\beta[R_\rho f_W\lambda_\alpha]=C_{\beta,\rho}^{(\alpha)}g_G, and its sampled network converges at the rate N^{-1/2} in C(K).

Lean code for Proposition6.2.1●11 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_i_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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) (ξ : H) :
  OperatorRidgelet.gaussFourier μ (OperatorRidgelet.gaussianTarget W)
      ξ =
    ↑(√(OperatorRidgelet.fredholmDet (S * W * S)))⁻¹ *
      Complex.exp (-↑(OperatorRidgelet.gaussianKappa S W ξ / 2))

theorem OperatorRidgelet.Paper.ex_closed_form_i_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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (ξ : H) :
  OperatorRidgelet.gaussFourier μ
      (OperatorRidgelet.gaussianTarget W)
      ξ =
    ↑(√(OperatorRidgelet.fredholmDet
              (S * W * S)))⁻¹ *
      Complex.exp
        (-↑(OperatorRidgelet.gaussianKappa
                S W ξ /
              2))

**Example [ex:closed-form]** Closed-form transform and its filtered network.  For `W` bounded,
positive, injective, self-adjoint with `M = Q^{1/2} W Q^{1/2}` trace class,
`𝒢_Q f_W(ξ) = D^{-1/2} e^{-κ_W(ξ)/2}` with `D = det(I+M)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_i_b.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) (p : H × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ) (OperatorRidgelet.gaussianTarget W)
      p =
    ↑((√(OperatorRidgelet.fredholmDet (S * W * S)))⁻¹ *
        OperatorRidgelet.gaussianSmooth (⇑ρ)
          (OperatorRidgelet.gaussianKappa S W p.1) p.2)

theorem OperatorRidgelet.Paper.ex_closed_form_i_b.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (p : H × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.gaussianTarget W)
      p =
    ↑((√(OperatorRidgelet.fredholmDet
              (S * W * S)))⁻¹ *
        OperatorRidgelet.gaussianSmooth
          (⇑ρ)
          (OperatorRidgelet.gaussianKappa
            S W p.1)
          p.2)

**Example [ex:closed-form]** Closed-form transform and its filtered network.  For every
band-pass `ρ`, `R_ρ f_W(a,c) = D^{-1/2} (ρ * φ_{κ_W(a)})(c)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_i_c.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) :
  OperatorRidgelet.MemSpectralCore μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.gaussianTarget W)

theorem OperatorRidgelet.Paper.ex_closed_form_i_c.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S)) :
  OperatorRidgelet.MemSpectralCore μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.gaussianTarget W)

**Example [ex:closed-form]** Closed-form transform and its filtered network.  In particular
`f_W ∈ 𝒟_α` for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_i_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (W : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x) (hWi : Function.Injective ⇑W)
  (hrank : OperatorRidgelet.HasInfiniteRank ↑W) :
  ¬OperatorRidgelet.IsCylindrical (OperatorRidgelet.gaussianTarget W)

theorem OperatorRidgelet.Paper.ex_closed_form_i_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (W : H →L[ℝ] H)
  (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hrank :
    OperatorRidgelet.HasInfiniteRank ↑W) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.gaussianTarget W)

**Example [ex:closed-form]** Closed-form transform and its filtered network.  `f_W` is not
cylindrical when `W` has infinite rank.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_ii_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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N α) I
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget W))

theorem OperatorRidgelet.Paper.ex_closed_form_ii_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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ)
      I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N
        α)
      I
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget
          W))

**Example [ex:closed-form]** Closed-form transform and its filtered network.  For every
band-pass `ρ`, the density `G = 𝒢_Q f_W` is regular along rays.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_ii_b.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (fW :
    ↥(OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture N α))) :
  ↑↑↑fW =ᵐ[μ] OperatorRidgelet.gaussianTarget W →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      (OperatorRidgelet.frameOperator μ
            (OperatorRidgelet.gaussianMixture N α)
            (OperatorRidgelet.spectralEmbed μ
              (OperatorRidgelet.gaussianMixture N α) fW))
          (OperatorRidgelet.spectralEmbed μ
            (OperatorRidgelet.gaussianMixture N α) g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture N α)
              (OperatorRidgelet.gaussFourier μ
                (OperatorRidgelet.gaussianTarget W))
              x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ

theorem OperatorRidgelet.Paper.ex_closed_form_ii_b.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (fW :
    ↥(OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture
          N α))) :
  ↑↑↑fW =ᵐ[μ]
      OperatorRidgelet.gaussianTarget W →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      (OperatorRidgelet.frameOperator μ
            (OperatorRidgelet.gaussianMixture
              N α)
            (OperatorRidgelet.spectralEmbed
              μ
              (OperatorRidgelet.gaussianMixture
                N α)
              fW))
          (OperatorRidgelet.spectralEmbed
            μ
            (OperatorRidgelet.gaussianMixture
              N α)
            g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture
                N α)
              (OperatorRidgelet.gaussFourier
                μ
                (OperatorRidgelet.gaussianTarget
                  W))
              x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ

**Example [ex:closed-form]** Closed-form transform and its filtered network.  The image
`T_α f_W` is represented by the bounded continuous function `g_G`, `G = 𝒢_Q f_W`:
`T_α f_W [g] = ∫ g_G(x) conj(g(x)) μ_Q(dx)` for `g ∈ 𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_ii_c.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S R : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (hR : OperatorRidgelet.IsPositiveSqrt R P) (x : H) :
  OperatorRidgelet.spectralTarget (OperatorRidgelet.gaussianMixture N α)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget W))
      x =
    ↑(√(OperatorRidgelet.fredholmDet (S * W * S)))⁻¹ *
      ∫ (s : ℝ) in Set.Ioi 0,
        ↑((√(OperatorRidgelet.fredholmDet
                    ((2 * s) •
                      (R *
                          OperatorRidgelet.gaussianTargetResolvent S W *
                        R))))⁻¹ *
              Real.exp
                (-inner ℝ
                      ((OperatorRidgelet.mixtureLayerCovariance R
                          (OperatorRidgelet.gaussianTargetResolvent S W)
                          s)
                        x)
                      x /
                  2) *
            s ^ (α / 2 - 1))

theorem OperatorRidgelet.Paper.ex_closed_form_ii_c.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S R : H →L[ℝ] H)
  (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (hR :
    OperatorRidgelet.IsPositiveSqrt R P)
  (x : H) :
  OperatorRidgelet.spectralTarget
      (OperatorRidgelet.gaussianMixture N
        α)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget
          W))
      x =
    ↑(√(OperatorRidgelet.fredholmDet
              (S * W * S)))⁻¹ *
      ∫ (s : ℝ) in Set.Ioi 0,
        ↑((√(OperatorRidgelet.fredholmDet
                    ((2 * s) •
                      (R *
                          OperatorRidgelet.gaussianTargetResolvent
                            S W *
                        R))))⁻¹ *
              Real.exp
                (-inner ℝ
                      ((OperatorRidgelet.mixtureLayerCovariance
                          R
                          (OperatorRidgelet.gaussianTargetResolvent
                            S W)
                          s)
                        x)
                      x /
                  2) *
            s ^ (α / 2 - 1))

**Example [ex:closed-form]** Closed-form transform and its filtered network.  With
`S_W = Q^{1/2}(I+M)⁻¹Q^{1/2}`, `R = P^{1/2}`, and
`Σ_s = 2s P^{1/2}(I + 2s P^{1/2} S_W P^{1/2})⁻¹ P^{1/2}`, the representing function is
`g_G(x) = D^{-1/2} ∫₀^∞ det(I + 2s P^{1/2} S_W P^{1/2})^{-1/2} exp(-½⟨Σ_s x,x⟩) s^{α/2-1} ds`
(`eq:filtered-gaussian-target`).

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_iii_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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) :
  OperatorRidgelet.ridgelet μ (⇑ρ) (OperatorRidgelet.gaussianTarget W) =
    OperatorRidgelet.coefficientFormula (⇑ρ)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget W))

theorem OperatorRidgelet.Paper.ex_closed_form_iii_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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S)) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.gaussianTarget
        W) =
    OperatorRidgelet.coefficientFormula
      (⇑ρ)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget
          W))

**Example [ex:closed-form]** Closed-form transform and its filtered network.  The ridgelet
coefficient of `f_W` is the coefficient `γ_G` of its density `G = 𝒢_Q f_W`:
`R_ρ f_W = γ_G`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_iii_b.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.gaussianTarget W) p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N α))

theorem OperatorRidgelet.Paper.ex_closed_form_iii_b.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S)) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.gaussianTarget
              W)
            p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N
        α))

**Example [ex:closed-form]** Closed-form transform and its filtered network.  The ridgelet
coefficient `R_ρ f_W` has finite variation and second moment:
`∫ (1 + ‖a‖² + |c|²) |R_ρ f_W(a,c)| λ_α(da,dc) < ∞`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_iii_c.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) {L : NNReal}
  (hb : LipschitzWith L b) (hbp : ¬OperatorRidgelet.IsPolynomialFun b) :
  OperatorRidgelet.integralNetworkDensity (fun t => ↑(b t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture N α))
      (OperatorRidgelet.ridgelet μ (⇑ρ)
        (OperatorRidgelet.gaussianTarget W)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst α β ρ *
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture N α)
        (OperatorRidgelet.gaussFourier μ
          (OperatorRidgelet.gaussianTarget W))
        x

theorem OperatorRidgelet.Paper.ex_closed_form_iii_c.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  {L : NNReal} (hb : LipschitzWith L b)
  (hbp :
    ¬OperatorRidgelet.IsPolynomialFun b) :
  OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(b t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture
          N α))
      (OperatorRidgelet.ridgelet μ (⇑ρ)
        (OperatorRidgelet.gaussianTarget
          W)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ *
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture
          N α)
        (OperatorRidgelet.gaussFourier μ
          (OperatorRidgelet.gaussianTarget
            W))
        x

**Example [ex:closed-form]** Closed-form transform and its filtered network.  For every
real, globally Lipschitz, non-polynomial `β` (including ReLU), the integral network
`S_β[R_ρ f_W λ_α]` equals `C^{(α)}_{β,ρ} g_G`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_closed_form_iii_d.{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 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) {L : NNReal}
  (hb : LipschitzWith L b) (hbp : ¬OperatorRidgelet.IsPolynomialFun b)
  (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.gaussianMixture N α))
            (OperatorRidgelet.ridgelet μ (⇑ρ)
              (OperatorRidgelet.gaussianTarget W))
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst α β ρ *
            OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture N α)
              (OperatorRidgelet.gaussFourier μ
                (OperatorRidgelet.gaussianTarget W))
              x ∂OperatorRidgelet.sampleLaw n
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture N α))
          (OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.gaussianTarget W))) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture N α))
            (OperatorRidgelet.ridgelet μ (⇑ρ)
              (OperatorRidgelet.gaussianTarget W)) /
        √↑n *
      (|b 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  (OperatorRidgelet.gaussianMixture N α))
                (OperatorRidgelet.ridgelet μ (⇑ρ)
                  (OperatorRidgelet.gaussianTarget W)))))

theorem OperatorRidgelet.Paper.ex_closed_form_iii_d.{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 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  {L : NNReal} (hb : LipschitzWith L b)
  (hbp :
    ¬OperatorRidgelet.IsPolynomialFun b)
  (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.gaussianMixture
                N α))
            (OperatorRidgelet.ridgelet μ
              (⇑ρ)
              (OperatorRidgelet.gaussianTarget
                W))
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst
              α β ρ *
            OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture
                N α)
              (OperatorRidgelet.gaussFourier
                μ
                (OperatorRidgelet.gaussianTarget
                  W))
              x ∂OperatorRidgelet.sampleLaw
        n
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture
              N α))
          (OperatorRidgelet.ridgelet μ
            (⇑ρ)
            (OperatorRidgelet.gaussianTarget
              W))) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture
                N α))
            (OperatorRidgelet.ridgelet μ
              (⇑ρ)
              (OperatorRidgelet.gaussianTarget
                W)) /
        √↑n *
      (|b 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  (OperatorRidgelet.gaussianMixture
                    N α))
                (OperatorRidgelet.ridgelet
                  μ (⇑ρ)
                  (OperatorRidgelet.gaussianTarget
                    W)))))

**Example [ex:closed-form]** Closed-form transform and its filtered network.  For every
real, globally Lipschitz, non-polynomial `β`, the sampled network `eq:polar-network` of
`R_ρ f_W λ_α` (with `V = ‖R_ρ f_W‖_{L¹(λ_α)}` and samples from `p = |R_ρ f_W| λ_α / V`, as in
Theorem `thm:E`(iv)) converges to `C^{(α)}_{β,ρ} g_G` at the rate `n^{-1/2}` in `C(K)`, as in
`eq:spectral-barron`: `E‖f_n - C g_G‖_{C(K)} ≤ 8V n^{-1/2} (|β(0)| + Lip(β) R_K M₂)`.

Proof for Proposition 6.2.1

uses 0

Lemma 6.1.4 with \Sigma=Q, S=W gives \mathcal G_Qf_W, Fourier inversion in the bias gives the convolution, (I+M)^{-1}\ge(1+\|M\|)^{-1}I gives the decay needed by Lemma 2.3.3, and f_W(x)<1=f_W(0) for x\ne0 in the kernel of a finite-rank map. Part (ii) is Theorem 3.2.7 (iii) with the Gaussian integral applied on each layer of \nu_\alpha; part (iii) is Lemma 5.2.2 (a) with S_W\ge(1+\|M\|)^{-1}Q followed by Theorem 5.2.1.