Infinite-dimensional operator ridgelet transform

3.1. Gaussian input and homogeneous direction measures🔗

DefinitionAux.2
uses 0
Used by 14
Reverse dependency previews
Preview
Definition Aux.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

These are the covariance and Gaussian-measure conventions of Section 3.1.

A covariance is an injective, positive, self-adjoint, trace-class operator; the trace is taken along a Hilbert basis. The centred Gaussian measure \mu=\mathcal N(0,Q) is the Borel probability measure with characteristic functional \int_He^{i\langle x,\xi\rangle}\mu(\mathrm dx)=e^{-\langle Q\xi,\xi\rangle/2}.

Lean code for DefinitionAux.2●2 definitions
  • structure(extends 1, 4 fields)defined in OperatorRidgelet/Transform/Defs.lean
    complete
    structure OperatorRidgelet.IsTraceClassCovariance.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (P : H →L[ℝ] H) : Prop
    structure OperatorRidgelet.IsTraceClassCovariance.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (P : H →L[ℝ] H) : Prop
    The standing hypothesis on the covariance operators `P` and `Q` of the manuscript: injective,
positive, self-adjoint, and trace class (`IsPositiveTraceClass` together with injectivity).  The
trace condition is expressed along a Hilbert basis; for a positive operator the sum
`∑ ⟪P e_j, e_j⟫` does not depend on the basis.

    Extends

    • OperatorRidgelet.IsPositiveTraceClass P

    Fields

    isSelfAdjoint : IsSelfAdjoint P
    Inherited from
    1. OperatorRidgelet.IsPositiveTraceClass
    inner_nonneg : ∀ (x : H), 0 ≤ inner ℝ (P x) x
    Inherited from
    1. OperatorRidgelet.IsPositiveTraceClass
    hasSummableTrace : OperatorRidgelet.HasSummableTrace P
    Inherited from
    1. OperatorRidgelet.IsPositiveTraceClass
    injective : Function.Injective ⇑P
    `P` is injective.
  • structure(2 fields)defined in OperatorRidgelet/Transform/Defs.lean
    complete
    structure OperatorRidgelet.IsCenteredGaussian.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (Q : H →L[ℝ] H) (μ : MeasureTheory.Measure H) : Prop
    structure OperatorRidgelet.IsCenteredGaussian.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (Q : H →L[ℝ] H)
  (μ : MeasureTheory.Measure H) : Prop
    `μ = 𝒩(0,Q)`: the manuscript's centred Gaussian measure with covariance `Q` is the Borel
probability measure whose characteristic functional is `∫ e^{i⟪x,ξ⟫} dμ(x) = e^{-⟪Qξ,ξ⟫/2}`.

    Fields

    isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure μ
    `μ` is a probability measure. 
    charFun_eq : ∀ (ξ : H), MeasureTheory.charFun μ ξ = Complex.exp (-↑(inner ℝ (Q ξ) ξ / 2))
    The characteristic functional of `μ` is `exp(-⟪Qξ,ξ⟫/2)`.
DefinitionAux.3
Statement uses 2
Statement dependency previews
Preview
Definition Aux.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Lemma 3.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

This is the scale-mixture setup of Section 3.1, used in Lemmas 3.1 and 3.2.

The Gaussian components of the mixture form a family N_s=\mathcal N(0,2sP), s>0, with characteristic functionals e^{-s\langle P\xi,\xi\rangle}. For \alpha>0 the homogeneous Gaussian mixture is \nu_\alpha=\int_0^\infty\mathcal N(0,2sP)\,s^{\alpha/2-1}\,\mathrm ds, the Giry-monad bind of the weight s^{\alpha/2-1}\mathrm ds against these components; the truncated mixture over a set of scales is used in Appendix A.

Lean code for DefinitionAux.3●4 definitions
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.IsCenteredGaussianLayers.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (P : H →L[ℝ] H) (N : ℝ → MeasureTheory.Measure H) : Prop
    def OperatorRidgelet.IsCenteredGaussianLayers.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (P : H →L[ℝ] H)
  (N : ℝ → MeasureTheory.Measure H) : Prop
    A family of Gaussian components `N s = 𝒩(0, 2sP)` for `s > 0` (the value of `N` at `s ≤ 0` is
irrelevant).  The characteristic functional of `𝒩(0,2sP)` is `exp(-s⟪Pξ,ξ⟫)`.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.mixtureWeight (α : ℝ) (S : Set ℝ) :
  MeasureTheory.Measure ℝ
    def OperatorRidgelet.mixtureWeight (α : ℝ)
  (S : Set ℝ) : MeasureTheory.Measure ℝ
    The weight `s^{α/2-1} ds` restricted to a set `S` of scales.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.gaussianMixtureOn.{u_1} {H : Type u_1}
  [MeasurableSpace H] (N : ℝ → MeasureTheory.Measure H) (α : ℝ)
  (S : Set ℝ) : MeasureTheory.Measure H
    def OperatorRidgelet.gaussianMixtureOn.{u_1}
  {H : Type u_1} [MeasurableSpace H]
  (N : ℝ → MeasureTheory.Measure H)
  (α : ℝ) (S : Set ℝ) :
  MeasureTheory.Measure H
    The Gaussian mixture over a set `S` of scales, `∫_S 𝒩(0,2sP) s^{α/2-1} ds`, as the
Giry-monad bind of the weight `s^{α/2-1} ds` on `S` against the components `N`.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.gaussianMixture.{u_1} {H : Type u_1}
  [MeasurableSpace H] (N : ℝ → MeasureTheory.Measure H) (α : ℝ) :
  MeasureTheory.Measure H
    def OperatorRidgelet.gaussianMixture.{u_1}
  {H : Type u_1} [MeasurableSpace H]
  (N : ℝ → MeasureTheory.Measure H)
  (α : ℝ) : MeasureTheory.Measure H
    The homogeneous Gaussian mixture `ν_α = ∫₀^∞ 𝒩(0,2sP) s^{α/2-1} ds` of the manuscript.

For an eigenbasis Pe_j=p_je_j with \sum_jp_j<\infty, independent standard Gaussians give the almost surely convergent series X=\sum_j\sqrt{p_j}Z_je_j. The scaled random variables \sqrt{2s}X realize every Gaussian component on one probability space. Joint measurability in s and the sample variable gives the mixture integration formula.

Lemma3.1
uses 1
Used by 4
Reverse dependency previews
Preview
Lemma 3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For every Borel set E, the map s\mapsto\mathcal N(0,2sP)(E) is Borel measurable (i), and the mixture defines a countably additive Borel measure with \nu_\alpha(E)=\int_0^\infty\mathcal N(0,2sP)(E)\,s^{\alpha/2-1}\,\mathrm ds (ii). For every nonnegative Borel F, \int_HF\,\mathrm d\nu_\alpha=\int_0^\infty\int_HF\,\mathrm d\mathcal N(0,2sP)\,s^{\alpha/2-1}\,\mathrm ds (iii), and the identity holds for complex F with \int_H|F|\,\mathrm d\nu_\alpha<\infty (iv).

Lean code for Lemma3.1●4 theorems
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_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)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (E : Set H) :
  MeasurableSet E → Measurable fun s => (N ↑s) E
    theorem OperatorRidgelet.Paper.lem_3_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)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (E : Set H) :
  MeasurableSet E →
    Measurable fun s => (N ↑s) E
    **Lemma [lem:3.1]** Measurability and integration of the mixture.  For every
Borel set `E`, the map `s ↦ 𝒩(0,2sP)(E)` is Borel measurable on `(0,∞)`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_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 < α) (E : Set H) :
  MeasurableSet E →
    (OperatorRidgelet.gaussianMixture N α) E =
      ∫⁻ (s : ℝ) in Set.Ioi 0,
        (N s) E * ENNReal.ofReal (s ^ (α / 2 - 1))
    theorem OperatorRidgelet.Paper.lem_3_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 < α) (E : Set H) :
  MeasurableSet E →
    (OperatorRidgelet.gaussianMixture N α)
        E =
      ∫⁻ (s : ℝ) in Set.Ioi 0,
        (N s) E *
          ENNReal.ofReal (s ^ (α / 2 - 1))
    **Lemma [lem:3.1]** Measurability and integration of the mixture.  The
mixture is a countably additive Borel measure given on Borel sets by
`ν_α(E) = ∫₀^∞ 𝒩(0,2sP)(E) s^{α/2-1} ds`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_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)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (F : H → ENNReal) :
  Measurable F →
    ∫⁻ (ξ : H), F ξ ∂OperatorRidgelet.gaussianMixture N α =
      ∫⁻ (s : ℝ) in Set.Ioi 0,
        (∫⁻ (ξ : H), F ξ ∂N s) * ENNReal.ofReal (s ^ (α / 2 - 1))
    theorem OperatorRidgelet.Paper.lem_3_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)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (F : H → ENNReal) :
  Measurable F →
    ∫⁻ (ξ : H),
        F
          ξ ∂OperatorRidgelet.gaussianMixture
          N α =
      ∫⁻ (s : ℝ) in Set.Ioi 0,
        (∫⁻ (ξ : H), F ξ ∂N s) *
          ENNReal.ofReal (s ^ (α / 2 - 1))
    **Lemma [lem:3.1]** Measurability and integration of the mixture.  For every
nonnegative Borel `F`, `∫ F dν_α = ∫₀^∞ (∫ F d𝒩(0,2sP)) s^{α/2-1} ds`, both sides possibly
infinite.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_1_iv.{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 < α) (F : H → ℂ) :
  MeasureTheory.Integrable F (OperatorRidgelet.gaussianMixture N α) →
    ∫ (ξ : H), F ξ ∂OperatorRidgelet.gaussianMixture N α =
      ∫ (s : ℝ) in Set.Ioi 0, (∫ (ξ : H), F ξ ∂N s) * ↑(s ^ (α / 2 - 1))
    theorem OperatorRidgelet.Paper.lem_3_1_iv.{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 < α) (F : H → ℂ) :
  MeasureTheory.Integrable F
      (OperatorRidgelet.gaussianMixture N
        α) →
    ∫ (ξ : H),
        F
          ξ ∂OperatorRidgelet.gaussianMixture
          N α =
      ∫ (s : ℝ) in Set.Ioi 0,
        (∫ (ξ : H), F ξ ∂N s) *
          ↑(s ^ (α / 2 - 1))
    **Lemma [lem:3.1]** Measurability and integration of the mixture.  For
complex `F` the integration formula holds when `∫ |F| dν_α < ∞`.
Proof for Lemma 3.1
uses 0

\mathcal N(0,2sP)(E)=\int\mathbf 1_E(\sqrt{2s}\,x)\,\mathcal N(0,P)(\mathrm dx) with a jointly Borel integrand; monotone convergence gives countable additivity and extends the integral identity from indicators to nonnegative Borel functions.

Lemma3.2
Statement uses 2
Statement dependency previews
Preview
Definition Aux.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 11
Reverse dependency previews
Preview
Lemma 3.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Assume \dim H=\infty and \alpha>0. Then \nu_\alpha is \sigma-finite (i), finite on bounded Borel sets (ii), infinite on H (iii), and has full support (iv). For \omega\ne0, (D_\omega)_\#\nu_\alpha=|\omega|^{-\alpha}\nu_\alpha (v), equivalently \int_HF(\omega a)\,\nu_\alpha(\mathrm da)=|\omega|^{-\alpha}\int_HF\,\mathrm d\nu_\alpha for every nonnegative Borel F (vi).

Lean code for Lemma3.2●6 theorems
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_2_i.{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 < α) :
  MeasureTheory.SigmaFinite (OperatorRidgelet.gaussianMixture N α)
    theorem OperatorRidgelet.Paper.lem_3_2_i.{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 < α) :
  MeasureTheory.SigmaFinite
    (OperatorRidgelet.gaussianMixture N α)
    **Lemma [lem:3.2]** Homogeneous Gaussian mixture.  In infinite dimension the
mixture `ν_α` is σ-finite.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_2_ii.{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 < α) (E : Set H) :
  MeasurableSet E →
    Bornology.IsBounded E → (OperatorRidgelet.gaussianMixture N α) E < ⊤
    theorem OperatorRidgelet.Paper.lem_3_2_ii.{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 < α) (E : Set H) :
  MeasurableSet E →
    Bornology.IsBounded E →
      (OperatorRidgelet.gaussianMixture N
            α)
          E <
        ⊤
    **Lemma [lem:3.2]** Homogeneous Gaussian mixture.  The mixture `ν_α` is
finite on bounded Borel sets.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_2_iii.{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 < α) : (OperatorRidgelet.gaussianMixture N α) Set.univ = ⊤
    theorem OperatorRidgelet.Paper.lem_3_2_iii.{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 < α) :
  (OperatorRidgelet.gaussianMixture N α)
      Set.univ =
    ⊤
    **Lemma [lem:3.2]** Homogeneous Gaussian mixture.  The mixture `ν_α` is
infinite on `H`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_2_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 < α) : (OperatorRidgelet.gaussianMixture N α).IsOpenPosMeasure
    theorem OperatorRidgelet.Paper.lem_3_2_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 < α) :
  (OperatorRidgelet.gaussianMixture N
      α).IsOpenPosMeasure
    **Lemma [lem:3.2]** Homogeneous Gaussian mixture.  The mixture `ν_α` has
full support: it charges every nonempty open set.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_2_v.{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 < α) :
  OperatorRidgelet.IsHomogeneous α
    (OperatorRidgelet.gaussianMixture N α)
    theorem OperatorRidgelet.Paper.lem_3_2_v.{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 < α) :
  OperatorRidgelet.IsHomogeneous α
    (OperatorRidgelet.gaussianMixture N α)
    **Lemma [lem:3.2]** Homogeneous Gaussian mixture.  Homogeneity:
`(D_ω)_# ν_α = |ω|^{-α} ν_α` for `ω ≠ 0`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_2_vi.{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 < α) (ω : ℝ) :
  ω ≠ 0 →
    ∀ (F : H → ENNReal),
      Measurable F →
        ∫⁻ (a : H), F (ω • a) ∂OperatorRidgelet.gaussianMixture N α =
          ENNReal.ofReal (|ω| ^ (-α)) *
            ∫⁻ (ξ : H), F ξ ∂OperatorRidgelet.gaussianMixture N α
    theorem OperatorRidgelet.Paper.lem_3_2_vi.{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 < α) (ω : ℝ) :
  ω ≠ 0 →
    ∀ (F : H → ENNReal),
      Measurable F →
        ∫⁻ (a : H),
            F
              (ω •
                a) ∂OperatorRidgelet.gaussianMixture
              N α =
          ENNReal.ofReal (|ω| ^ (-α)) *
            ∫⁻ (ξ : H),
              F
                ξ ∂OperatorRidgelet.gaussianMixture
                N α
    **Lemma [lem:3.2]** Homogeneous Gaussian mixture.  The integrated form of
homogeneity: `∫ F(ωa) ν_α(da) = |ω|^{-α} ∫ F dν_α` for every nonnegative Borel `F`.
Proof for Lemma 3.2
uses 1

Coordinate small-ball estimates of order s^{-k/2} with k>\alpha give finite mass on bounded sets, the part s\le1 is integrable because s^{\alpha/2-1} is, balls exhaust H while \nu_\alpha(H)=\int_0^\infty s^{\alpha/2-1}\mathrm ds=\infty, injectivity of P gives full support, and the substitution u=s\omega^2 in each component proves homogeneity.