8.13.1. Lemma F.1 — Hilbert--Schmidt reduction (lem:hs-reduction)🔗

Blueprint node: Lemma 1.2.3. Status: verified (its Lean theorem is verified).

Formalization note. Mathlib has no Hilbert–Schmidt class: hsNormSq is the supremum over finite orthonormal families of ∑‖Ae‖², so IsHilbertSchmidt is basis-free; 𝓛₂(H) is the set {A | IsHilbertSchmidt A} of bounded operators. Neurons are the elements of C(H, ℝ) (compact-open topology) whose function is operatorNeuron σ ℓ A b; closures are of the ℝ-span as a set.

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

/-- **Lemma [lem:hs-reduction]** Hilbert–Schmidt reduction.  For globally Lipschitz `σ`, the
spans of the operator neurons with `A ∈ 𝓛(H)` and with `A ∈ 𝓛₂(H)` have the same compact-open
closure in `C(H; ℝ)`. -/
theorem lem_hs_reduction [CompleteSpace H] [SecondCountableTopology H] {σ : H → H} {L : ℝ≥0}
    (hσ : LipschitzWith L σ) :
    closure (Submodule.span ℝ (operatorNeuronSet σ Set.univ) : Set C(H, ℝ)) =
      closure (Submodule.span ℝ (operatorNeuronSet σ {A | IsHilbertSchmidt A}) :
        Set C(H, ℝ)) := by

Status: verified by comparator.

8.13.2. Lemma F.2 — Exact rank-one lift (lem:rank-one-lift)🔗

Blueprint node: Lemma 1.2.4. Status: verified (all 7 Lean theorems verified).

Formalization note. A_a = rankOneLift ψ a, b_c = biasLift ψ c, π_ψ = operatorParameterMap ψ, J_ψ = operatorRidgeletSection ψ (module OperatorValuedRidgelet). Part i holds without ψ ≠ 0 (A_0 = 0). Part v states continuity of J_ψ into 𝓛₂(H) × H as: the Hilbert–Schmidt norm of the operator increment plus the norm of the bias increment tends to 0 (the space 𝓛₂(H) is not bundled as a normed space); continuity for the operator norm is continuous_operatorRidgeletSection. Parts vi (integral networks, Y = ℂ) and vii (finite-width networks, Y a complex Hilbert space) are the exact lifts with ⟪ℓ, z⟫ = 1; z ≠ 0 is implied by the normalization and is not assumed separately. Part vi needs no integrability hypothesis because J_ψ is a closed embedding.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  `A_a = ‖ψ‖⁻² ψ ⊗ a` is
Hilbert–Schmidt. -/
theorem lem_rank_one_lift_i (ψ a : H) : IsHilbertSchmidt (rankOneLift ψ a) := by

Status: verified by comparator.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  `‖A_a‖_{𝓛₂} = ‖a‖ / ‖ψ‖`. -/
theorem lem_rank_one_lift_ii {ψ : H} (hψ : ψ ≠ 0) (a : H) :
    hsNorm (rankOneLift ψ a) = ‖a‖ / ‖ψ‖ := by

Status: verified by comparator.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  `‖b_c‖ = |c| / ‖ψ‖`. -/
theorem lem_rank_one_lift_iii {ψ : H} (hψ : ψ ≠ 0) (c : ℝ) :
    ‖biasLift ψ c‖ = |c| / ‖ψ‖ := by

Status: verified by comparator.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  `π_ψ(A_a, b_c) = (a, c)`. -/
theorem lem_rank_one_lift_iv [CompleteSpace H] {ψ : H} (hψ : ψ ≠ 0) (a : H) (c : ℝ) :
    operatorParameterMap ψ (operatorRidgeletSection ψ (a, c)) = (a, c) := by

Status: verified by comparator.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  The section `J_ψ(a, c) = (A_a, b_c)` is
continuous into `𝓛₂(H) × H`: the Hilbert–Schmidt distance of the operator components plus the
distance of the biases tends to `0` at every `(a, c)`. -/
theorem lem_rank_one_lift_v {ψ : H} (hψ : ψ ≠ 0) (a : H) (c : ℝ) :
    Filter.Tendsto
      (fun p : H × ℝ =>
        hsNorm (rankOneLift ψ p.1 - rankOneLift ψ a) + ‖biasLift ψ p.2 - biasLift ψ c‖)
      (𝓝 (a, c)) (𝓝 0) := by

Status: verified by comparator.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  Every scalar integral network with
activation `β` lifts exactly to the operator architecture with activation `σ_β` and readout
normalized by `⟪ℓ, z⟫ = 1`: `S_op[(J_ψ)_# Γ] = S_β[Γ]`. -/
theorem lem_rank_one_lift_vi [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
    [BorelSpace H] (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0) (hℓz : inner ℝ ℓ z = 1)
    (Γ : ComplexMeasure (ScalarRidgeParameter H)) :
    operatorSynthesis (rankOneActivation β ψ z) ℓ (Γ.map (operatorRidgeletSection ψ)) =
      integralNetwork (fun t => (β t : ℂ)) Γ := by

Status: verified by comparator.

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

/-- **Lemma [lem:rank-one-lift]** Exact rank-one lift.  Every scalar finite-width network with
activation `β` lifts exactly to the operator architecture with activation `σ_β`, parameters
`(A_{a_j}, b_{c_j})`, and readout normalized by `⟪ℓ, z⟫ = 1`. -/
theorem lem_rank_one_lift_vii [CompleteSpace H] {Y : Type*} [NormedAddCommGroup Y]
    [InnerProductSpace ℂ Y] [CompleteSpace Y] (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0)
    (hℓz : inner ℝ ℓ z = 1) {N : ℕ} (v : Fin N → Y) (a : Fin N → H) (c : Fin N → ℝ) :
    operatorFiniteNetwork (rankOneActivation β ψ z) ℓ v (fun j => rankOneLift ψ (a j))
        (fun j => biasLift ψ (c j)) =
      finiteNetwork (fun t => (β t : ℂ)) v a c := by

Status: verified by comparator.

8.13.3. Proposition F.3 — Compact-open universality by finite-dimensional reduction (prop:scalar-universality)🔗

Blueprint node: Proposition 1.2.5. Status: verified (all 2 Lean theorems verified).

Formalization note. 'Not a polynomial' is ¬ IsPolynomialFun β (β is not the evaluation of any Polynomial ℝ); density is Dense of the ℝ-span in C(H, ℝ) with the compact-open topology; H is assumed second countable (separable) as in the manuscript's standing assumptions.

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

/-- **Proposition [prop:scalar-universality]** Compact-open universality by finite-dimensional
reduction.  For continuous non-polynomial `β : ℝ → ℝ`, finite linear combinations of
`β(⟪a, x⟫ + c)` are dense in `C(H; ℝ)` for uniform convergence on compact sets. -/
theorem prop_scalar_universality_i [CompleteSpace H] [SecondCountableTopology H] {β : ℝ → ℝ}
    (hβ : Continuous β) (hpoly : ¬ IsPolynomialFun β) :
    Dense (Submodule.span ℝ (ridgeSet (H := H) β) : Set C(H, ℝ)) := by

Status: verified by comparator.

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

/-- **Proposition [prop:scalar-universality]** Compact-open universality by finite-dimensional
reduction.  For continuous non-polynomial `β : ℝ → ℝ` and nonzero `ψ, z`, finite linear
combinations of the operator neurons with the rank-one activation `σ_β` and Hilbert–Schmidt
parameters are dense in `C(H; ℝ)` for uniform convergence on compact sets. -/
theorem prop_scalar_universality_ii [CompleteSpace H] [SecondCountableTopology H] {β : ℝ → ℝ}
    (hβ : Continuous β) (hpoly : ¬ IsPolynomialFun β) {ψ z : H} (hψ : ψ ≠ 0) (hz : z ≠ 0) :
    Dense (Submodule.span ℝ
      (operatorNeuronSet (rankOneActivation β ψ z) {A | IsHilbertSchmidt A}) : Set C(H, ℝ)) := by

Status: verified by comparator.

8.13.4. Lemma F.4 — Bounded synthesis and exact transport of measures (lem:measure-transport)🔗

Blueprint node: Lemma 1.2.6. Status: verified (all 5 Lean theorems verified).

Formalization note. Γ_op is a ComplexMeasure on (H →L[ℝ] H) × H (Borel for the operator norm) with finite variation, carried by 𝓛₂(H) × H (∀ᵐ p ∂Γop.variation, IsHilbertSchmidt p.1) and with Integrable (fun p => 1 + hsNorm p.1 + ‖p.2‖) Γop.variation; the Borel σ-algebra of the Hilbert–Schmidt norm on 𝓛₂(H) coincides with the trace of the operator-norm Borel σ-algebra (both separable metrizable, continuous injective identity). S_op integrates the real neuron as a complex-valued function. Parts i and iii hold for every ψ (ψ ≠ 0 is not used) and are stated without it, as in the manuscript, whose parts (i)–(iii) carry exactly the hypotheses each one needs; part ii holds for every complex measure (Mathlib variation_map_le) and is stated without the other hypotheses; part iii uses r_K = sSup (‖·‖ '' K) and Lip(β) = any L with LipschitzWith L β; part iv needs only ψ ≠ 0; part v (S_op (J_ψ)_# Γ = S_β Γ) is proved without the moment condition because J_ψ is a closed embedding, so that hypothesis is dropped.

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

/-- **Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.  For
real globally Lipschitz `β`, `ψ ≠ 0`, a finite complex Borel measure `Γ_op` on `𝓛₂(H) × H`
with `∫ (1 + ‖A‖_{𝓛₂} + ‖b‖) d|Γ_op| < ∞`, and readout normalized by `⟪ℓ, z⟫ = 1`,
`S_op Γ_op = S_β[(π_ψ)_# Γ_op]`. -/
theorem lem_measure_transport_i [CompleteSpace H] [SecondCountableTopology H]
    [MeasurableSpace H] [BorelSpace H] {β : ℝ → ℝ} {L : ℝ≥0} (hβ : LipschitzWith L β)
    (ψ : H) (Γop : ComplexMeasure (OperatorRidgeParameter H))
    [IsFiniteMeasure Γop.variation] (hHS : ∀ᵐ p ∂Γop.variation, IsHilbertSchmidt p.1)
    (hmom : Integrable (fun p : OperatorRidgeParameter H => 1 + hsNorm p.1 + ‖p.2‖)
      Γop.variation)
    {ℓ z : H} (hℓz : inner ℝ ℓ z = 1) :
    operatorSynthesis (rankOneActivation β ψ z) ℓ Γop =
      integralNetwork (fun t => (β t : ℂ)) (Γop.map (operatorParameterMap ψ)) := by

Status: verified by comparator.

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

/-- **Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.  The
variation of the pushforward is dominated by the pushforward of the variation:
`|(π_ψ)_# Γ_op| ≤ (π_ψ)_# |Γ_op|`. -/
theorem lem_measure_transport_ii [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] (ψ : H)
    (Γop : ComplexMeasure (OperatorRidgeParameter H)) :
    (Γop.map (operatorParameterMap ψ)).variation ≤
      Γop.variation.map (operatorParameterMap ψ) := by

Status: verified by comparator.

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

/-- **Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.  For
compact `K` with `r_K = sup_K ‖x‖`,
`‖S_op Γ_op‖_{C(K)} ≤ ∫ [|β(0)| + Lip(β) ‖ψ‖ (r_K ‖A‖_{𝓛₂} + ‖b‖)] d|Γ_op|`. -/
theorem lem_measure_transport_iii [CompleteSpace H] [SecondCountableTopology H]
    [MeasurableSpace H] [BorelSpace H] {β : ℝ → ℝ} {L : ℝ≥0} (hβ : LipschitzWith L β)
    (ψ : H) (Γop : ComplexMeasure (OperatorRidgeParameter H))
    [IsFiniteMeasure Γop.variation] (hHS : ∀ᵐ p ∂Γop.variation, IsHilbertSchmidt p.1)
    (hmom : Integrable (fun p : OperatorRidgeParameter H => 1 + hsNorm p.1 + ‖p.2‖)
      Γop.variation)
    {ℓ z : H} (hℓz : inner ℝ ℓ z = 1) {K : Set H} (hK : IsCompact K) :
    ∀ x ∈ K, ‖operatorSynthesis (rankOneActivation β ψ z) ℓ Γop x‖ ≤
      ∫ p, (|β 0| + (L : ℝ) * ‖ψ‖ * (sSup ((fun y : H => ‖y‖) '' K) * hsNorm p.1 + ‖p.2‖))
        ∂Γop.variation := by

Status: verified by comparator.

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

/-- **Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.
Conversely, `(π_ψ)_# (J_ψ)_# Γ = Γ`. -/
theorem lem_measure_transport_iv [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] {ψ : H}
    (hψ : ψ ≠ 0) (Γ : ComplexMeasure (ScalarRidgeParameter H)) :
    (Γ.map (operatorRidgeletSection ψ)).map (operatorParameterMap ψ) = Γ := by

Status: verified by comparator.

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

/-- **Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.
Conversely, `S_op (J_ψ)_# Γ = S_β Γ` with readout normalized by `⟪ℓ, z⟫ = 1`. -/
theorem lem_measure_transport_v [CompleteSpace H] [SecondCountableTopology H]
    [MeasurableSpace H] [BorelSpace H] (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0)
    (hℓz : inner ℝ ℓ z = 1) (Γ : ComplexMeasure (ScalarRidgeParameter H)) :
    operatorSynthesis (rankOneActivation β ψ z) ℓ (Γ.map (operatorRidgeletSection ψ)) =
      integralNetwork (fun t => (β t : ℂ)) Γ := by

Status: verified by comparator.