Appendix A. A kernel interpretation of the frame operator🔗

This appendix computes a regularized characteristic functional of the infinite Gaussian mixture and explains a formal kernel interpretation of the frame operator. These optional observations are not prerequisites for the main proofs.

LemmaA.1

uses 1used by 0✓L∃∀N

For z\ne0 put q=\langle Pz,z\rangle>0 (i) and \nu_\alpha^{\varepsilon,M}=\int_\varepsilon^M\mathcal N(0,2sP)s^{\alpha/2-1}\mathrm ds. Then \lim_{\varepsilon\downarrow0,M\uparrow\infty}\int_He^{i\langle z,\xi\rangle}\,\nu_\alpha^{\varepsilon,M}(\mathrm d\xi)=\Gamma(\alpha/2)q^{-\alpha/2} (ii), where \int_0^\infty e^{-sq}s^{\alpha/2-1}\mathrm ds=\Gamma(\alpha/2)q^{-\alpha/2} (iii). In contrast \int_H|e^{i\langle z,\xi\rangle}|\,\nu_\alpha(\mathrm d\xi)=\infty (iv), so the limit is not a Lebesgue integral against \nu_\alpha.

Lean code for LemmaA.1●4 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_A_1_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {P : H →L[ℝ] H} (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (z : H) (hz : z ≠ 0) : 0 < inner ℝ (P z) z

theorem OperatorRidgelet.Paper.lem_A_1_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (z : H) (hz : z ≠ 0) :
  0 < inner ℝ (P z) z

**Lemma [lem:A.1]** Truncation of the scale integral.  For `z ≠ 0` the quadratic
form `q = ⟨Pz,z⟩` is positive.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_A_1_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {P : H →L[ℝ] H} (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (z : H) (hz : z ≠ 0) :
  Filter.Tendsto
    (fun εM =>
      MeasureTheory.charFun
        (OperatorRidgelet.gaussianMixtureOn N α (Set.Ioo εM.1 εM.2)) z)
    (nhdsWithin 0 (Set.Ioi 0) ×ˢ Filter.atTop)
    (nhds ↑(Real.Gamma (α / 2) * inner ℝ (P z) z ^ (-(α / 2))))

theorem OperatorRidgelet.Paper.lem_A_1_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (z : H)
  (hz : z ≠ 0) :
  Filter.Tendsto
    (fun εM =>
      MeasureTheory.charFun
        (OperatorRidgelet.gaussianMixtureOn
          N α (Set.Ioo εM.1 εM.2))
        z)
    (nhdsWithin 0 (Set.Ioi 0) ×ˢ
      Filter.atTop)
    (nhds
      ↑(Real.Gamma (α / 2) *
          inner ℝ (P z) z ^ (-(α / 2))))

**Lemma [lem:A.1]** Truncation of the scale integral.  The characteristic
functionals of the truncated mixtures `ν_α^{ε,M} = ∫_ε^M 𝒩(0,2sP) s^{α/2-1} ds` converge, as
`ε ↓ 0` and `M ↑ ∞`, to `Γ(α/2) q^{-α/2}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_A_1_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {P : H →L[ℝ] H} (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {α : ℝ} (hα : 0 < α) (z : H) (hz : z ≠ 0) :
  ∫ (s : ℝ) in Set.Ioi 0,
      Real.exp (-s * inner ℝ (P z) z) * s ^ (α / 2 - 1) =
    Real.Gamma (α / 2) * inner ℝ (P z) z ^ (-(α / 2))

theorem OperatorRidgelet.Paper.lem_A_1_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {α : ℝ} (hα : 0 < α) (z : H)
  (hz : z ≠ 0) :
  ∫ (s : ℝ) in Set.Ioi 0,
      Real.exp (-s * inner ℝ (P z) z) *
        s ^ (α / 2 - 1) =
    Real.Gamma (α / 2) *
      inner ℝ (P z) z ^ (-(α / 2))

**Lemma [lem:A.1]** Truncation of the scale integral.  The limit is the Gamma
integral `∫₀^∞ e^{-sq} s^{α/2-1} ds = Γ(α/2) q^{-α/2}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_A_1_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (z : H) (hz : z ≠ 0) :
  ¬MeasureTheory.Integrable
      (fun ξ => Complex.exp (↑(inner ℝ z ξ) * Complex.I))
      (OperatorRidgelet.gaussianMixture N α)

theorem OperatorRidgelet.Paper.lem_A_1_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (z : H)
  (hz : z ≠ 0) :
  ¬MeasureTheory.Integrable
      (fun ξ =>
        Complex.exp
          (↑(inner ℝ z ξ) * Complex.I))
      (OperatorRidgelet.gaussianMixture N
        α)

**Lemma [lem:A.1]** Truncation of the scale integral.  In contrast, the character
`ξ ↦ e^{i⟨z,ξ⟩}` is not integrable against `ν_α`, so the limit is not a Lebesgue integral.

Proof for Lemma A.1

Proof uses 2

Proof dependency previews

Preview

Lemma 3.1

Loading preview

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

The truncated mixture is finite, so Fubini and the characteristic functional of \mathcal N(0,2sP) reduce the integral to \int_\varepsilon^Me^{-sq}s^{\alpha/2-1}\mathrm ds; monotone convergence and the substitution u=sq finish the proof.

Remark A.2 (A Riesz-type kernel for the frame operator).

The regularized characteristic functional in Lemma A.1 suggests the kernel \Gamma(\alpha/2)\langle P(x-y),x-y\rangle^{-\alpha/2} for the frame operator. This is only a formal interchange against an infinite oscillatory measure and is not used as an identity. In finite dimension, with P=I and 0<\alpha<m, it agrees with the Riesz-potential interpretation of Corollary D.2.