Infinite-dimensional operator ridgelet transform

8.10. Appendix C🔗

8.10.1. Lemma C.1 — Hilbert structure and continuous activation pairing (lem:weighted-duality)🔗

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

Formalization note. 𝒜_{s,t} is the vendored MemActivationSpace s t (⟨x⟩^{-t} β ∈ H^s), B^q is the vendored angular Bessel potential, and the coordinate ⟨ω⟩^s B^{-t} β̂ is activationFourierCoordinate with L² representative activationCoordinate (by choice); the norm ‖β‖_{𝒜_{s,t}} is its L² norm (the isometry is the definition of the norm). 'Isometric isomorphism 𝒜_{s,t} → L²' is split into: the coordinate exists for β ∈ 𝒜_{s,t} (i), injectivity (ii), surjectivity through the vendored activationRealization (iii). The dual test norm ‖r‖_{ℋ^♯_{s,t}} = ‖⟨ω⟩^{-s} B^t r‖_{L²} is testFilterNorm; the bound is (iv), and the extension to the completion (v) is a continuous linear functional on L²(ℝ) (the completion of the test filters via r ↦ ⟨ω⟩^{-s} B^t r) of norm ≤ (2π)⁻¹‖β‖ that agrees with (2π)⁻¹⟨β̂, r⟩ on test filters.

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

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

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

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

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

OperatorRidgelet.Paper.lem_weighted_duality_i, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
map `β ↦ ⟨ω⟩^s B^{-t} β̂` is well defined on `𝒜_{s,t}`: its value is represented by an element
of `L²(ℝ)`. -/
theorem lem_weighted_duality_i (s t : ℝ) (β : TemperedDistribution ℝ ℂ)
    (hβ : MemActivationSpace s t β) :
    ∃ σ : L2 ℝ volume,
      Lp.toTemperedDistributionCLM ℂ volume 2 σ = activationFourierCoordinate s t β := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_weighted_duality_ii, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
map `β ↦ ⟨ω⟩^s B^{-t} β̂` is injective on `𝒜_{s,t}`. -/
theorem lem_weighted_duality_ii (s t : ℝ) (β β' : TemperedDistribution ℝ ℂ)
    (hβ : MemActivationSpace s t β) (hβ' : MemActivationSpace s t β')
    (h : activationCoordinate s t β = activationCoordinate s t β') :
    β = β' := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_weighted_duality_iii, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
map `β ↦ ⟨ω⟩^s B^{-t} β̂` is onto `L²(ℝ)`: every `σ ∈ L²(ℝ)` is the coordinate of the activation
`β = 𝓕⁻¹[B^t ⟨ω⟩^{-s} σ] ∈ 𝒜_{s,t}` (the vendored `activationRealization`); the isometry is the
definition of the norm `‖β‖_{𝒜_{s,t}} = ‖σ‖_{L²}`. -/
theorem lem_weighted_duality_iii (s t : ℝ) (σ : L2 ℝ volume) :
    MemActivationSpace s t (activationRealization s t σ) ∧
      activationCoordinate s t (activationRealization s t σ) = σ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_weighted_duality_iv, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
duality bound `|(2π)⁻¹ ⟨β̂, r⟩| ≤ (2π)⁻¹ ‖β‖_{𝒜_{s,t}} ‖r‖_{ℋ^♯_{s,t}}` for `β ∈ 𝒜_{s,t}` and
Schwartz `r`. -/
theorem lem_weighted_duality_iv (s t : ℝ) (β : TemperedDistribution ℝ ℂ)
    (hβ : MemActivationSpace s t β) (r : SchwartzMap ℝ ℂ) :
    ‖((2 * Real.pi)⁻¹ : ℝ) * angularFourierDistribution β r‖ ≤
      (2 * Real.pi)⁻¹ * activationNorm s t β * testFilterNorm s t r := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_weighted_duality_v, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:weighted-duality]** Hilbert structure and continuous activation pairing.  The
pairing extends to the completion of the test filters in `ℋ^♯_{s,t}`, which is `L²(ℝ)` through
the coordinate `r ↦ ⟨ω⟩^{-s} B^t r`: there is a continuous linear functional on `L²(ℝ)` of norm
at most `(2π)⁻¹ ‖β‖_{𝒜_{s,t}}` that agrees with `(2π)⁻¹ ⟨β̂, r⟩` on the test filters. -/
theorem lem_weighted_duality_v (s t : ℝ) (β : TemperedDistribution ℝ ℂ)
    (hβ : MemActivationSpace s t β) :
    ∃ Φ : L2 ℝ volume →L[ℂ] ℂ, ‖Φ‖ ≤ (2 * Real.pi)⁻¹ * activationNorm s t β ∧
      ∀ r : SchwartzMap ℝ ℂ,
        Φ ((testFilterCoordinate s t r).toLp 2 volume) =
          ((2 * Real.pi)⁻¹ : ℝ) * angularFourierDistribution β r := by

Status: verified by comparator.

8.10.2. Lemma C.2 — Standard activations and admissible test filters (lem:standard-activation-class)🔗

Blueprint node: Lemma 4.2.2. Status: verified (all 13 Lean theorems verified).

Formalization note. Membership 'β ∈ 𝒜_{0,2}' for a function β is MemActivationSpaceFun 0 2 β: some tempered distribution acting by integration against β satisfies the vendored MemActivationSpace 0 2 (for ReLU and tanh this is the vendored realization, for Φ = gaussianCdf and e^{-u²/2} = gaussianFun it is weightedDistribution 2); globally Lipschitz is ∃ L, LipschitzWith L β; not a polynomial is ¬ IsPolynomialFun β. The last claim (a real band-pass ρ with C^{(α)}_{β,ρ} = 1 for every non-polynomial real β ∈ 𝒮') is stated for the standing α > 0.

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

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

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

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

OperatorRidgelet.Paper.lem_standard_activation_class_relu_mem, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU belongs to `𝒜_{0,2}`. -/
theorem lem_standard_activation_class_relu_mem : MemActivationSpaceFun 0 2 relu := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_relu_lipschitz, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU is globally Lipschitz. -/
theorem lem_standard_activation_class_relu_lipschitz : ∃ L : ℝ≥0, LipschitzWith L relu := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_relu_not_polynomial, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
ReLU is not a polynomial. -/
theorem lem_standard_activation_class_relu_not_polynomial : ¬ IsPolynomialFun relu := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_tanh_mem, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` belongs to `𝒜_{0,2}`. -/
theorem lem_standard_activation_class_tanh_mem : MemActivationSpaceFun 0 2 Real.tanh := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_tanh_lipschitz, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` is globally Lipschitz. -/
theorem lem_standard_activation_class_tanh_lipschitz :
    ∃ L : ℝ≥0, LipschitzWith L Real.tanh := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_tanh_not_polynomial, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
`tanh` is not a polynomial. -/
theorem lem_standard_activation_class_tanh_not_polynomial : ¬ IsPolynomialFun Real.tanh := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_mem, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` belongs to `𝒜_{0,2}`. -/
theorem lem_standard_activation_class_gaussianCdf_mem : MemActivationSpaceFun 0 2 gaussianCdf := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_lipschitz, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is globally Lipschitz. -/
theorem lem_standard_activation_class_gaussianCdf_lipschitz :
    ∃ L : ℝ≥0, LipschitzWith L gaussianCdf := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_gaussianCdf_not_polynomial, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian distribution function `Φ` is not a polynomial. -/
theorem lem_standard_activation_class_gaussianCdf_not_polynomial :
    ¬ IsPolynomialFun gaussianCdf := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_mem, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` belongs to `𝒜_{0,2}`. -/
theorem lem_standard_activation_class_gaussian_mem : MemActivationSpaceFun 0 2 gaussianFun := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_lipschitz, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` is globally Lipschitz. -/
theorem lem_standard_activation_class_gaussian_lipschitz :
    ∃ L : ℝ≥0, LipschitzWith L gaussianFun := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_gaussian_not_polynomial, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
The Gaussian `e^{-u²/2}` is not a polynomial. -/
theorem lem_standard_activation_class_gaussian_not_polynomial : ¬ IsPolynomialFun gaussianFun := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_standard_activation_class_exists_filter, theorem in Challenge/Tempered.lean:

/-- **Lemma [lem:standard-activation-class]** Standard activations and admissible test filters.
For every non-polynomial real `β ∈ 𝒮'` there is a real band-pass `ρ` with
`C^{(α)}_{β,ρ} = 1`. -/
theorem lem_standard_activation_class_exists_filter {α : ℝ} (hα : 0 < α)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β)
    (hpoly : ¬ IsPolynomialDistribution β) :
    ∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧ temperedAdmissibilityConst α β ρ = 1 := by

Status: verified by comparator.

8.10.3. Lemma C.3 — Weighted inverse Fourier estimates and modulation (lem:sobolev-tools)🔗

Blueprint node: Lemma 4.3.1. Status: verified (all 4 Lean theorems verified).

Formalization note. New in the 2026-09-13 revision; taken from supp.tex supp:lem:sobolev-tools. The Sobolev space H^s_ω(ℝ;Y) is carried by the pair of a profile h and its inverse Fourier transform γ = ȟ (OperatorRidgelet.Sobolev.Defs): MemRaySobolev s γ is the membership (γ square integrable against the weight ⟨t⟩^{2s} = (1+t²)^s), raySobolevNorm s γ is the norm (2π ∫ ⟨t⟩^{2s} ‖γ‖²)^{1/2} of eq:sobolev-norm, rayProfile γ = γ̂ in the angular convention (for s > 1/2 the coefficient is integrable by part i, so the profile is an ordinary Fourier integral), and sobolevMomentConst s r is A_{s,r}. i is eq:sobolev-weighted-l1; ii is the reflection isometry together with the identity Rh = (γ(-·))^; iii is eq:sobolev-modulation together with the identity M_u h = (γ(·+u))^; iv is the joint continuity of (u,h) ↦ M_u h, stated along an arbitrary filter as the convergence of ‖M_{u_i} h_i − M_{u₀} h‖_{H^s_ω} to zero when u_i → u₀ and ‖h_i − h‖_{H^s_ω} → 0.

OperatorRidgelet.Paper.lem_sobolev_tools_i, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-tools]**(i) The weighted inverse Fourier estimate
`∫ ⟨t⟩^r ‖γ(t)‖ dt ≤ A_{s,r} ‖h‖_{H^s_ω}` (`eq:sobolev-weighted-l1`) for `0 ≤ r < s - 1/2`,
where `γ = ȟ` and `A_{s,r} = (2π)^{-1/2}(∫ (1+t²)^{-(s-r)} dt)^{1/2}`. -/
theorem lem_sobolev_tools_i {s r : ℝ} (hr0 : 0 ≤ r) (hrs : r + 1 / 2 < s) {γ : ℝ → Y}
    (hγ : MemRaySobolev s γ) :
    ∫ t : ℝ, (bracket t ^ r : ℝ) * ‖γ t‖ ≤ sobolevMomentConst s r * raySobolevNorm s γ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_sobolev_tools_ii, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-tools]**(ii) Reflection `R h(ω) = h(-ω)` is an isometry of
`H^s_ω(ℝ;Y)`: the reflected coefficient is again in the class with the same norm, and its
profile is the reflected profile. -/
theorem lem_sobolev_tools_ii {s : ℝ} {γ : ℝ → Y} (hγ : MemRaySobolev s γ) :
    MemRaySobolev s (fun t => γ (-t)) ∧
      raySobolevNorm s (fun t => γ (-t)) = raySobolevNorm s γ ∧
      ∀ ω : ℝ, rayProfile (fun t => γ (-t)) ω = rayProfile γ (-ω) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_sobolev_tools_iii, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-tools]**(iii) Modulation `M_u h(ω) = e^{iuω} h(ω)` maps `H^s_ω(ℝ;Y)`
to itself with `‖M_u h‖_{H^s_ω} ≤ (1 + |u|)^s ‖h‖_{H^s_ω}` (`eq:sobolev-modulation`); its
coefficient is the translate `γ(· + u)`. -/
theorem lem_sobolev_tools_iii {s : ℝ} (hs : 0 ≤ s) {γ : ℝ → Y} (hγ : MemRaySobolev s γ)
    (u : ℝ) :
    MemRaySobolev s (fun t => γ (t + u)) ∧
      raySobolevNorm s (fun t => γ (t + u)) ≤ ((1 + |u|) ^ s : ℝ) * raySobolevNorm s γ ∧
      ∀ ω : ℝ, rayProfile (fun t => γ (t + u)) ω =
        Complex.exp (((u * ω : ℝ) : ℂ) * Complex.I) • rayProfile γ ω := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_sobolev_tools_iv, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-tools]**(iv) The map `(u, h) ↦ M_u h` is jointly continuous: if the
biases converge and the profiles converge in `H^s_ω(ℝ;Y)`, then so do the modulated profiles. -/
theorem lem_sobolev_tools_iv {S : Type*} {l : Filter S} {s : ℝ} (hs : 0 ≤ s) {γ : ℝ → Y}
    {γ' : S → ℝ → Y} {u : S → ℝ} {u₀ : ℝ} (hγ : MemRaySobolev s γ)
    (hγ' : ∀ i, MemRaySobolev s (γ' i)) (hu : Tendsto u l (nhds u₀))
    (hconv : Tendsto (fun i => raySobolevNorm s (fun t => γ' i t - γ t)) l (nhds 0)) :
    Tendsto (fun i => raySobolevNorm s (fun t => γ' i (t + u i) - γ (t + u₀))) l (nhds 0) := by

Status: verified by comparator.

8.10.4. Lemma C.4 — The bilinear Sobolev pairing and its translation formula (lem:sobolev-pairing)🔗

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

Formalization note. New in the 2026-09-13 revision; taken from supp.tex supp:lem:sobolev-pairing. In the pair formulation of OperatorRidgelet.Sobolev.Defs the pairing is the absolutely convergent integral sobolevPairing σ γ = ∫ σ(t) • γ(-t) dt, which is the manuscript's normalization (2π)⁻¹⟨σ̂, q⟩ = ∫ σ(t) q̌(-t) dt written on the coefficient side, and sobolevPairingConst σ s is b_{σ,s}. i is the finiteness of b_{σ,s} for a continuous σ of polynomial growth p and s > p + 1/2, stated as square integrability of ⟨·⟩^{-s}σ; ii is the absolute convergence together with the bound ‖L_σ^Y(h)‖ ≤ (2π)^{-1/2} b_{σ,s} ‖h‖_{H^s_ω}, which is the assertion that the functional lies in the bilinear dual with that norm; iii is eq:sobolev-bias-pairing. The identification of the extended functional with the distributional Fourier transform of σ on Schwartz tests is the manuscript's interpretation of the same integral and is not restated in Lean.

OperatorRidgelet.Paper.lem_sobolev_pairing_i, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-pairing]**(i) For a continuous activation of polynomial growth `p` and
`s > p + 1/2`, the weighted activation `⟨·⟩^{-s} σ` is square integrable, that is
`b_{σ,s} = ‖⟨·⟩^{-s}σ‖_2 < ∞`. -/
theorem lem_sobolev_pairing_i {σ : ℝ → ℂ} {p s C : ℝ} (hp : 0 ≤ p) (hps : p + 1 / 2 < s)
    (hσ : Continuous σ) (hbound : ∀ t : ℝ, ‖σ t‖ ≤ C * (1 + |t|) ^ p) :
    MemLp (fun t : ℝ => (bracket t ^ (-s) : ℝ) • σ t) 2 volume := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_sobolev_pairing_ii, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-pairing]**(ii) The pairing `L_σ^Y(h) = ∫ σ(t) γ(-t) dt` converges
absolutely and is bounded: `‖L_σ^Y(h)‖ ≤ (2π)^{-1/2} b_{σ,s} ‖h‖_{H^s_ω}`, so it is an element
of the bilinear dual of `H^s_ω(ℝ;Y)` with that norm (`eq:sobolev-pairing`). -/
theorem lem_sobolev_pairing_ii {σ : ℝ → ℂ} {s : ℝ} {γ : ℝ → Y}
    (hσ : MemLp (fun t : ℝ => (bracket t ^ (-s) : ℝ) • σ t) 2 volume)
    (hγ : MemRaySobolev s γ) :
    Integrable (fun t : ℝ => σ t • γ (-t)) volume ∧
      ‖sobolevPairing σ γ‖ ≤
        sobolevPairingConst σ s / Real.sqrt (2 * Real.pi) * raySobolevNorm s γ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_sobolev_pairing_iii, theorem in Challenge/Sobolev.lean:

/-- **Lemma [lem:sobolev-pairing]**(iii) The bias translation of the activation is the
modulation of the profile: `∫ σ(u - b) γ(b) db = L_σ^Y(M_u h)` (`eq:sobolev-bias-pairing`). -/
theorem lem_sobolev_pairing_iii (σ : ℝ → ℂ) (γ : ℝ → Y) (u : ℝ) :
    ∫ b : ℝ, σ (u - b) • γ b = sobolevPairing σ (fun t => γ (t + u)) := by

Status: verified by comparator.