Infinite-dimensional operator ridgelet transform

2.1. Finite-width and integral networks🔗

The finite sum and the integral representation use the same atoms. In the vector-valued case the coefficient measure has bounded variation, and integration is understood in the Bochner sense.

Definition2.1
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 6.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For a continuous activation \beta:\mathbb R\to\mathbb C, a width-N network on H with values in Y is f_N(x)=\sum_{j=1}^Nv_j\,\beta(\langle a_j,x\rangle+c_j) with outer weights v_j\in Y and parameters (a_j,c_j)\in H\times\mathbb R; the scalar case is Y=\mathbb C. Approximation is measured in the compact-open topology of C(H;Y), generated by the seminorms \|f\|_{C(K;Y)}=\sup_{x\in K}\|f(x)\|_Y over compact K\subset H.

Lean code for Definition2.1●1 definition
  • defdefined in OperatorRidgelet/Network/Defs.lean
    complete
    def OperatorRidgelet.finiteNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ} (β : ℝ → ℂ)
  (v : Fin N → Y) (a : Fin N → H) (c : Fin N → ℝ) (x : H) : Y
    def OperatorRidgelet.finiteNetwork.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ) (v : Fin N → Y)
  (a : Fin N → H) (c : Fin N → ℝ)
  (x : H) : Y
    **Definition [def:2.1]** The width-`N` network on `H` with values in `Y`,
`f_N(x) = ∑_{j} β(⟪a_j, x⟫ + c_j) • v_j`, with outer weights `v : Fin N → Y`, directions
`a : Fin N → H`, biases `c : Fin N → ℝ`, and scalar activation `β : ℝ → ℂ` (continuous in the
manuscript).  The scalar case is `Y = ℂ`.

A vector measure assigns a vector to each Borel set and is countably additive in the output norm. Its variation is |\Gamma|(E)=\sup\sum_j\|\Gamma(E_j)\|_Y, over finite Borel partitions of E; bounded variation means finite mass on the whole parameter space. Since Y is a separable Hilbert space, \Gamma(E)=\int_E h\,\mathrm d|\Gamma| with \|h\|_Y=1 almost everywhere, and the integral of a scalar function u against \Gamma means the Bochner integral \int uh\,\mathrm d|\Gamma|. A vector-valued function is Bochner integrable when it is strongly measurable, meaning an almost-everywhere limit of measurable simple functions, and its norm is integrable; integrating simple-function approximants in L^1 gives its integral. For further details, see Diestel and Uhl, Vector Measures (1977).

TheoremAux.1
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

This is the polar-decomposition fact recalled before Definition 2.2 in Section 2.1. It also supplies the sampling data before Definition 6.1 in Section 6.1. Every complex or Hilbert-space-valued measure \Gamma of bounded variation has a polar decomposition \Gamma=h|\Gamma| with \|h\|=1 |\Gamma|-almost everywhere (the Radon–Nikodym theorem for vector measures). Mathlib has the scalar Radon–Nikodym theorem but not this form; it is proved in the project's ToMathlib modules, so the density that the sampled network of Section 6 chooses always exists.

Lean code for TheoremAux.1●4 theorems
  • theoremdefined in OperatorRidgelet/ToMathlib/VectorMeasureRadonNikodym.lean
    complete
    theorem MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq.{u_1, u_2}
  {X : Type u_1} {Y : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
  (Γ : MeasureTheory.VectorMeasure X Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation] :
  ∃ g,
    (∀ᵐ (x : X) ∂Γ.variation, ‖g x‖ = 1) ∧
      Γ = Γ.variation.withDensityᵥ g
    theorem MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq.{u_1,
    u_2}
  {X : Type u_1} {Y : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℝ Y]
  [CompleteSpace Y]
  (Γ : MeasureTheory.VectorMeasure X Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation] :
  ∃ g,
    (∀ᵐ (x : X) ∂Γ.variation, ‖g x‖ = 1) ∧
      Γ = Γ.variation.withDensityᵥ g
    Polar decomposition of a finite-variation Hilbert-valued measure.
  • theoremdefined in OperatorRidgelet/Sampling/Basic.lean
    complete
    theorem OperatorRidgelet.polarDensity_spec.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Z : Type u_2} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z] [CompleteSpace Z]
  (Γ : MeasureTheory.VectorMeasure Θ Z)
  [MeasureTheory.IsFiniteMeasure Γ.variation] :
  (∀ᵐ (θ : Θ) ∂Γ.variation, ‖OperatorRidgelet.polarDensity Γ θ‖ = 1) ∧
    Γ = Γ.variation.withDensityᵥ (OperatorRidgelet.polarDensity Γ)
    theorem OperatorRidgelet.polarDensity_spec.{u_1,
    u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Z : Type u_2} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z]
  [CompleteSpace Z]
  (Γ : MeasureTheory.VectorMeasure Θ Z)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation] :
  (∀ᵐ (θ : Θ) ∂Γ.variation,
      ‖OperatorRidgelet.polarDensity Γ
            θ‖ =
        1) ∧
    Γ =
      Γ.variation.withDensityᵥ
        (OperatorRidgelet.polarDensity Γ)
    The specification of `polarDensity`: for a complex measure of finite variation the polar
decomposition exists, so `‖h‖ = 1` `|Γ|`-almost everywhere and `Γ = |Γ|.withDensityᵥ h`.
  • theoremdefined in OperatorRidgelet/Sampling/Basic.lean
    complete
    theorem OperatorRidgelet.ae_norm_polarDensity_eq_one.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Z : Type u_2} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z] [CompleteSpace Z]
  (Γ : MeasureTheory.VectorMeasure Θ Z)
  [MeasureTheory.IsFiniteMeasure Γ.variation] :
  ∀ᵐ (θ : Θ) ∂Γ.variation, ‖OperatorRidgelet.polarDensity Γ θ‖ = 1
    theorem OperatorRidgelet.ae_norm_polarDensity_eq_one.{u_1,
    u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Z : Type u_2} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z]
  [CompleteSpace Z]
  (Γ : MeasureTheory.VectorMeasure Θ Z)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation] :
  ∀ᵐ (θ : Θ) ∂Γ.variation,
    ‖OperatorRidgelet.polarDensity Γ θ‖ =
      1
    The polar density has norm one almost everywhere for the variation measure.
  • theoremdefined in OperatorRidgelet/Sampling/Basic.lean
    complete
    theorem OperatorRidgelet.withDensityᵥ_polarDensity.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Z : Type u_2} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z] [CompleteSpace Z]
  (Γ : MeasureTheory.VectorMeasure Θ Z)
  [MeasureTheory.IsFiniteMeasure Γ.variation] :
  Γ.variation.withDensityᵥ (OperatorRidgelet.polarDensity Γ) = Γ
    theorem OperatorRidgelet.withDensityᵥ_polarDensity.{u_1,
    u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Z : Type u_2} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z]
  [CompleteSpace Z]
  (Γ : MeasureTheory.VectorMeasure Θ Z)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation] :
  Γ.variation.withDensityᵥ
      (OperatorRidgelet.polarDensity Γ) =
    Γ
    Integrating the polar density against the variation recovers the vector measure.
Definition2.2
uses 1
Used by 7
Reverse dependency previews
Preview
Theorem 4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let \Gamma be a Y-valued Borel measure of bounded variation on \Theta=H\times\mathbb R with variation |\Gamma| and total variation \|\Gamma\|_{\mathrm{TV}}=|\Gamma|(\Theta). Whenever the Bochner integral exists, the integral network is S_\beta[\Gamma](x)=\int_{H\times\mathbb R}\beta(\langle a,x\rangle+c)\,\Gamma(\mathrm da,\mathrm dc); if \beta is globally Lipschitz, it suffices that \int(1+\|a\|+|c|)\,\mathrm d|\Gamma|<\infty (part i). When \Gamma=\gamma\lambda has a density \gamma with respect to a \sigma-finite reference measure \lambda, the network is also written S_\beta[\gamma] and computed as the Bochner integral of \beta(\langle a,x\rangle+c)\gamma(a,c) against \lambda (part ii).

Lean code for Definition2.2●5 declarations
  • defdefined in OperatorRidgelet/Network/Defs.lean
    complete
    def OperatorRidgelet.integralNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] [MeasurableSpace H]
  (β : ℝ → ℂ) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y) (x : H) : Y
    def OperatorRidgelet.integralNetwork.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [MeasurableSpace H] (β : ℝ → ℂ)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  (x : H) : Y
    **Definition [def:2.2]** The integral network
`S_β[Γ](x) = ∫ β(⟪a, x⟫ + c) Γ(da, dc)` of a `Y`-valued measure `Γ` on `Θ = H × ℝ`, as the
vector-measure Bochner integral with complex scalars acting on `Y`; it is `0` when the integrand
is not integrable against `Γ.variation`.
  • defdefined in OperatorRidgelet/Network/Defs.lean
    complete
    def OperatorRidgelet.totalVariation.{u_2, u_3} {Y : Type u_2}
  [NormedAddCommGroup Y] {Θ : Type u_3} [MeasurableSpace Θ]
  (Γ : MeasureTheory.VectorMeasure Θ Y) : ENNReal
    def OperatorRidgelet.totalVariation.{u_2, u_3}
  {Y : Type u_2} [NormedAddCommGroup Y]
  {Θ : Type u_3} [MeasurableSpace Θ]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  ENNReal
    The total variation `‖Γ‖_TV = |Γ|(Θ)` of a vector measure `Γ`, in `ℝ≥0∞`.
  • defdefined in OperatorRidgelet/Network/Defs.lean
    complete
    def OperatorRidgelet.integralNetworkDensity.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] [MeasurableSpace H]
  (β : ℝ → ℂ) (lam : MeasureTheory.Measure (H × ℝ)) (γ : H × ℝ → Y)
  (x : H) : Y
    def OperatorRidgelet.integralNetworkDensity.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  [MeasurableSpace H] (β : ℝ → ℂ)
  (lam : MeasureTheory.Measure (H × ℝ))
  (γ : H × ℝ → Y) (x : H) : Y
    The integral network `S_β[γ](x) = ∫ β(⟪a, x⟫ + c) γ(a, c) λ(da, dc)` of a coefficient
density `γ` with respect to a reference measure `λ` on `Θ = H × ℝ` (the manuscript's
`Γ = γ λ`), as a Bochner integral.
  • theoremdefined in OperatorRidgelet/Paper/Networks.lean
    complete
    theorem OperatorRidgelet.Paper.def_2_2_i.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {β : ℝ → ℂ} {L : NNReal}
  (hβ : LipschitzWith L β) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation]
  (hmom :
    MeasureTheory.Integrable (fun θ => 1 + ‖θ.1‖ + |θ.2|) Γ.variation)
  (x : H) : Γ.Integrable fun θ => β (inner ℝ θ.1 x + θ.2)
    theorem OperatorRidgelet.Paper.def_2_2_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {β : ℝ → ℂ}
  {L : NNReal} (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation]
  (hmom :
    MeasureTheory.Integrable
      (fun θ => 1 + ‖θ.1‖ + |θ.2|)
      Γ.variation)
  (x : H) :
  Γ.Integrable fun θ =>
    β (inner ℝ θ.1 x + θ.2)
    **Definition [def:2.2]** Integral network.  If `β` is globally Lipschitz and
`∫ (1 + ‖a‖ + |c|) d|Γ| < ∞`, then the Bochner integral defining `S_β[Γ](x)` exists for every
`x`.
  • theoremdefined in OperatorRidgelet/Paper/Networks.lean
    complete
    theorem OperatorRidgelet.Paper.def_2_2_ii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {β : ℝ → ℂ}
  (hβ : Continuous β) (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam] {γ : H × ℝ → Y}
  (hγ : MeasureTheory.Integrable γ lam) (x : H)
  (hint :
    MeasureTheory.Integrable (fun θ => β (inner ℝ θ.1 x + θ.2) • γ θ)
      lam) :
  OperatorRidgelet.integralNetwork β (lam.withDensityᵥ γ) x =
    OperatorRidgelet.integralNetworkDensity β lam γ x
    theorem OperatorRidgelet.Paper.def_2_2_ii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {β : ℝ → ℂ}
  (hβ : Continuous β)
  (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam]
  {γ : H × ℝ → Y}
  (hγ : MeasureTheory.Integrable γ lam)
  (x : H)
  (hint :
    MeasureTheory.Integrable
      (fun θ =>
        β (inner ℝ θ.1 x + θ.2) • γ θ)
      lam) :
  OperatorRidgelet.integralNetwork β
      (lam.withDensityᵥ γ) x =
    OperatorRidgelet.integralNetworkDensity
      β lam γ x
    **Definition [def:2.2]** Integral network.  For `Γ = γ λ` with a density `γ`
with respect to a σ-finite reference measure `λ`, the integral network `S_β[Γ]` is the Bochner
integral `S_β[γ](x) = ∫ β(⟪a, x⟫ + c) γ(a, c) λ(da, dc)`, whenever the latter exists.