8.2.1. Definition 2.1 — Finite-width network (def:finite-network)🔗

Blueprint node: Definition 1.1.1. Status: defined (definitions only, nothing for comparator to check).

Formalization note. Width-N network with Fin N-indexed parameters; Y a complex Banach space in the definition (the manuscript's Y is a separable complex Hilbert space).

OperatorRidgelet.finiteNetwork: definition in the library (def in OperatorRidgelet/Network/Defs.lean); see the Lean panel of the Blueprint node above.

8.2.2. Definition 2.2 — Integral network (def:integral-network)🔗

Blueprint node: Definition 1.1.2. Status: verified (all 2 Lean theorems verified).

Formalization note. A Y-valued Borel measure of bounded variation is a Mathlib VectorMeasure (H × ℝ) Y with [IsFiniteMeasure Γ.variation]; the Bochner integral is VectorMeasure.integral with the pairing lsmul ℝ ℂ, which is 0 when the integrand is not integrable ('whenever the Bochner integral exists'). The moment condition is encoded as Integrable (fun θ => 1 + ‖θ.1‖ + |θ.2|) Γ.variation. Part i: Lipschitz β and the moment condition give integrability; part ii: the density case Γ = λ.withDensityᵥ γ agrees with the Bochner integral integralNetworkDensity (stated with the integrability of the integrand as hypothesis).

OperatorRidgelet.integralNetwork: definition in the library (def in OperatorRidgelet/Network/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.totalVariation: definition in the library (def in OperatorRidgelet/Network/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.integralNetworkDensity: definition in the library (def in OperatorRidgelet/Network/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.Paper.def_integral_network_i, theorem in Challenge/Networks.lean:

/-- **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`. -/
theorem def_integral_network_i [MeasurableSpace H] [BorelSpace H] {Y : Type*}
    [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] {β : ℝ → ℂ} {L : ℝ≥0}
    (hβ : LipschitzWith L β) (Γ : VectorMeasure (H × ℝ) Y) [IsFiniteMeasure Γ.variation]
    (hmom : Integrable (fun θ : H × ℝ => 1 + ‖θ.1‖ + |θ.2|) Γ.variation) (x : H) :
    Γ.Integrable fun θ : H × ℝ => β (inner ℝ θ.1 x + θ.2) := by

Status: verified by comparator.

OperatorRidgelet.Paper.def_integral_network_ii, theorem in Challenge/Networks.lean:

/-- **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. -/
theorem def_integral_network_ii [MeasurableSpace H] [BorelSpace H] {Y : Type*}
    [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] {β : ℝ → ℂ}
    (hβ : Continuous β) (lam : Measure (H × ℝ)) [SigmaFinite lam] {γ : H × ℝ → Y}
    (hγ : Integrable γ lam) (x : H)
    (hint : Integrable (fun θ : H × ℝ => β (inner ℝ θ.1 x + θ.2) • γ θ) lam) :
    integralNetwork β (lam.withDensityᵥ γ) x = integralNetworkDensity β lam γ x := by

Status: verified by comparator.