1.1. Finite-width and integral networks🔗

Definition1.1.1

uses 0

Used by 4

Reverse dependency previews

Preview

Definition 1.2.2

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 Definition1.1.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:finite-network]** 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 = ℂ`.

Definition1.1.2

uses 0

Used by 11

Reverse dependency previews

Preview

Definition 1.2.2

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 Definition1.1.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:integral-network]** 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_integral_network_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_integral_network_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:integral-network]** 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_integral_network_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_integral_network_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:integral-network]** 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.