8.6. Manuscript Section 6🔗

8.6.1. Definition 6.1 — Activation-dependent Rademacher complexity (`def:rademacher-complexity`)🔗

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

Formalization note. The sample space of N i.i.d. parameters is Fin N → H × ℝ with the product measure sampleLaw N p = Measure.pi (fun _ => p); Rademacher signs are real coordinates ε : Fin N → ℝ with the law rademacherMeasure N = Measure.pi of (δ_{-1} + δ_1)/2; 𝔑_N(K;p,β) = rademacherComplexity N K p β h is the Bochner integral over the product law of sup_{x∈K} ‖N⁻¹ Σ ε_j β(⟨a_j,x⟩+c_j) h(θ_j)‖, polymorphic in the output space (Y-valued h gives 𝔑^Y_N). The polar decomposition Γ = h|Γ| of a VectorMeasure of finite variation is polarDensity Γ = h (a density of Γ w.r.t. Γ.variation with ‖h‖ = 1 a.e., chosen when one exists, junk 0 otherwise), polarWeight Γ = V = ‖Γ‖_TV, polarLaw Γ = p = |Γ|/V (the zero measure when Γ = 0, the manuscript's zero network). The sampled network eq:polar-network is sampledNetwork β V h θ = finiteNetwork with outer weights (V/N) h(θ_j). ‖·‖_{C(K)} is compactSupNorm K f = sSup ((‖f ·‖) '' K).

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

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

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

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

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

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

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

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

8.6.2. Theorem 6.2 — General compact-open sampling bound (`thm:general-rademacher`)🔗

Blueprint node: Theorem 5.1.4. Status: verified (its Lean theorem is verified).

Formalization note. 'The atoms are measurable and integrably bounded in C(K)' is encoded as a Bochner-integrable map Φ : H × ℝ → (K →ᵇ ℂ) (BoundedContinuousFunction on the subtype K) with respect to p whose values are the atoms h(θ)β(⟨a,·⟩+c) on K. Expectation is the Bochner integral over sampleLaw N (polarLaw Γ) of compactSupNorm K (f_N θ − S_β Γ); N > 0 is assumed (the bound is void for N = 0). The theorem is stated with f = integralNetwork β Γ, which is the vector-measure integral (0 if the integrand is not integrable) — under the hypothesis it is the Bochner integral.

OperatorRidgelet.Paper.thm_general_rademacher, theorem in Challenge/Sampling.lean:

/-- **Theorem [thm:general-rademacher]** General compact-open sampling bound.  Whenever the
atoms `x ↦ h(θ) β(⟪a, x⟫ + c)` are measurable and integrably bounded in `C(K)` (they are the
values of a Bochner-integrable map `Φ : Θ → C(K)`), the sampled network of the polar
decomposition of `Γ` satisfies `𝔼‖f_N − f‖_{C(K)} ≤ 2V 𝔑_N(K; p, β)`. -/
theorem thm_general_rademacher [MeasurableSpace H] [BorelSpace H] (β : ℝ → ℂ)
    (Γ : ComplexMeasure (H × ℝ)) [IsFiniteMeasure Γ.variation] {K : Set H} (hK : IsCompact K)
    (Φ : H × ℝ → (K →ᵇ ℂ))
    (hΦ : ∀ θ : H × ℝ, ∀ x : K, Φ θ x = β (⟪θ.1, (x : H)⟫ + θ.2) * polarDensity Γ θ)
    (hint : Integrable Φ (polarLaw Γ)) {N : ℕ} (hN : 0 < N) :
    ∫ θ, compactSupNorm K (fun x => polarSampledNetwork β Γ θ x - integralNetwork β Γ x)
        ∂sampleLaw N (polarLaw Γ) ≤
      2 * polarWeight Γ * rademacherComplexity N K (polarLaw Γ) β (polarDensity Γ) := by