2.1. The input and direction measures🔗

Definition2.1.1

uses 0

Used by 16

Reverse dependency previews

Preview

Definition 2.1.2

Loading preview

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

✓L∃∀N

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 Definition2.1.1●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

OperatorRidgelet.IsPositiveTraceClass

inner_nonneg : ∀ (x : H), 0 ≤ inner ℝ (P x) x

Inherited from

OperatorRidgelet.IsPositiveTraceClass

hasSummableTrace : OperatorRidgelet.HasSummableTrace P

Inherited from

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)`.

Definition2.1.2

Statement uses 2

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

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

Used by 7

Reverse dependency previews

Preview

Lemma 2.1.3

Loading preview

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

✓L∃∀N

The Gaussian layers are 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 the layers; the truncated mixture over a set of scales is used in Appendix A.

Lean code for Definition2.1.2●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 layers `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 layers `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.

Lemma2.1.3

uses 1

Used by 4

Reverse dependency previews

Preview

Lemma 2.1.4

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 Lemma2.1.3●4 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_mixture_integration_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_mixture_integration_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:mixture-integration]** 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_mixture_integration_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_mixture_integration_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:mixture-integration]** 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_mixture_integration_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_mixture_integration_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:mixture-integration]** 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_mixture_integration_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_mixture_integration_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:mixture-integration]** Measurability and integration of the mixture.  For
complex `F` the integration formula holds when `∫ |F| dν_α < ∞`.

Proof for Lemma 2.1.3

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.

Lemma2.1.4

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.2

Loading preview

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

Used by 11

Reverse dependency previews

Preview

Lemma 2.1.5

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 Lemma2.1.4●6 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_homogeneous_mixture_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_homogeneous_mixture_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:homogeneous-mixture]** Homogeneous Gaussian mixture.  In infinite dimension the
mixture `ν_α` is σ-finite.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_homogeneous_mixture_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_homogeneous_mixture_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:homogeneous-mixture]** Homogeneous Gaussian mixture.  The mixture `ν_α` is
finite on bounded Borel sets.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_homogeneous_mixture_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_homogeneous_mixture_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:homogeneous-mixture]** Homogeneous Gaussian mixture.  The mixture `ν_α` is
infinite on `H`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_homogeneous_mixture_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_homogeneous_mixture_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:homogeneous-mixture]** 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_homogeneous_mixture_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_homogeneous_mixture_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:homogeneous-mixture]** Homogeneous Gaussian mixture.  Homogeneity:
`(D_ω)_# ν_α = |ω|^{-α} ν_α` for `ω ≠ 0`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_homogeneous_mixture_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_homogeneous_mixture_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:homogeneous-mixture]** Homogeneous Gaussian mixture.  The integrated form of
homogeneity: `∫ F(ωa) ν_α(da) = |ω|^{-α} ∫ F dν_α` for every nonnegative Borel `F`.

Proof for Lemma 2.1.4

uses 0

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 on each layer proves homogeneity.

Lemma2.1.5

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.2

Loading preview

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

used 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 Lemma2.1.5●4 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_mixture_character_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_mixture_character_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:mixture-character]** Gaussian-layer regularization.  For `z ≠ 0` the quadratic
form `q = ⟨Pz,z⟩` is positive.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_mixture_character_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_mixture_character_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:mixture-character]** Gaussian-layer regularization.  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_mixture_character_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_mixture_character_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:mixture-character]** Gaussian-layer regularization.  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_mixture_character_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_mixture_character_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:mixture-character]** Gaussian-layer regularization.  In contrast, the character
`ξ ↦ e^{i⟨z,ξ⟩}` is not integrable against `ν_α`, so the limit is not a Lebesgue integral.

Proof for Lemma 2.1.5

uses 0

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.