6.1. Preliminaries🔗

Definition6.1.1

uses 0

Used by 4

Reverse dependency previews

Preview

Proposition 6.2.1

Loading preview

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

✓L∃∀N

A function f on H is cylindrical if f=\widetilde f\circ L for a linear map L:H\to\mathbb R^m, and a linear map has infinite rank when its range is not finite dimensional. The elementary obstruction: a target F cannot factor through an observation P if P(x)=P(y) but F(x)\ne F(y); in particular, if F separates 0 from a vector in the kernel of a linear P, then F is not cylindrical through P.

Lean code for Definition6.1.1●5 declarations

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.IsCylindrical.{u_1, u_2} {H : Type u_1} {Y : Type u_2}
  [AddCommGroup H] [Module ℝ H] (f : H → Y) : Prop

def OperatorRidgelet.IsCylindrical.{u_1, u_2}
  {H : Type u_1} {Y : Type u_2}
  [AddCommGroup H] [Module ℝ H]
  (f : H → Y) : Prop

A function `f` on `H` is cylindrical if `f = f̃ ∘ L` for a finite-rank linear map `L`, here
a linear map `L : H → ℝ^m` (not assumed continuous).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.HasInfiniteRank.{u_1, u_3} {H : Type u_1}
  [AddCommGroup H] [Module ℝ H] {F : Type u_3} [AddCommGroup F]
  [Module ℝ F] (L : H →ₗ[ℝ] F) : Prop

def OperatorRidgelet.HasInfiniteRank.{u_1,
    u_3}
  {H : Type u_1} [AddCommGroup H]
  [Module ℝ H] {F : Type u_3}
  [AddCommGroup F] [Module ℝ F]
  (L : H →ₗ[ℝ] F) : Prop

A linear map has infinite rank when its range is not finite dimensional.

defdefined in OperatorRidgelet/Cylindrical.lean

complete

def OperatorRidgelet.FactorsThrough.{u_1, u_2, u_3} {E : Type u_1}
  {Y : Type u_2} {Z : Type u_3} (F : E → Y) (P : E → Z) : Prop

def OperatorRidgelet.FactorsThrough.{u_1, u_2,
    u_3}
  {E : Type u_1} {Y : Type u_2}
  {Z : Type u_3} (F : E → Y) (P : E → Z) :
  Prop

A function `F` factors through an observation map `P`.

theoremdefined in OperatorRidgelet/Cylindrical.lean

complete

theorem OperatorRidgelet.not_factorsThrough_of_fibre_separation.{u_1, u_2, u_3}
  {E : Type u_1} {Y : Type u_2} {Z : Type u_3} {F : E → Y} {P : E → Z}
  {x y : E} (hP : P x = P y) (hF : F x ≠ F y) :
  ¬OperatorRidgelet.FactorsThrough F P

theorem OperatorRidgelet.not_factorsThrough_of_fibre_separation.{u_1,
    u_2, u_3}
  {E : Type u_1} {Y : Type u_2}
  {Z : Type u_3} {F : E → Y} {P : E → Z}
  {x y : E} (hP : P x = P y)
  (hF : F x ≠ F y) :
  ¬OperatorRidgelet.FactorsThrough F P

A function separating two points of one fibre cannot factor through the observation map.

theoremdefined in OperatorRidgelet/Cylindrical.lean

complete

theorem OperatorRidgelet.not_factorsThrough_linear_of_kernel_separation.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {E : Type u_2} {Y : Type u_3} {Z : Type u_4}
  [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid Z]
  [Module 𝕜 Z] {F : E → Y} (P : E →ₗ[𝕜] Z) {x : E} (hx : x ∈ P.ker)
  (hF : F x ≠ F 0) : ¬OperatorRidgelet.FactorsThrough F ⇑P

theorem OperatorRidgelet.not_factorsThrough_linear_of_kernel_separation.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {E : Type u_2}
  {Y : Type u_3} {Z : Type u_4}
  [Semiring 𝕜] [AddCommMonoid E]
  [Module 𝕜 E] [AddCommMonoid Z]
  [Module 𝕜 Z] {F : E → Y} (P : E →ₗ[𝕜] Z)
  {x : E} (hx : x ∈ P.ker)
  (hF : F x ≠ F 0) :
  ¬OperatorRidgelet.FactorsThrough F ⇑P

Separating zero from a kernel vector obstructs factorization through a linear map.

Definition6.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 4

Reverse dependency previews

Preview

Definition 6.1.3

Loading preview

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

✓L∃∀N

Mathlib has neither trace-class operators nor Fredholm determinants. The trace \operatorname{tr}P=\sum_i\langle Pe_i,e_i\rangle is taken along a Hilbert basis for which the sum converges; a positive trace-class operator is positive, self-adjoint, with summable trace; square roots Q^{1/2} are data S with S positive self-adjoint and S^2=Q; the Fredholm determinant \det(I+M)=\prod_i(1+m_i) is computed along an orthonormal eigenbasis of M; and (I+M)^{-1} enters through the quadratic form \langle S(I+M)^{-1}Sx,x\rangle.

Lean code for Definition6.1.2●9 definitions

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.traceAlong.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Type u_2}
  (b : HilbertBasis ι ℝ H) (P : H →L[ℝ] H) : ℝ

def OperatorRidgelet.traceAlong.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ι : Type u_2}
  (b : HilbertBasis ι ℝ H)
  (P : H →L[ℝ] H) : ℝ

The trace `∑ ⟪P e_i, e_i⟫` of `P` along the Hilbert basis `b`.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.HasSummableTrace.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (P : H →L[ℝ] H) : Prop

def OperatorRidgelet.HasSummableTrace.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (P : H →L[ℝ] H) : Prop

`P` is trace class in the sense of the manuscript: `∑ ⟪P e_i, e_i⟫` converges along some
Hilbert basis.

defdefined in OperatorRidgelet/Transform/Defs.lean

complete

def OperatorRidgelet.traceOf.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (P : H →L[ℝ] H) : ℝ

def OperatorRidgelet.traceOf.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (P : H →L[ℝ] H) : ℝ

The trace `tr P = ∑ ⟪P e_i, e_i⟫`, along a Hilbert basis for which the sum converges (`0`
if there is none); for a positive operator the value does not depend on the basis.

structure(3 fields)defined in OperatorRidgelet/Transform/Defs.lean

complete

structure OperatorRidgelet.IsPositiveTraceClass.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (P : H →L[ℝ] H) : Prop

structure OperatorRidgelet.IsPositiveTraceClass.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (P : H →L[ℝ] H) : Prop

A positive, self-adjoint, trace-class operator: the hypothesis on `Σ` in Lemma
`lem:gaussian-quadratic`, and the covariance hypothesis `IsTraceClassCovariance` without
injectivity.

Fields

isSelfAdjoint : IsSelfAdjoint P

`P` is self-adjoint.

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

`P` is positive: `⟪P x, x⟫ ≥ 0`.

hasSummableTrace : OperatorRidgelet.HasSummableTrace P

`P` is trace class: `∑ ⟪P e_j, e_j⟫ < ∞` along a Hilbert basis.

structure(3 fields)defined in OperatorRidgelet/Examples/Defs.lean

complete

structure OperatorRidgelet.IsPositiveSqrt.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (S Q : H →L[ℝ] H) : Prop

structure OperatorRidgelet.IsPositiveSqrt.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (S Q : H →L[ℝ] H) :
  Prop

`S` is the positive square root of `Q`: `S` is positive self-adjoint and `S² = Q`.

Fields

isSelfAdjoint : IsSelfAdjoint S

`S` is self-adjoint.

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

`S` is positive.

mul_self : S * S = Q

`S * S = Q`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.HasEigenbasis.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Type u_2}
  (M : H →L[ℝ] H) (e : HilbertBasis ι ℝ H) (w : ι → ℝ) : Prop

def OperatorRidgelet.HasEigenbasis.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ι : Type u_2}
  (M : H →L[ℝ] H) (e : HilbertBasis ι ℝ H)
  (w : ι → ℝ) : Prop

`e` is an orthonormal eigenbasis of `M` with eigenvalues `w`: `M e_i = w_i e_i`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.fredholmDetAlong.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Type u_2}
  (e : HilbertBasis ι ℝ H) (M : H →L[ℝ] H) : ℝ

def OperatorRidgelet.fredholmDetAlong.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ι : Type u_2}
  (e : HilbertBasis ι ℝ H)
  (M : H →L[ℝ] H) : ℝ

The product `∏ (1 + ⟪M e_i, e_i⟫)` along the Hilbert basis `e`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.fredholmDet.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (M : H →L[ℝ] H) : ℝ

def OperatorRidgelet.fredholmDet.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (M : H →L[ℝ] H) : ℝ

The Fredholm determinant `det(I + M)` of a (positive trace-class) operator `M`: the product
`∏ (1 + m_i)` over the eigenvalues, computed along an orthonormal eigenbasis of `M` (`1` if `M`
has none).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.resolventForm.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S M : H →L[ℝ] H)
  (x : H) : ℝ

def OperatorRidgelet.resolventForm.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (S M : H →L[ℝ] H) (x : H) : ℝ

The quadratic form `⟪S (I + M)⁻¹ S x, x⟫`, with `(I + M)⁻¹ = Ring.inverse (1 + M)`.

Definition6.1.3

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 5

Reverse dependency previews

Preview

Lemma 6.1.6

Loading preview

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

✓L∃∀N

The Gaussian activation \Phi(u)=\phi(u)=e^{-u^2/2} with \phi''(b)=(b^2-1)e^{-b^2/2}, the convolution (\rho*\phi_v)(c) with the centred Gaussian of variance v\ge0, the Gaussian target f_W(x)=e^{-\langle Wx,x\rangle/2}, and, for M=Q^{1/2}WQ^{1/2}, \kappa_W(\xi)=\langle Q^{1/2}(I+M)^{-1}Q^{1/2}\xi,\xi\rangle, S_W=Q^{1/2}(I+M)^{-1}Q^{1/2}, and \Sigma_s=2sP^{1/2}(I+2sP^{1/2}S_WP^{1/2})^{-1}P^{1/2}. Membership f\in\mathcal D_\alpha of a function (rather than of an L^2 class) means f\in L^2(\mu) and \mathcal G_\mu f\in L^2(\nu), related to the submodule \mathcal D_\alpha by the stated lemmas.

Lean code for Definition6.1.3●13 declarations

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.gaussianFun (u : ℝ) : ℝ

def OperatorRidgelet.gaussianFun (u : ℝ) : ℝ

The Gaussian activation `u ↦ e^{-u²/2}`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianActDeriv2 (b : ℝ) : ℝ

def OperatorRidgelet.gaussianActDeriv2
  (b : ℝ) : ℝ

The second derivative `φ''(b) = (b² - 1) e^{-b²/2}` of the Gaussian activation
`φ = gaussianFun`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianSmooth (ρ : ℝ → ℝ) (v c : ℝ) : ℝ

def OperatorRidgelet.gaussianSmooth
  (ρ : ℝ → ℝ) (v c : ℝ) : ℝ

The convolution `(ρ * φ_v)(c) = ∫ ρ(c - t) 𝒩(0,v)(dt)` of a filter with the centred
one-dimensional Gaussian of variance `v ≥ 0` (`φ_0 = δ_0`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianTarget.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (W : H →L[ℝ] H)
  (x : H) : ℂ

def OperatorRidgelet.gaussianTarget.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (W : H →L[ℝ] H)
  (x : H) : ℂ

The Gaussian target `f_W(x) = e^{-⟨Wx,x⟩/2}` (`eq:gaussian-target`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianKappa.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S W : H →L[ℝ] H)
  (ξ : H) : ℝ

def OperatorRidgelet.gaussianKappa.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (S W : H →L[ℝ] H) (ξ : H) : ℝ

`κ_W(ξ) = ⟨Q^{1/2} (I + M)⁻¹ Q^{1/2} ξ, ξ⟩` with `M = Q^{1/2} W Q^{1/2}`, for `S = Q^{1/2}`
(`eq:gaussian-target`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianTargetResolvent.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S W : H →L[ℝ] H) :
  H →L[ℝ] H

def OperatorRidgelet.gaussianTargetResolvent.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (S W : H →L[ℝ] H) : H →L[ℝ] H

`S_W = Q^{1/2} (I + M)⁻¹ Q^{1/2}`, `M = Q^{1/2} W Q^{1/2}`, for `S = Q^{1/2}`
(`eq:filtered-gaussian-target`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.mixtureLayerCovariance.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (R T : H →L[ℝ] H)
  (s : ℝ) : H →L[ℝ] H

def OperatorRidgelet.mixtureLayerCovariance.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (R T : H →L[ℝ] H) (s : ℝ) : H →L[ℝ] H

`Σ_s = 2s P^{1/2} (I + 2s P^{1/2} T P^{1/2})⁻¹ P^{1/2}` for `R = P^{1/2}` and `T = S_W`
(`eq:filtered-gaussian-target`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.MemSpectralCore.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) (f : H → ℂ) : Prop

def OperatorRidgelet.MemSpectralCore.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  (f : H → ℂ) : Prop

`f ∈ 𝒟_α` for a function `f`: `f ∈ L²(μ)` and `𝒢_μ f ∈ L²(ν)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.MemSpectralCoreVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H) (f : H → Y) : Prop

def OperatorRidgelet.MemSpectralCoreVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H)
  (f : H → Y) : Prop

`f ∈ 𝒟_α(Y)` for a `Y`-valued function `f`: `f ∈ L²(μ;Y)` and `𝒢_μ f ∈ L²(ν;Y)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.toLpOrZero.{u_1, u_2} {α : Type u_1} {E : Type u_2}
  [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α) (f : α → E) : ↥(MeasureTheory.Lp E p μ)

def OperatorRidgelet.toLpOrZero.{u_1, u_2}
  {α : Type u_1} {E : Type u_2}
  [MeasurableSpace α]
  [NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α)
  (f : α → E) : ↥(MeasureTheory.Lp E p μ)

The element of `L^p(μ)` represented by `f`, and `0` when `f ∉ L^p(μ)`.

theoremdefined in OperatorRidgelet/Examples/Defs.lean

complete

theorem OperatorRidgelet.gaussFourier_congr_ae.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {μ : MeasureTheory.Measure H} {f g : H → ℂ} (h : f =ᵐ[μ] g) :
  OperatorRidgelet.gaussFourier μ f = OperatorRidgelet.gaussFourier μ g

theorem OperatorRidgelet.gaussFourier_congr_ae.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  {μ : MeasureTheory.Measure H}
  {f g : H → ℂ} (h : f =ᵐ[μ] g) :
  OperatorRidgelet.gaussFourier μ f =
    OperatorRidgelet.gaussFourier μ g

Almost-everywhere equal spectral densities define the same Gaussian Fourier target.

theoremdefined in OperatorRidgelet/Examples/Defs.lean

complete

theorem OperatorRidgelet.toLp_mem_spectralCore_iff.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ] {f : H → ℂ}
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp.toLp f hf ∈ OperatorRidgelet.spectralCore μ ν ↔
    MeasureTheory.MemLp (OperatorRidgelet.gaussFourier μ f) 2 ν

theorem OperatorRidgelet.toLp_mem_spectralCore_iff.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : H → ℂ}
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp.toLp f hf ∈
      OperatorRidgelet.spectralCore μ ν ↔
    MeasureTheory.MemLp
      (OperatorRidgelet.gaussFourier μ f)
      2 ν

Passing a square-integrable density to `L²` preserves membership in the spectral core.

theoremdefined in OperatorRidgelet/Examples/Defs.lean

complete

theorem OperatorRidgelet.memSpectralCore_iff.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ] {f : H → ℂ} :
  OperatorRidgelet.MemSpectralCore μ ν f ↔
    ∃ (hf : MeasureTheory.MemLp f 2 μ),
      MeasureTheory.MemLp.toLp f hf ∈ OperatorRidgelet.spectralCore μ ν

theorem OperatorRidgelet.memSpectralCore_iff.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : H → ℂ} :
  OperatorRidgelet.MemSpectralCore μ ν f ↔
    ∃ (hf : MeasureTheory.MemLp f 2 μ),
      MeasureTheory.MemLp.toLp f hf ∈
        OperatorRidgelet.spectralCore μ ν

The function-level spectral core agrees with membership of its `L²` representative.

Lemma6.1.4

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 1✓L∃∀N

Let \Sigma be a positive self-adjoint trace-class operator, S a bounded positive self-adjoint operator, and x\in H. Then M=\Sigma^{1/2}S\Sigma^{1/2} is trace class (i), and \int_He^{i\langle x,\xi\rangle-\langle S\xi,\xi\rangle/2}\,\mathcal N(0,\Sigma)(\mathrm d\xi)=\det(I+M)^{-1/2}\exp\bigl(-\tfrac12\langle\Sigma^{1/2}(I+M)^{-1}\Sigma^{1/2}x,x\rangle\bigr) (ii).

Lean code for Lemma6.1.4●2 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_gaussian_quadratic_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  {Cov S R : H →L[ℝ] H}
  (hCov : OperatorRidgelet.IsPositiveTraceClass Cov)
  (hS : IsSelfAdjoint S) (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR : OperatorRidgelet.IsPositiveSqrt R Cov) :
  OperatorRidgelet.HasSummableTrace (R * S * R)

theorem OperatorRidgelet.Paper.lem_gaussian_quadratic_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {Cov S R : H →L[ℝ] H}
  (hCov :
    OperatorRidgelet.IsPositiveTraceClass
      Cov)
  (hS : IsSelfAdjoint S)
  (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR :
    OperatorRidgelet.IsPositiveSqrt R
      Cov) :
  OperatorRidgelet.HasSummableTrace
    (R * S * R)

**Lemma [lem:gaussian-quadratic]** Gaussian integral of a quadratic exponential.  For a
positive self-adjoint trace-class `Σ` and a bounded positive self-adjoint `S`, the operator
`M = Σ^{1/2} S Σ^{1/2}` is trace class.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_gaussian_quadratic_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Cov S R : H →L[ℝ] H}
  (hCov : OperatorRidgelet.IsPositiveTraceClass Cov)
  (hS : IsSelfAdjoint S) (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR : OperatorRidgelet.IsPositiveSqrt R Cov)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Cov μ) (x : H) :
  ∫ (ξ : H),
      Complex.exp
        (↑(inner ℝ x ξ) * Complex.I - ↑(inner ℝ (S ξ) ξ / 2)) ∂μ =
    ↑(√(OperatorRidgelet.fredholmDet (R * S * R)))⁻¹ *
      Complex.exp
        (-↑(OperatorRidgelet.resolventForm R (R * S * R) x / 2))

theorem OperatorRidgelet.Paper.lem_gaussian_quadratic_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Cov S R : H →L[ℝ] H}
  (hCov :
    OperatorRidgelet.IsPositiveTraceClass
      Cov)
  (hS : IsSelfAdjoint S)
  (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR :
    OperatorRidgelet.IsPositiveSqrt R Cov)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian
      Cov μ)
  (x : H) :
  ∫ (ξ : H),
      Complex.exp
        (↑(inner ℝ x ξ) * Complex.I -
          ↑(inner ℝ (S ξ) ξ / 2)) ∂μ =
    ↑(√(OperatorRidgelet.fredholmDet
              (R * S * R)))⁻¹ *
      Complex.exp
        (-↑(OperatorRidgelet.resolventForm
                R (R * S * R) x /
              2))

**Lemma [lem:gaussian-quadratic]** Gaussian integral of a quadratic exponential.  With
`M = Σ^{1/2} S Σ^{1/2}`,
`∫ e^{i⟨x,ξ⟩ - ⟨Sξ,ξ⟩/2} 𝒩(0,Σ)(dξ) = det(I+M)^{-1/2} exp(-½⟨Σ^{1/2}(I+M)⁻¹Σ^{1/2}x, x⟩)`.

Proof for Lemma 6.1.4

uses 0

In an orthonormal eigenbasis (u_j) of M with eigenvalues m_j, the Gaussian series \xi=\sum_j\eta_j\Sigma^{1/2}u_j has law \mathcal N(0,\Sigma), \langle S\xi,\xi\rangle=\sum_jm_j\eta_j^2, and the expectation factorizes into one-dimensional Gaussian integrals (1+m_j)^{-1/2}e^{-x_j^2/(2(1+m_j))}.

Definition6.1.5

uses 0

Used by 4

Reverse dependency previews

Preview

Lemma 6.1.6

Loading preview

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

✓L∃∀N

\operatorname{ReLU}(x)=\max(x,0) and its odd part is the identity, \operatorname{ReLU}(x)-\operatorname{ReLU}(-x)=x. For a finite spectral index set, the paired-ReLU network \sum_i\lambda_i[\operatorname{ReLU}(\langle e_i,x\rangle)-\operatorname{ReLU}(-\langle e_i,x\rangle)]e_i therefore equals the spectral truncation \sum_i\lambda_i\langle e_i,x\rangle e_i exactly.

Lean code for Definition6.1.5●4 declarations

defdefined in LeanRidgelet/Activation/ReLU.lean

complete

def LeanRidgelet.relu (x : ℝ) : ℝ

def LeanRidgelet.relu (x : ℝ) : ℝ

The classical rectified linear unit.

theoremdefined in OperatorRidgelet/Activation.lean

complete

theorem OperatorRidgelet.relu_sub_relu_neg (x : ℝ) :
  LeanRidgelet.relu x - LeanRidgelet.relu (-x) = x

theorem OperatorRidgelet.relu_sub_relu_neg
  (x : ℝ) :
  LeanRidgelet.relu x -
      LeanRidgelet.relu (-x) =
    x

The difference of the two signed ReLU neurons is the identity.

defdefined in OperatorRidgelet/Activation.lean

complete

def OperatorRidgelet.spectralReLUNetwork.{u_1, u_2} {ι : Type u_1}
  {E : Type u_2} [DecidableEq ι] [AddCommMonoid E] [Module ℝ E]
  (s : Finset ι) (coeff coordinate : ι → ℝ) (basis : ι → E) : E

def OperatorRidgelet.spectralReLUNetwork.{u_1,
    u_2}
  {ι : Type u_1} {E : Type u_2}
  [DecidableEq ι] [AddCommMonoid E]
  [Module ℝ E] (s : Finset ι)
  (coeff coordinate : ι → ℝ)
  (basis : ι → E) : E

A finite signed-pair ReLU network with spectral coefficients.

theoremdefined in OperatorRidgelet/Activation.lean

complete

theorem OperatorRidgelet.spectralReLUNetwork_eq.{u_1, u_2} {ι : Type u_1}
  {E : Type u_2} [DecidableEq ι] [AddCommMonoid E] [Module ℝ E]
  (s : Finset ι) (coeff coordinate : ι → ℝ) (basis : ι → E) :
  OperatorRidgelet.spectralReLUNetwork s coeff coordinate basis =
    ∑ i ∈ s, (coeff i * coordinate i) • basis i

theorem OperatorRidgelet.spectralReLUNetwork_eq.{u_1,
    u_2}
  {ι : Type u_1} {E : Type u_2}
  [DecidableEq ι] [AddCommMonoid E]
  [Module ℝ E] (s : Finset ι)
  (coeff coordinate : ι → ℝ)
  (basis : ι → E) :
  OperatorRidgelet.spectralReLUNetwork s
      coeff coordinate basis =
    ∑ i ∈ s,
      (coeff i * coordinate i) • basis i

Each signed ReLU pair reduces the spectral network to its linear spectral sum.

Lemma6.1.6

Statement uses 2

Statement dependency previews

Preview

Definition 6.1.3

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Proposition 6.3.2

Loading preview

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

✓L∃∀N

For \phi(u)=e^{-u^2/2}, the integral \int_{\mathbb R}(u-b)_+\phi''(b)\,\mathrm db converges absolutely for each u (i a) and equals \phi(u) (i b), and \int_{\mathbb R}(1+|b|^k)|\phi''(b)|\,\mathrm db<\infty for every k\ge0 (ii).

Lean code for Lemma6.1.6●3 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_gaussian_hinge_i_a (u : ℝ) :
  MeasureTheory.Integrable
    (fun b =>
      LeanRidgelet.relu (u - b) * OperatorRidgelet.gaussianActDeriv2 b)
    MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_gaussian_hinge_i_a
  (u : ℝ) :
  MeasureTheory.Integrable
    (fun b =>
      LeanRidgelet.relu (u - b) *
        OperatorRidgelet.gaussianActDeriv2
          b)
    MeasureTheory.volume

**Lemma [lem:gaussian-hinge]** Absolute hinge representation of the Gaussian.  For
`φ(u) = e^{-u²/2}` the integral `∫ (u-b)_+ φ''(b) db` converges absolutely for each `u`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_gaussian_hinge_i_b (u : ℝ) :
  ∫ (b : ℝ),
      LeanRidgelet.relu (u - b) * OperatorRidgelet.gaussianActDeriv2 b =
    OperatorRidgelet.gaussianFun u

theorem OperatorRidgelet.Paper.lem_gaussian_hinge_i_b
  (u : ℝ) :
  ∫ (b : ℝ),
      LeanRidgelet.relu (u - b) *
        OperatorRidgelet.gaussianActDeriv2
          b =
    OperatorRidgelet.gaussianFun u

**Lemma [lem:gaussian-hinge]** Absolute hinge representation of the Gaussian.  For
`φ(u) = e^{-u²/2}`, `φ(u) = ∫ (u-b)_+ φ''(b) db` for each `u`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_gaussian_hinge_ii (k : ℕ) :
  MeasureTheory.Integrable
    (fun b => (1 + |b| ^ k) * |OperatorRidgelet.gaussianActDeriv2 b|)
    MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_gaussian_hinge_ii
  (k : ℕ) :
  MeasureTheory.Integrable
    (fun b =>
      (1 + |b| ^ k) *
        |OperatorRidgelet.gaussianActDeriv2
            b|)
    MeasureTheory.volume

**Lemma [lem:gaussian-hinge]** Absolute hinge representation of the Gaussian.
`∫ (1 + |b|^k) |φ''(b)| db < ∞` for every `k ≥ 0`.

Proof for Lemma 6.1.6

uses 0

\phi''(b)=(b^2-1)e^{-b^2/2} has all polynomially weighted absolute integrals finite, and integrating by parts on (-L,u) gives \int_{-L}^u(u-b)\phi''(b)\mathrm db=\phi(u)-\phi(-L)-(u+L)\phi'(-L)\to\phi(u).