8.11.1. Lemma D.1 — Qualitative sampling of integrable Banach-valued atoms (lem:banach-rademacher-vanishing)🔗

Blueprint node: Lemma 5.1.3. Status: verified (all 2 Lean theorems verified).

OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i, theorem in Challenge/SamplingRevision.lean:

/-- **Lemma [lem:banach-rademacher-vanishing](i).** The signed empirical mean of a
Bochner-integrable separable Banach-valued atom tends to zero in expected norm. -/
theorem lem_banach_rademacher_vanishing_i {Ω E : Type*} [MeasurableSpace Ω]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    (p : Measure Ω) [IsProbabilityMeasure p] {Φ : Ω → E} (hint : Integrable Φ p) :
    Tendsto (fun N : ℕ => ∫ z : (Fin N → Ω) × (Fin N → ℝ),
      ‖(N : ℝ)⁻¹ • ∑ j, z.2 j • Φ (z.1 j)‖
        ∂((Measure.pi fun _ : Fin N => p).prod (rademacherMeasure N))) atTop (𝓝 0) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii, theorem in Challenge/SamplingRevision.lean:

/-- **Lemma [lem:banach-rademacher-vanishing](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. -/
theorem lem_banach_rademacher_vanishing_ii {Ω E : Type*} [MeasurableSpace Ω]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (p : Measure Ω) [IsProbabilityMeasure p] {Φ : Ω → E} (hint : Integrable Φ p) (N : ℕ) :
    (N : ℝ)⁻¹ *
        (∫ ω, ‖∑ j : Fin N, Φ (ω j) - (N : ℝ) • ∫ x, Φ x ∂p‖
          ∂(Measure.pi fun _ : Fin N => p)) ≤
      2 * (N : ℝ)⁻¹ * ∑ σ : Fin N → Bool, (2 ^ N : ℝ)⁻¹ *
        (∫ ω, ‖∑ j : Fin N, (if σ j then (1 : ℝ) else -1) • Φ (ω j)‖
          ∂(Measure.pi fun _ : Fin N => p)) := by

Status: verified by comparator.

8.11.2. Lemma D.2 — A two-coordinate Rademacher comparison (lem:two-coordinate-comparison)🔗

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

Formalization note. New in the 2026-09-13 revision; taken from supp.tex supp:lem:supp-two-coordinate-comparison. Two-coordinate Rademacher comparison behind the Hilbert-valued uniform bound of thm:lipschitz-barron. The Lean statement writes the Rademacher averages as uniform averages over the Boolean sign vectors Fin N → Bool and boundedness as ∃ C, ∀ s, |f s| ≤ C; the supremum is the ⨆ over an arbitrary nonempty index type, as in the manuscript, which no longer assumes countability: the averages are finite, so no measurability of the supremum is at issue.

OperatorRidgelet.Paper.lem_two_coordinate_comparison, theorem in Challenge/SamplingRevision.lean:

/-- **Lemma [lem:two-coordinate-comparison]** A two-coordinate Rademacher comparison.  For
bounded `ψ_i, u_i, v_i` on a nonempty set `S` whose increments satisfy
`|ψ_i(s) − ψ_i(t)| ≤ |u_i(s) − u_i(t)| + |v_i(s) − v_i(t)|`, the Rademacher average of
`sup_s ∑_i ε_i ψ_i(s)` is at most twice the average of
`sup_s ∑_i (ε_{i1} u_i(s) + ε_{i2} v_i(s))` over two independent sign vectors.  The averages
are the uniform averages over the Boolean sign vectors. -/
theorem lem_two_coordinate_comparison {S : Type*} [Nonempty S] {N : ℕ}
    {ψ u v : Fin N → S → ℝ} (hψ : ∀ i, ∃ C, ∀ s, |ψ i s| ≤ C)
    (hu : ∀ i, ∃ C, ∀ s, |u i s| ≤ C) (hv : ∀ i, ∃ C, ∀ s, |v i s| ≤ C)
    (hincr : ∀ i s t, |ψ i s - ψ i t| ≤ |u i s - u i t| + |v i s - v i t|) :
    (2 ^ N : ℝ)⁻¹ * ∑ ε : Fin N → Bool, ⨆ s, ∑ i, (if ε i then (1 : ℝ) else -1) * ψ i s ≤
      2 * ((2 ^ N : ℝ)⁻¹ * (2 ^ N : ℝ)⁻¹ *
        ∑ ε₁ : Fin N → Bool, ∑ ε₂ : Fin N → Bool, ⨆ s,
          ∑ i, ((if ε₁ i then (1 : ℝ) else -1) * u i s +
            (if ε₂ i then (1 : ℝ) else -1) * v i s)) := by

Status: verified by comparator.

8.11.3. Lemma D.3 — Densities that are regular along rays (lem:ray-regular-examples)🔗

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

Formalization note. 'For every band-pass ρ' is quantified together with every frequency window I of ρ (IsFrequencyWindow ρ I). Part a (Gaussian type) needs the Gaussian mixture ν_α and Q and is stated with S : H →L[ℝ] H self-adjoint with θ⟨Qξ,ξ⟩ ≤ ⟨Sξ,ξ⟩ (positivity follows), and q an MvPolynomial with complex coefficients in k bounded linear functionals ℓ_i and in κ(ξ) = ⟨Sξ,ξ⟩ (variable index Option (Fin k), none ↦ κ); each ℓ_i is dominated by the quadratic form, (ℓ_i ξ)² ≤ C_i ⟨Sξ,ξ⟩ (hypothesis hℓ), without which q e^{-κ/2} need not be bounded. The proof is the reduction lemma isRegularAlongRays_of_gaussian_decay (boundedness, measurability, smoothness along rays, and the pointwise derivative bound sup_{ω∈I}|∂_ω^k G(ωa)| ≤ C_k (1+‖a‖)^{p_k} e^{-r²θ⟨Qa,a⟩/2} are proved outright) applied to the Gaussian-decay integrability of lem:gaussian-decay (i). Part b_i: φ ∈ C_c^∞(ℝ) is ContDiff ℝ ⊤ φ with compact support (complex valued); b_ii: 'C^∞ along rays' is read as in def:ray-regular (smooth on an open neighbourhood of I for every direction), 'vanishes outside a bounded set' as G ξ = 0 for ‖ξ‖ > R₀, and the derivative bounds are sup over ω ∈ I ≤ C_k (1+‖a‖)^{p_k}; both b parts use ν_α (finite on bounded sets). Part c_i (finite linear combinations) and c_ii (Bochner integrals ∫ G_y m(dy)) are stated for a general ν; in c_ii the measurable family is Measurable (uncurry G), with a uniform sup bound on G_y, a common open neighbourhood U of I on which every ray is smooth, and for each order k a finite-valued y-independent majorant h : H → NNReal of rayDerivBound U (G_y) k whose weighted integral ∫ (1+‖a‖)^{k+2} h dν is finite. Taking h to be the cumulative maximum of the manuscript derivative bounds makes the formulations equivalent. Bounds only over I or extended-valued majorants on null directions do not justify differentiation: a family of rays whose derivative majorants are finite only off a null set has no differentiable integral.

OperatorRidgelet.Paper.lem_ray_regular_examples_a, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Gaussian-type
densities `G(ξ) = q(ξ) e^{-κ(ξ)/2}`, `κ(ξ) = ⟨Sξ,ξ⟩` with `S` a bounded positive operator with
`S ≥ θQ`, `θ > 0`, and `q` a polynomial in `κ(ξ)` and in finitely many bounded linear
functionals `ℓ_i` of `ξ` dominated by the quadratic form, `|ℓ_i(ξ)|² ≤ C_i κ(ξ)`, are regular
along rays for every band-pass `ρ` (and every frequency window of `ρ`). -/
theorem lem_ray_regular_examples_a (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (S : H →L[ℝ] H)
    (hS : IsSelfAdjoint S) {θ : ℝ} (hθ : 0 < θ) (hSQ : ∀ ξ, θ * ⟪Q ξ, ξ⟫ ≤ ⟪S ξ, ξ⟫) {k : ℕ}
    (ℓ : Fin k → (H →L[ℝ] ℝ)) (hℓ : ∀ i, ∃ C : ℝ, ∀ ξ, (ℓ i ξ) ^ 2 ≤ C * ⟪S ξ, ξ⟫)
    (q : MvPolynomial (Option (Fin k)) ℂ) :
    ∀ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ → ∀ I : Set ℝ, IsFrequencyWindow ρ I →
      IsRegularAlongRays (gaussianMixture N α) I fun ξ =>
        MvPolynomial.eval (fun o : Option (Fin k) =>
            o.elim ((⟪S ξ, ξ⟫ : ℝ) : ℂ) fun i => ((ℓ i ξ : ℝ) : ℂ)) q *
          Complex.exp (-((⟪S ξ, ξ⟫ / 2 : ℝ) : ℂ)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_ray_regular_examples_b_i, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Radial bumps
`G(ξ) = φ(‖ξ - ξ₀‖²)` with `φ ∈ C_c^∞(ℝ)` are regular along rays for every band-pass `ρ`. -/
theorem lem_ray_regular_examples_b_i (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) (ξ₀ : H) (φ : ℝ → ℂ) (hφ : ContDiff ℝ (⊤ : ℕ∞) φ)
    (hφc : HasCompactSupport φ) :
    ∀ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ → ∀ I : Set ℝ, IsFrequencyWindow ρ I →
      IsRegularAlongRays (gaussianMixture N α) I fun ξ => φ (‖ξ - ξ₀‖ ^ 2) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_ray_regular_examples_b_ii, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  More generally,
a bounded Borel `G` that is `C^∞` along rays (on a neighbourhood of the frequency window),
vanishes outside a bounded set, and satisfies `sup_{ω ∈ I} |∂_ω^k G(ωa)| ≤ C_k (1+‖a‖)^{p_k}`
for all `k`, is regular along rays for every band-pass `ρ`. -/
theorem lem_ray_regular_examples_b_ii (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) (G : H → ℂ) (hG : Measurable G) (hGb : ∃ M : ℝ, ∀ ξ, ‖G ξ‖ ≤ M)
    (hG0 : ∃ R₀ : ℝ, ∀ ξ : H, R₀ < ‖ξ‖ → G ξ = 0) :
    ∀ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ → ∀ I : Set ℝ, IsFrequencyWindow ρ I →
      (∀ a : H, ∃ U : Set ℝ, IsOpen U ∧ I ⊆ U ∧
        ContDiffOn ℝ (⊤ : ℕ∞) (fun ω : ℝ => G (ω • a)) U) →
      (∀ k : ℕ, ∃ C p : ℝ, ∀ a : H, ∀ ω ∈ I,
        ‖iteratedDeriv k (fun ω : ℝ => G (ω • a)) ω‖ ≤ C * (1 + ‖a‖) ^ p) →
      IsRegularAlongRays (gaussianMixture N α) I G := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_ray_regular_examples_c_i, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Finite linear
combinations of densities that are regular along rays are regular along rays. -/
theorem lem_ray_regular_examples_c_i (ν : Measure H) (I : Set ℝ) {ι : Type*} (s : Finset ι)
    (c : ι → ℂ) (G : ι → H → ℂ) (hG : ∀ i ∈ s, IsRegularAlongRays ν I (G i)) :
    IsRegularAlongRays ν I fun ξ => ∑ i ∈ s, c i * G i ξ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_ray_regular_examples_c_ii, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:ray-regular-examples]** Densities that are regular along rays.  Bochner
integrals `∫ G_y m(dy)` of a measurable family of densities that are regular along rays, over
a finite measure `m`, are regular along rays when the densities are uniformly bounded and the
weights of `eq:ray-regularity` have a `ν_α`-integrable majorant that is uniform in `y`. -/
theorem lem_ray_regular_examples_c_ii (ν : Measure H) (I : Set ℝ) {Ω : Type*}
    [MeasurableSpace Ω] (m : Measure Ω) [IsFiniteMeasure m] (G : Ω → H → ℂ)
    (hGm : Measurable (Function.uncurry G)) (hG : ∀ y, IsRegularAlongRays ν I (G y))
    (hGb : ∃ M : ℝ, ∀ y ξ, ‖G y ξ‖ ≤ M)
    (U : Set ℝ) (hU : IsOpen U) (hIU : I ⊆ U)
    (hsmooth : ∀ y a, ContDiffOn ℝ (⊤ : ℕ∞) (fun ω : ℝ => G y (ω • a)) U)
    (hunif : ∀ k : ℕ, ∃ h : H → NNReal,
      (∫⁻ a, ENNReal.ofReal ((1 + ‖a‖) ^ (k + 2)) * (h a : ℝ≥0∞) ∂ν) < ⊤ ∧
        ∀ y a, rayDerivBound U (G y) k a ≤ h a) :
    IsRegularAlongRays ν I fun ξ => ∫ y, G y ξ ∂m := by

Status: verified by comparator.

8.11.4. Lemma D.4 — Qualitative finite-atomic approximation (lem:qualitative-sampling)🔗

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

Formalization note. The hypothesis ∫ ‖β(⟨a,·⟩+c)‖_{C(K)} d|Γ| < ∞ is Integrable (θ ↦ compactSupNorm K (β(⟨a,·⟩+c))) Γ.variation; a finite atomic complex measure is atomicMeasure w θ = Σ_j VectorMeasure.dirac (θ_j) (w_j), and its synthesis is integralNetwork β (atomicMeasure w θ).

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

/-- **Lemma [lem:qualitative-sampling]** Qualitative finite-atomic approximation.  For
continuous `β`, compact `K`, and `∫ ‖β(⟪a,·⟫ + c)‖_{C(K)} d|Γ| < ∞`, for every `ε > 0` there
is a finite atomic complex measure `Γ_ε = ∑_j w_j δ_{θ_j}` with
`‖S_β Γ_ε − S_β Γ‖_{C(K)} < ε`. -/
theorem lem_qualitative_sampling [MeasurableSpace H] [BorelSpace H] {β : ℝ → ℂ}
    (hβ : Continuous β) (Γ : ComplexMeasure (H × ℝ)) [IsFiniteMeasure Γ.variation] {K : Set H}
    (hK : IsCompact K)
    (hint : Integrable (fun θ : H × ℝ => compactSupNorm K fun x => β (⟪θ.1, x⟫ + θ.2))
      Γ.variation)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (n : ℕ) (w : Fin n → ℂ) (θ : Fin n → H × ℝ),
      compactSupNorm K
        (fun x => integralNetwork β (atomicMeasure w θ) x - integralNetwork β Γ x) < ε := by

Status: verified by comparator.

8.11.5. Corollary D.5 — Concentration for bounded parameters (cor:sampling-concentration)🔗

Blueprint node: Corollary 5.1.8. Status: verified (its Lean theorem is verified).

Formalization note. '‖a‖²+|c|² ≤ B² almost surely' is ∀ᵐ θ ∂(polarLaw Γ), with the bound B ≥ 0 (hB0 : 0 ≤ B; implicit in the manuscript, where B bounds a norm, and needed since the threshold could be negative for B < 0). 'With probability at least 1 − δ' is stated as the (outer) measure under sampleLaw N (polarLaw Γ) of the exceptional set {θ | bound < ‖f_N θ − f‖_{C(K)}} being ≤ ENNReal.ofReal δ, for 0 < δ (this is what the bounded-difference inequality gives and implies the measure of the good set is ≥ 1 − δ). The hypotheses of thm:lipschitz-barron (Lipschitz, second moment) are kept; M_K = |β 0| + L R_K B.

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

/-- **Corollary [cor:sampling-concentration]** Concentration for bounded parameters.  Under the
hypotheses of Theorem `thm:lipschitz-barron`, if `‖a‖² + |c|² ≤ B²` almost surely for some
`B ≥ 0` and `M_K = |β(0)| + Lip(β) R_K B`, then with probability at least `1 − δ`,
`‖f_N − f‖_{C(K)} ≤ (8V/√N)(|β(0)| + Lip(β) R_K M₂) + V M_K √(2 log(1/δ)/N)`. -/
theorem cor_sampling_concentration [MeasurableSpace H] [BorelSpace H] {β : ℝ → ℝ} {L : ℝ≥0}
    (hβ : LipschitzWith L β) (Γ : ComplexMeasure (H × ℝ)) [IsFiniteMeasure Γ.variation]
    (hM : Integrable (fun θ : H × ℝ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2) (polarLaw Γ)) {B : ℝ}
    (hB0 : 0 ≤ B) (hB : ∀ᵐ θ ∂polarLaw Γ, ‖θ.1‖ ^ 2 + |θ.2| ^ 2 ≤ B ^ 2) {K : Set H}
    (hK : IsCompact K) {N : ℕ} (hN : 0 < N) {δ : ℝ} (hδ : 0 < δ) :
    sampleLaw N (polarLaw Γ) {θ |
        8 * polarWeight Γ / Real.sqrt N *
            (|β 0| + (L : ℝ) * compactRadius K * Real.sqrt (secondMoment (polarLaw Γ))) +
          polarWeight Γ * (|β 0| + (L : ℝ) * compactRadius K * B) *
            Real.sqrt (2 * Real.log (1 / δ) / N) <
        compactSupNorm K (fun x =>
          polarSampledNetwork (fun t => (β t : ℂ)) Γ θ x -
            integralNetwork (fun t => (β t : ℂ)) Γ x)} ≤
      ENNReal.ofReal δ := by

Status: verified by comparator.

8.11.6. Lemma D.6 — Hilbert-valued sampling identity (lem:hilbert-sampling)🔗

Blueprint node: Lemma 5.1.9. Status: verified (all 3 Lean theorems verified).

Formalization note. X is a separable real Hilbert space (a complex Hilbert space is one via InnerProductSpace.complexToReal, and only norms enter); Y ∈ L²(p;X) is MemLp Y 2 p on an abstract probability space (Ω, p); independent copies are the coordinates of sampleLaw N p on Fin N → Ω; f = V • ∫ Y dp and f_N ω = (V/N) • Σ_j Y (ω j). Part i the identity, ii the upper bound, iii the deterministic sample; N > 0.

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

/-- **Lemma [lem:hilbert-sampling]** Hilbert-valued sampling identity.  For `Y ∈ L²(p; X)` with
values in a separable Hilbert space, independent copies `Y_j`, `f = V 𝔼Y`, and
`f_N = V N⁻¹ ∑_j Y_j`: `𝔼‖f_N − f‖² = (V²/N)(𝔼‖Y‖² − ‖𝔼Y‖²)`. -/
theorem lem_hilbert_sampling_i (p : Measure Ω) [IsProbabilityMeasure p] {Y : Ω → X}
    (hY : MemLp Y 2 p) (V : ℝ) {N : ℕ} (hN : 0 < N) :
    ∫ ω, ‖(V / N : ℝ) • ∑ j, Y (ω j) - V • ∫ ω', Y ω' ∂p‖ ^ 2 ∂sampleLaw N p =
      V ^ 2 / N * ((∫ ω', ‖Y ω'‖ ^ 2 ∂p) - ‖∫ ω', Y ω' ∂p‖ ^ 2) := by

Status: verified by comparator.

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

/-- **Lemma [lem:hilbert-sampling]** Hilbert-valued sampling identity.
`𝔼‖f_N − f‖² ≤ (V²/N) 𝔼‖Y‖²`. -/
theorem lem_hilbert_sampling_ii (p : Measure Ω) [IsProbabilityMeasure p] {Y : Ω → X}
    (hY : MemLp Y 2 p) (V : ℝ) {N : ℕ} (hN : 0 < N) :
    ∫ ω, ‖(V / N : ℝ) • ∑ j, Y (ω j) - V • ∫ ω', Y ω' ∂p‖ ^ 2 ∂sampleLaw N p ≤
      V ^ 2 / N * ∫ ω', ‖Y ω'‖ ^ 2 ∂p := by

Status: verified by comparator.

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

/-- **Lemma [lem:hilbert-sampling]** Hilbert-valued sampling identity.  A deterministic sample
satisfies the same upper bound `‖f_N − f‖² ≤ (V²/N) 𝔼‖Y‖²`. -/
theorem lem_hilbert_sampling_iii (p : Measure Ω) [IsProbabilityMeasure p] {Y : Ω → X}
    (hY : MemLp Y 2 p) (V : ℝ) {N : ℕ} (hN : 0 < N) :
    ∃ ω : Fin N → Ω,
      ‖(V / N : ℝ) • ∑ j, Y (ω j) - V • ∫ ω', Y ω' ∂p‖ ^ 2 ≤ V ^ 2 / N * ∫ ω', ‖Y ω'‖ ^ 2 ∂p := by

Status: verified by comparator.

8.11.7. Corollary D.7 — Sampling in operator parameters (cor:operator-sampling)🔗

Blueprint node: Corollary 5.1.10. Status: verified (all 2 Lean theorems verified).

Formalization note. Γ_op is a ComplexMeasure on (H →L[ℝ] H) × H with finite variation carried by 𝓛₂(H) × H (∀ᵐ q ∂Γ_op.variation, IsHilbertSchmidt q.1), as in lem:measure-transport; its polar data are polarDensity/polarWeight/polarLaw Γ_op; M_op² < ∞ is Integrable (‖A*ψ‖² + |⟨ψ,b⟩|²) (polarLaw Γ_op) and M_op = √(operatorSecondMoment ψ (polarLaw Γ_op)). The sampled operator network is sampledOperatorNetwork (rankOneActivation β ψ z) ℓ V h ω, an operatorFiniteNetwork with weights (V/N) h(A_j,b_j), and S_op Γ_op is operatorSynthesis; the readout is normalized by ⟨ℓ,z⟩ = 1 and ψ ≠ 0 is not needed (as in lem:measure-transport), so it is not assumed. Part ii (M_op² ≤ ‖ψ‖² ∫(‖A‖²_{𝓛₂}+‖b‖²) dp_op) is stated with lintegrals and hsNormSq (∞ off 𝓛₂), so that no integrability hypothesis is needed.

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

/-- **Corollary [cor:operator-sampling]** Sampling in operator parameters.  For a finite
complex measure `Γ_op` on `𝓛₂(H) × H` with polar decomposition `h_op |Γ_op|`,
`V_op = ‖Γ_op‖_TV`, `p_op = |Γ_op|/V_op`, real globally Lipschitz `β`, readout normalized by
`⟪ℓ, z⟫ = 1`, and `M_op² = ∫ (‖A^*ψ‖² + |⟪ψ, b⟫|²) dp_op < ∞`, sampling `(A_j, b_j)` from
`p_op` with the weights `h_op` gives
`𝔼‖f_{op,N} − S_op Γ_op‖_{C(K)} ≤ 8 V_op N^{-1/2} (|β(0)| + Lip(β) R_K M_op)`. -/
theorem cor_operator_sampling_i [CompleteSpace H] [SecondCountableTopology H]
    [MeasurableSpace H] [BorelSpace H] {β : ℝ → ℝ} {L : ℝ≥0} (hβ : LipschitzWith L β) (ψ : H)
    (Γop : ComplexMeasure (OperatorRidgeParameter H)) [IsFiniteMeasure Γop.variation]
    (hHS : ∀ᵐ q ∂Γop.variation, IsHilbertSchmidt q.1)
    (hM : Integrable (fun q : OperatorRidgeParameter H =>
      ‖ContinuousLinearMap.adjoint q.1 ψ‖ ^ 2 + |⟪ψ, q.2⟫| ^ 2) (polarLaw Γop))
    {ℓ z : H} (hℓz : ⟪ℓ, z⟫ = 1) {K : Set H} (hK : IsCompact K) {N : ℕ} (hN : 0 < N) :
    ∫ ω, compactSupNorm K (fun x =>
          sampledOperatorNetwork (rankOneActivation β ψ z) ℓ (polarWeight Γop)
              (polarDensity Γop) ω x -
            operatorSynthesis (rankOneActivation β ψ z) ℓ Γop x)
        ∂sampleLaw N (polarLaw Γop) ≤
      8 * polarWeight Γop / Real.sqrt N *
        (|β 0| + (L : ℝ) * compactRadius K *
          Real.sqrt (operatorSecondMoment ψ (polarLaw Γop))) := by

Status: verified by comparator.

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

/-- **Corollary [cor:operator-sampling]** Sampling in operator parameters.
`M_op² ≤ ‖ψ‖² ∫ (‖A‖²_{𝓛₂} + ‖b‖²) dp_op`. -/
theorem cor_operator_sampling_ii [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] (ψ : H)
    (Γop : ComplexMeasure (OperatorRidgeParameter H)) [IsFiniteMeasure Γop.variation]
    (hHS : ∀ᵐ q ∂Γop.variation, IsHilbertSchmidt q.1) :
    ∫⁻ q, (‖ContinuousLinearMap.adjoint q.1 ψ‖ₑ ^ 2 + ‖⟪ψ, q.2⟫‖ₑ ^ 2) ∂polarLaw Γop ≤
      ‖ψ‖ₑ ^ 2 * ∫⁻ q, (hsNormSq q.1 + ‖q.2‖ₑ ^ 2) ∂polarLaw Γop := by

Status: verified by comparator.

8.11.8. Corollary D.8 — Input truncation and sampling are separate errors (cor:two-stage-error)🔗

Blueprint node: Corollary 5.1.11. Status: verified (all 2 Lean theorems verified).

Formalization note. Π_m is P : ℕ → (H →L[ℝ] H) with IsFiniteRankProjection (P m) (IsStarProjection, i.e. self-adjoint idempotent, with finite-dimensional range) and strong convergence ∀ x, Tendsto (P m x) → x. Part i: Tendsto (compactSupNorm K (f − f ∘ P m)) → 0 for continuous f : H → ℂ. Part ii: the truncated network f_{m,N} keeps the samples θ_j and the weights (V/N) h(θ_j) of the polar sampled network and projects only the directions inside the activation, f_{m,N}(x) = (V/N) ∑_j h(θ_j) β(⟪P m a_j, x⟫ + c_j), encoded as finiteNetwork β (fun j => (V/N) • polarDensity Γ (θ j)) (fun j => P m (θ j).1) (fun j => (θ j).2) (the phase h = polarDensity Γ is only specified |Γ|-a.e., so it may not be evaluated at the projected parameters); ∫ ‖a‖ d|Γ| is the Bochner integral against Γ.variation (finite under the hypotheses) and sup_K ‖x − Π_m x‖ is compactSupNorm K (x ↦ x − P m x); hypotheses of thm:lipschitz-barron (real Lipschitz β, second moment of polarLaw Γ), N > 0, m arbitrary.

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

/-- **Corollary [cor:two-stage-error]** Input truncation and sampling are separate errors.  For
finite-rank orthogonal projections `Π_m` converging strongly to the identity, `f ∈ C(H)`, and
compact `K`, `‖f − f ∘ Π_m‖_{C(K)} → 0`. -/
theorem cor_two_stage_error_i [CompleteSpace H] (P : ℕ → (H →L[ℝ] H))
    (hP : ∀ m, IsFiniteRankProjection (P m))
    (hlim : ∀ x : H, Tendsto (fun m => P m x) atTop (𝓝 x)) {f : H → ℂ} (hf : Continuous f)
    {K : Set H} (hK : IsCompact K) :
    Tendsto (fun m => compactSupNorm K (fun x => f x - f (P m x))) atTop (𝓝 0) := by

Status: verified by comparator.

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

/-- **Corollary [cor:two-stage-error]** Input truncation and sampling are separate errors.  If
`f = S_β Γ` satisfies the hypotheses of Theorem `thm:lipschitz-barron` and the same samples and
weights `(V/N) h(θ_j)` are used with the truncated directions `Π_m a_j` inside the activation,
`f_{m,N}(x) = (V/N) ∑_j h(θ_j) β(⟪Π_m a_j, x⟫ + c_j)`, then
`𝔼‖f − f_{m,N}‖_{C(K)} ≤ Lip(β) (∫ ‖a‖ d|Γ|) sup_K ‖x − Π_m x‖ +
(8V/√N)(|β(0)| + Lip(β) R_K M₂)`. -/
theorem cor_two_stage_error_ii [CompleteSpace H] [MeasurableSpace H] [BorelSpace H]
    (P : ℕ → (H →L[ℝ] H)) (hP : ∀ m, IsFiniteRankProjection (P m))
    (hlim : ∀ x : H, Tendsto (fun m => P m x) atTop (𝓝 x)) {β : ℝ → ℝ} {L : ℝ≥0}
    (hβ : LipschitzWith L β) (Γ : ComplexMeasure (H × ℝ)) [IsFiniteMeasure Γ.variation]
    (hM : Integrable (fun θ : H × ℝ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2) (polarLaw Γ)) {K : Set H}
    (hK : IsCompact K) {N : ℕ} (hN : 0 < N) (m : ℕ) :
    ∫ θ, compactSupNorm K (fun x =>
          integralNetwork (fun t => (β t : ℂ)) Γ x -
            finiteNetwork (fun t => (β t : ℂ))
              (fun j => ((polarWeight Γ / N : ℝ) : ℂ) • polarDensity Γ (θ j))
              (fun j => P m (θ j).1) (fun j => (θ j).2) x)
        ∂sampleLaw N (polarLaw Γ) ≤
      (L : ℝ) * (∫ θ, ‖θ.1‖ ∂Γ.variation) * compactSupNorm K (fun x => x - P m x) +
        8 * polarWeight Γ / Real.sqrt N *
          (|β 0| + (L : ℝ) * compactRadius K * Real.sqrt (secondMoment (polarLaw Γ))) := by

Status: verified by comparator.