Infinite-dimensional operator ridgelet transform

6.1. Rademacher complexity and the general approximation bound🔗

For a finite coefficient measure with V=\|\Gamma\|_{\mathrm{TV}}>0, choose its polar decomposition \Gamma=h|\Gamma|, where \|h\|_Y=1 almost everywhere, and put p=|\Gamma|/V. Draw neuron parameters independently from p; the polar density supplies the output weights. For V=0, use the zero network.

Definition6.1
Statement uses 3
Statement dependency previews
Preview
Definition 2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Definition Aux.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For a compact K\subset H, the activation-dependent Rademacher complexity is \mathfrak R_N(K;p,\beta)=\mathbb E_{\theta,\varepsilon}\sup_{x\in K}\bigl|\frac1N\sum_{j=1}^N\varepsilon_jh(\theta_j)\beta(\langle a_j,x\rangle+c_j)\bigr|, where \varepsilon_j are independent Rademacher signs; with Y-valued phases h it is \mathfrak R_N^Y(K;p,\beta). The Lean definition carries the polar data h, V, p of \Gamma, the product law p^{\otimes N} of the sample, the law of the signs, the sampled network, and the compact sup norm \|f\|_{C(K)}=\sup_{x\in K}\|f(x)\|.

Lean code for Definition6.1●8 definitions
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.compactSupNorm.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] (K : Set X) (f : X → Y) : ℝ
    def OperatorRidgelet.compactSupNorm.{u_1, u_2}
  {X : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] (K : Set X)
  (f : X → Y) : ℝ
    The compact sup norm `‖f‖_{C(K;Y)} = sup_{x ∈ K} ‖f(x)‖` of a function `f : X → Y` on a
set `K`, as the supremum of the image `{‖f x‖ : x ∈ K}` (`0` when `K` is empty or the norms are
unbounded on `K`).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarDensity.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (Γ : MeasureTheory.VectorMeasure Θ Y) : Θ → Y
    def OperatorRidgelet.polarDensity.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  Θ → Y
    The phase `h` of the polar decomposition `Γ = h |Γ|` of a `Y`-valued measure of bounded
variation: a density of `Γ` with respect to its variation measure `|Γ|` with `‖h‖ = 1`
`|Γ|`-almost everywhere, chosen when one exists, and `0` otherwise.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarWeight.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) : ℝ
    def OperatorRidgelet.polarWeight.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  ℝ
    The weight `V = ‖Γ‖_TV = |Γ|(Θ)` of the polar decomposition, as a real number
(`eq:polar-decomposition`).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarLaw.{u_1, u_2} {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) : MeasureTheory.Measure Θ
    def OperatorRidgelet.polarLaw.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  MeasureTheory.Measure Θ
    The parameter law `p = |Γ| / V` of the polar decomposition (`eq:polar-decomposition`); it
is a probability measure when `Γ ≠ 0` and the zero measure when `Γ = 0`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.sampleLaw.{u_1} {Θ : Type u_1} [MeasurableSpace Θ]
  (N : ℕ) (p : MeasureTheory.Measure Θ) :
  MeasureTheory.Measure (Fin N → Θ)
    def OperatorRidgelet.sampleLaw.{u_1}
  {Θ : Type u_1} [MeasurableSpace Θ]
  (N : ℕ) (p : MeasureTheory.Measure Θ) :
  MeasureTheory.Measure (Fin N → Θ)
    The law `p^{⊗N}` of `N` independent parameters `θ_1, …, θ_N ∼ p`, on `Fin N → Θ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.rademacherMeasure (N : ℕ) :
  MeasureTheory.Measure (Fin N → ℝ)
    def OperatorRidgelet.rademacherMeasure
  (N : ℕ) :
  MeasureTheory.Measure (Fin N → ℝ)
    The law of `N` independent Rademacher signs `ε_1, …, ε_N ∈ {-1, 1}`, represented as real
numbers: the product of `N` copies of `(δ_{-1} + δ_1)/2` on `Fin N → ℝ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.sampledNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ} (β : ℝ → ℂ) (V : ℝ)
  (h : H × ℝ → Y) (θ : Fin N → H × ℝ) : H → Y
    def OperatorRidgelet.sampledNetwork.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ) (V : ℝ)
  (h : H × ℝ → Y) (θ : Fin N → H × ℝ) :
  H → Y
    The sampled network `f_N(x) = (V/N) ∑_j β(⟪a_j, x⟫ + c_j) • h(θ_j)` (`eq:polar-network`)
of the samples `θ_j = (a_j, c_j)`, with weight `V` and phase `h`: a width-`N` network with outer
weights `(V/N) h(θ_j)`.  The scalar case is `Y = ℂ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.rademacherComplexity.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y] (N : ℕ)
  (K : Set H) (p : MeasureTheory.Measure (H × ℝ)) (β : ℝ → ℂ)
  (h : H × ℝ → Y) : ℝ
    def OperatorRidgelet.rademacherComplexity.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (N : ℕ) (K : Set H)
  (p : MeasureTheory.Measure (H × ℝ))
  (β : ℝ → ℂ) (h : H × ℝ → Y) : ℝ
    **Definition [def:6.1]** The activation-dependent Rademacher complexity
`𝔑_N(K; p, β) = 𝔼_{θ,ε} sup_{x ∈ K} ‖N⁻¹ ∑_j ε_j β(⟪a_j, x⟫ + c_j) h(θ_j)‖`
(`eq:rademacher-complexity`), with `θ_j ∼ p` independent and `ε_j` independent Rademacher
signs; `h` is the phase of the polar decomposition.  The scalar case is `Y = ℂ`, and `Y`-valued
phases give `𝔑^Y_N(K; p, β)` of Corollary `cor:6.10`.
DefinitionAux.9
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 6.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

These are the sampling definitions used across Section 6: polar data in Section 6.1, radius and moment bounds in Theorem 6.5, atomic measures in Lemma 6.7, and finite-rank projections in Corollary C.2.

The radius R_K=\sup_{x\in K}\sqrt{\|x\|^2+1} of a compact set, the second moment M_2^2=\int_{H\times\mathbb R}(\|a\|^2+|c|^2)\,p(\mathrm da,\mathrm dc), the polar data V=\|\gamma\|_{L^1(\lambda)}, p=|\gamma|\lambda/V, h=\gamma/|\gamma| of a coefficient measure \gamma\lambda and the sampled networks of \Gamma and of \gamma\lambda, the finite atomic measure \sum_jw_j\delta_{\theta_j}, and finite-rank orthogonal projections.

Lean code for DefinitionAux.9●9 definitions
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.compactRadius.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] (K : Set H) : ℝ
    def OperatorRidgelet.compactRadius.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  (K : Set H) : ℝ
    The radius `R_K = sup_{x ∈ K} √(‖x‖² + 1)` of a set `K` (Theorem `thm:6.5`).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densityWeight.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ) (γ : Θ → Y) : ℝ
    def OperatorRidgelet.densityWeight.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ)
  (γ : Θ → Y) : ℝ
    The weight `V = ‖γ‖_{L¹(λ)} = ∫ ‖γ‖ dλ` of a coefficient measure `γ λ` with a density.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densityLaw.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ) (γ : Θ → Y) : MeasureTheory.Measure Θ
    def OperatorRidgelet.densityLaw.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ)
  (γ : Θ → Y) : MeasureTheory.Measure Θ
    The parameter law `p = |γ| λ / V` of a coefficient measure `γ λ` with a density.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densityPhase.{u_1, u_2} {Θ : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (γ : Θ → Y) (θ : Θ) : Y
    def OperatorRidgelet.densityPhase.{u_1, u_2}
  {Θ : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (γ : Θ → Y) (θ : Θ) : Y
    The phase `h = γ / ‖γ‖` of a coefficient measure `γ λ` with a density (`0` where `γ`
vanishes).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarSampledNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ}
  (β : ℝ → ℂ) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  (θ : Fin N → H × ℝ) : H → Y
    def OperatorRidgelet.polarSampledNetwork.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  (θ : Fin N → H × ℝ) : H → Y
    The sampled network `eq:polar-network` of a measure `Γ` of bounded variation: the weight
`V = ‖Γ‖_TV` and the phase `h` of its polar decomposition, with samples `θ_j ∼ p = |Γ|/V`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densitySampledNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ}
  (β : ℝ → ℂ) (lam : MeasureTheory.Measure (H × ℝ)) (γ : H × ℝ → Y)
  (θ : Fin N → H × ℝ) : H → Y
    def OperatorRidgelet.densitySampledNetwork.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ)
  (lam : MeasureTheory.Measure (H × ℝ))
  (γ : H × ℝ → Y) (θ : Fin N → H × ℝ) :
  H → Y
    The sampled network `eq:polar-network` of a coefficient measure `γ λ` with a density: the
weight `V = ‖γ‖_{L¹(λ)}` and the phase `h = γ/‖γ‖`, with samples `θ_j ∼ p = |γ| λ / V`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.secondMoment.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [MeasurableSpace H]
  (p : MeasureTheory.Measure (H × ℝ)) : ℝ
    def OperatorRidgelet.secondMoment.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [MeasurableSpace H]
  (p : MeasureTheory.Measure (H × ℝ)) : ℝ
    The second moment `M₂² = ∫ (‖a‖² + |c|²) p(da, dc)` (`eq:second-moment`) of a parameter
law `p`; `M₂` is its square root.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.atomicMeasure.{u_1, u_2} {H : Type u_1}
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y] {n : ℕ}
  (w : Fin n → Y) (θ : Fin n → H × ℝ) :
  MeasureTheory.VectorMeasure (H × ℝ) Y
    def OperatorRidgelet.atomicMeasure.{u_1, u_2}
  {H : Type u_1} [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  {n : ℕ} (w : Fin n → Y)
  (θ : Fin n → H × ℝ) :
  MeasureTheory.VectorMeasure (H × ℝ) Y
    The finite atomic `Y`-valued measure `∑_j w_j δ_{θ_j}` on `H × ℝ`.
  • structure(2 fields)defined in OperatorRidgelet/Sampling/Defs.lean
    complete
    structure OperatorRidgelet.IsFiniteRankProjection.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (P : H →L[ℝ] H) : Prop
    structure OperatorRidgelet.IsFiniteRankProjection.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (P : H →L[ℝ] H) : Prop
    `P` is a finite-rank orthogonal projection: a self-adjoint idempotent with
finite-dimensional range.

    Fields

    isStarProjection : IsStarProjection P
    `P` is an orthogonal projection: `P^* = P = P²`. 
    finiteDimensional_range : FiniteDimensional ℝ ↥(↑P).range
    The range of `P` is finite dimensional.
Lemma6.2
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 6.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let X be a separable Banach space, p a probability measure, and \Phi\in L^1(p;X). For independent samples \theta_j\sim p and independent Rademacher signs \varepsilon_j, \mathbb E\|N^{-1}\sum_{j=1}^N\varepsilon_j\Phi(\theta_j)\|_X\to0. Moreover, for N\ge1 and m=\int\Phi\,\mathrm dp, \mathbb E\|N^{-1}\sum_{j=1}^N\Phi(\theta_j)-m\|_X\le2\mathbb E\|N^{-1}\sum_{j=1}^N\varepsilon_j\Phi(\theta_j)\|_X.

Lean code for Lemma6.2●2 theorems
  • theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_6_2_i.{u_1, u_2} {Ω : Type u_1}
  {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p] {Φ : Ω → E}
  (hint : MeasureTheory.Integrable Φ p) :
  Filter.Tendsto
    (fun N =>
      ∫ (z : (Fin N → Ω) × (Fin N → ℝ)),
        ‖(↑N)⁻¹ •
            ∑ j,
              z.2 j •
                Φ
                  (z.1
                    j)‖ ∂(MeasureTheory.Measure.pi fun x => p).prod
          (OperatorRidgelet.rademacherMeasure N))
    Filter.atTop (nhds 0)
    theorem OperatorRidgelet.Paper.lem_6_2_i.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSpace E]
  [BorelSpace E]
  [SecondCountableTopology E]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Φ : Ω → E}
  (hint : MeasureTheory.Integrable Φ p) :
  Filter.Tendsto
    (fun N =>
      ∫ (z : (Fin N → Ω) × (Fin N → ℝ)),
        ‖(↑N)⁻¹ •
            ∑ j,
              z.2 j •
                Φ
                  (z.1
                    j)‖ ∂(MeasureTheory.Measure.pi
              fun x => p).prod
          (OperatorRidgelet.rademacherMeasure
            N))
    Filter.atTop (nhds 0)
    **Lemma [lem:6.2](i).** The signed empirical mean of a
Bochner-integrable separable Banach-valued atom tends to zero in expected norm.
  • theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_6_2_ii.{u_1, u_2} {Ω : Type u_1}
  {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E] (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p] {Φ : Ω → E}
  (hint : MeasureTheory.Integrable Φ p) (N : ℕ) :
  ((↑N)⁻¹ *
      ∫ (ω : Fin N → Ω),
        ‖∑ j, Φ (ω j) -
            ↑N •
              ∫ (x : Ω), Φ x ∂p‖ ∂MeasureTheory.Measure.pi fun x => p) ≤
    2 * (↑N)⁻¹ *
      ∑ σ,
        (2 ^ N)⁻¹ *
          ∫ (ω : Fin N → Ω),
            ‖∑ j,
                (if σ j = true then 1 else -1) •
                  Φ (ω j)‖ ∂MeasureTheory.Measure.pi fun x => p
    theorem OperatorRidgelet.Paper.lem_6_2_ii.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Φ : Ω → E}
  (hint : MeasureTheory.Integrable Φ p)
  (N : ℕ) :
  ((↑N)⁻¹ *
      ∫ (ω : Fin N → Ω),
        ‖∑ j, Φ (ω j) -
            ↑N •
              ∫ (x : Ω),
                Φ
                  x ∂p‖ ∂MeasureTheory.Measure.pi
          fun x => p) ≤
    2 * (↑N)⁻¹ *
      ∑ σ,
        (2 ^ N)⁻¹ *
          ∫ (ω : Fin N → Ω),
            ‖∑ j,
                (if σ j = true then 1
                  else -1) •
                  Φ
                    (ω
                      j)‖ ∂MeasureTheory.Measure.pi
              fun x => p
    **Lemma [lem:6.2](ii).** Symmetrization of the empirical mean.
The finite sum averages over the uniform Boolean sign vectors; the inverse width outside
the norm is the equivalent normalization of the manuscript's empirical averages.
Proof for Lemma 6.2
uses 0

Approximate \Phi in L^1 by a simple function \Psi=\sum_{k=1}^Jx_k\mathbf1_{E_k}. The signed-average error has expected norm at most \|\Phi-\Psi\|_{L^1}. For \Psi, the scalar second-moment identity and Cauchy–Schwarz bound the expected norm by \sum_k\|x_k\|\sqrt{p(E_k)/N}, which tends to zero. For symmetrization, introduce a ghost sample, apply Jensen, and insert independent signs using exchangeability of each pair. The triangle inequality gives the factor two. Bochner integrability justifies every expectation.

Theorem6.3
Statement uses 2
Statement dependency previews
Preview
Definition 2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 6.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Whenever the atoms x\mapsto h(\theta)\beta(\langle a,x\rangle+c) are strongly measurable and integrable as C(K)-valued functions, the sampled network satisfies \mathbb E\|f_N-f\|_{C(K)}\le2V\,\mathfrak R_N(K;p,\beta).

Lean code for Theorem6.3●1 theorem
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.thm_6_3.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (β : ℝ → ℂ) (Γ : MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γ)]
  {K : Set H} (hK : IsCompact K)
  (Φ : H × ℝ → BoundedContinuousFunction ↑K ℂ)
  (hΦ :
    ∀ (θ : H × ℝ) (x : ↑K),
      (Φ θ) x =
        β (inner ℝ θ.1 ↑x + θ.2) * OperatorRidgelet.polarDensity Γ θ)
  (hint : MeasureTheory.Integrable Φ (OperatorRidgelet.polarLaw Γ))
  {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork β Γ θ x -
          OperatorRidgelet.integralNetwork β Γ
            x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) ≤
    2 * OperatorRidgelet.polarWeight Γ *
      OperatorRidgelet.rademacherComplexity N K
        (OperatorRidgelet.polarLaw Γ) β
        (OperatorRidgelet.polarDensity Γ)
    theorem OperatorRidgelet.Paper.thm_6_3.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (β : ℝ → ℂ)
  (Γ :
    MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γ)]
  {K : Set H} (hK : IsCompact K)
  (Φ :
    H × ℝ →
      BoundedContinuousFunction ↑K ℂ)
  (hΦ :
    ∀ (θ : H × ℝ) (x : ↑K),
      (Φ θ) x =
        β (inner ℝ θ.1 ↑x + θ.2) *
          OperatorRidgelet.polarDensity Γ
            θ)
  (hint :
    MeasureTheory.Integrable Φ
      (OperatorRidgelet.polarLaw Γ))
  {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            β Γ θ x -
          OperatorRidgelet.integralNetwork
            β Γ
            x ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) ≤
    2 * OperatorRidgelet.polarWeight Γ *
      OperatorRidgelet.rademacherComplexity
        N K (OperatorRidgelet.polarLaw Γ)
        β
        (OperatorRidgelet.polarDensity Γ)
    **Theorem [thm:6.3]** Compact-open approximation 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, β)`.
Proof for Theorem 6.3
uses 1

Apply Lemma 6.2 in C(K) and multiply by V. The same lemma gives convergence to zero. This step needs only Bochner integrability.