8.16.1. Example I.1 — A band-pass filter for every \(\alpha>0\) (ex:bandlimited-filter)🔗

Blueprint node: Proposition 2.6.2. Status: verified (all 10 Lean theorems verified).

Formalization note. ρ_bp is obtained by choice as the Schwartz map equal to the Fourier inversion of ρ̂_bp (bandPass); the ReLU-synthesis admissibility claim belongs to the tempered work package (cor:relu-admissible).

OperatorRidgelet.Paper.ex_bandlimited_filter_i, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  The prescribed
Fourier transform `ρ̂_bp` is smooth. -/
theorem ex_bandlimited_filter_i : ContDiff ℝ (⊤ : ℕ∞) bandPassHat := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_ii, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ̂_bp` is
nonpositive. -/
theorem ex_bandlimited_filter_ii : ∀ ω : ℝ, bandPassHat ω ≤ 0 := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_iii, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ̂_bp` is
nonzero. -/
theorem ex_bandlimited_filter_iii : bandPassHat ≠ 0 := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_iv, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ̂_bp` is
supported in `{1 ≤ |ω| ≤ 2}`. -/
theorem ex_bandlimited_filter_iv : tsupport bandPassHat ⊆ {ω : ℝ | 1 ≤ |ω| ∧ |ω| ≤ 2} := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_v, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  The inverse
Fourier transform `ρ_bp` of `ρ̂_bp` is a real Schwartz function. -/
theorem ex_bandlimited_filter_v : ⇑bandPass = bandPassFun := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_vi, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ_bp` is even. -/
theorem ex_bandlimited_filter_vi : ∀ t : ℝ, bandPass (-t) = bandPass t := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_vii, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  The Fourier
transform of `ρ_bp` is the prescribed `ρ̂_bp`. -/
theorem ex_bandlimited_filter_vii : ∀ ω : ℝ, filterFourier bandPass ω = (bandPassHat ω : ℂ) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_viii, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ_bp` satisfies
the band-pass condition. -/
theorem ex_bandlimited_filter_viii : IsBandPass bandPass := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_ix, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  `ρ_bp` is
`α`-admissible for every `α > 0`. -/
theorem ex_bandlimited_filter_ix : ∀ α : ℝ, 0 < α → IsAdmissible α bandPass := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_bandlimited_filter_x, theorem in Challenge/Transform.lean:

/-- **Example [ex:bandlimited-filter]** A band-pass filter for every `α > 0`.  Multiplying by
`(C^{(α)}_{ρ_bp})^{-1/2}` normalizes the admissibility constant to one. -/
theorem ex_bandlimited_filter_x :
    ∀ α : ℝ, 0 < α →
      admissibilityConst α ((Real.sqrt (admissibilityConst α bandPass))⁻¹ • bandPass) = 1 := by

Status: verified by comparator.

8.16.2. Example I.2 — Mexican hat (ex:mexican-hat)🔗

Blueprint node: Proposition 2.6.3. Status: verified (all 6 Lean theorems verified).

Formalization note. ρ_MH is obtained by choice as the Schwartz map equal to (1-t²)e^{-t²/2} (mexicanHat); admissibility exactly for 0 < α < 5 with C = Γ((5-α)/2), C^{(1)} = 1, not band pass. Part (iii) is stated under the manuscript's standing assumption α > 0 (for α ≤ 0 the admissibility integral also converges, so 'exactly for 0 < α < 5' is only true given α > 0).

OperatorRidgelet.Paper.ex_mexican_hat_i, theorem in Challenge/Transform.lean:

/-- **Example [ex:mexican-hat]** Mexican hat.  `ρ_MH(t) = (1 - t²) e^{-t²/2}` is a Schwartz
function. -/
theorem ex_mexican_hat_i : ⇑mexicanHat = mexicanHatFun := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_mexican_hat_ii, theorem in Challenge/Transform.lean:

/-- **Example [ex:mexican-hat]** Mexican hat.  `ρ̂_MH(ω) = √(2π) ω² e^{-ω²/2}`. -/
theorem ex_mexican_hat_ii :
    ∀ ω : ℝ, filterFourier mexicanHat ω =
      ((Real.sqrt (2 * Real.pi) * ω ^ 2 * Real.exp (-ω ^ 2 / 2) : ℝ) : ℂ) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_mexican_hat_iii, theorem in Challenge/Transform.lean:

/-- **Example [ex:mexican-hat]** Mexican hat.  Under the standing assumption `α > 0`, `ρ_MH` is
`α`-admissible exactly for `α < 5`. -/
theorem ex_mexican_hat_iii : ∀ α : ℝ, 0 < α → (IsAdmissible α mexicanHat ↔ α < 5) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_mexican_hat_iv, theorem in Challenge/Transform.lean:

/-- **Example [ex:mexican-hat]** Mexican hat.  For `0 < α < 5`,
`C^{(α)}_{ρ_MH} = Γ((5-α)/2)`. -/
theorem ex_mexican_hat_iv :
    ∀ α : ℝ, 0 < α → α < 5 → admissibilityConst α mexicanHat = Real.Gamma ((5 - α) / 2) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_mexican_hat_v, theorem in Challenge/Transform.lean:

/-- **Example [ex:mexican-hat]** Mexican hat.  In particular `C^{(1)}_{ρ_MH} = 1`. -/
theorem ex_mexican_hat_v : admissibilityConst 1 mexicanHat = 1 := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_mexican_hat_vi, theorem in Challenge/Transform.lean:

/-- **Example [ex:mexican-hat]** Mexican hat.  `ρ_MH` is not band pass. -/
theorem ex_mexican_hat_vi : ¬ IsBandPass mexicanHat := by

Status: verified by comparator.

8.16.3. Proposition I.3 — Non-band-pass Gaussian-derivative filters (prop:nonbandpass-sobolev)🔗

Blueprint node: Proposition 4.4.1. Status: verified (all 9 Lean theorems verified).

Formalization note. New in the 2026-09-13 revision; taken from supp.tex supp:prop:nonbandpass-sobolev. The Gaussian-derivative filter rho_k with rho^_k(omega) = omega^{2k} e^{-omega^2} is built in OperatorRidgelet.Sobolev.GaussianDefs as the inverse angular transform of that symbol, which is real because the symbol is real and even; i is that transform, ii the failure of the band-pass property, and iii self-admissibility, which holds for alpha < 4k+1. iv is eq:homogeneous-polynomial-integrability, stated for a homogeneous nu that is finite on the unit ball. v-vii are the hypotheses of thm:weak-sobolev-synthesis for the target g(xi) = e^{-||xi||^2} v: the rays are the dilates A^{-2k-1} rho_k(b/A) v at the scale A = (1+||a||^2)^{1/2}, and the Sobolev mass B_s is finite exactly in the range eq:nonbandpass-order, 2k > alpha + 2s - 1/2. viii is q_{alpha,rho} in H^s_omega, proved as in the manuscript by subordination through the Gamma integral |omega|^{-alpha} = Gamma(alpha/2)^{-1} int u^{alpha/2-1} e^{-u omega^2} du, which writes q as a superposition of the ray symbols and needs no weak derivatives. ix assembles i-viii into the conclusion of thm:weak-sobolev-synthesis for this filter and every continuous activation of growth order p < s - 1/2. The two closed-form constants of the manuscript, C^(alpha)_{sigma,rho} for the Gaussian activation and for ReLU, are not formalized: the Lean statement carries the constant as the Sobolev pairing sobolevPairing sigma q of lem:sobolev-pairing, which is what the synthesis identity uses.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(i) The Gaussian-derivative filter of order `k`
is a real Schwartz function with Fourier transform `ρ̂_k(ω) = ω^{2k} e^{-ω²}`. -/
theorem prop_nonbandpass_sobolev_i (k : ℕ) (ω : ℝ) :
    filterFourier (gaussDerivFilter k) ω = ((ω ^ (2 * k) * Real.exp (-ω ^ 2) : ℝ) : ℂ) := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(ii) The filter is not band pass: its Fourier
transform vanishes only at the origin. -/
theorem prop_nonbandpass_sobolev_ii (k : ℕ) : ¬ IsBandPass (gaussDerivFilter k) := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(iii) The filter is nevertheless `α`-admissible,
`0 < C^{(α)}_{ρ_k} < ∞`, in the range `α < 4k + 1`. -/
theorem prop_nonbandpass_sobolev_iii {k : ℕ} {α : ℝ} (hα : 0 < α) (hk : α < 4 * k + 1) :
    IsAdmissible α (gaussDerivFilter k) := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(iv) The polynomial moments
`eq:homogeneous-polynomial-integrability` of a homogeneous measure that is finite on the unit
ball: `∫ (1 + ‖a‖²)^e dν < ∞` whenever `2e + α < 0`. -/
theorem prop_nonbandpass_sobolev_iv {α e : ℝ} (hα : 0 < α) {ν : Measure H}
    (hν : IsHomogeneous α ν) (hB : ν (Metric.closedBall 0 1) ≠ ⊤) (he : 2 * e + α < 0) :
    ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖ ^ 2) ^ e) ∂ν < ⊤ := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(v) The coefficient of the rays of the filter for
the Gaussian target `g(ξ) = e^{-‖ξ‖²} v` is jointly strongly measurable. -/
theorem prop_nonbandpass_sobolev_v (k : ℕ) (v : Y) :
    StronglyMeasurable (gaussRayCoefficient (H := H) k v) := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(vi) Every ray lies in `H^s_ω(ℝ;Y)` and has the
profile `h_a(ω) = ρ̂_k(-ω) g(ωa)` required by `thm:weak-sobolev-synthesis`. -/
theorem prop_nonbandpass_sobolev_vi [CompleteSpace Y] (k : ℕ) (v : Y) {s : ℝ} (hs : 0 ≤ s)
    (a : H) :
    MemRaySobolev s (fun b => gaussRayCoefficient k v (a, b)) ∧
      ∀ ω : ℝ, rayProfile (fun b => gaussRayCoefficient k v (a, b)) ω =
        filterFourier (gaussDerivFilter k) (-ω) • gaussTarget v (ω • a) := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(vii) The Sobolev mass `𝔅_s(ρ_k, g)` is finite in
the range `2k > α + 2s - 1/2` of `eq:nonbandpass-order`. -/
theorem prop_nonbandpass_sobolev_vii {k : ℕ} {α s : ℝ} (hα : 0 < α) (hs : 0 ≤ s)
    (hk : α + 2 * s - 1 / 2 < 2 * k) {ν : Measure H} (hν : IsHomogeneous α ν)
    (hB : ν (Metric.closedBall 0 1) ≠ ⊤) (v : Y) :
    ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖) ^ s *
      raySobolevNorm s fun b => gaussRayCoefficient k v (a, b)) ∂ν ≠ ⊤ := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(viii) The Sobolev test
`q_{α,ρ_k}(ω) = ρ̂_k(-ω) |ω|^{-α}` lies in `H^s_ω(ℝ)` in the same range. -/
theorem prop_nonbandpass_sobolev_viii {k : ℕ} {α s : ℝ} (hα : 0 < α) (hs : 1 / 2 < s)
    (hk : α + 2 * s - 1 / 2 < 2 * k) :
    MemRaySobolev s (gaussSobolevRay k α) ∧
      ∀ ω : ℝ, rayProfile (gaussSobolevRay k α) ω =
        filterFourier (gaussDerivFilter k) (-ω) * ((|ω| ^ (-α) : ℝ) : ℂ) := by

Status: verified by comparator.

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

/-- **Proposition [prop:nonbandpass-sobolev]**(ix) Consequently the filter satisfies every
hypothesis of `thm:weak-sobolev-synthesis`: for each continuous activation of growth order
`p < s - 1/2` the synthesis of the rays is absolutely convergent and reproduces the target. -/
theorem prop_nonbandpass_sobolev_ix [CompleteSpace Y] {k : ℕ} {α s p Cσ : ℝ} (hα : 0 < α)
    (hp : 0 ≤ p) (hps : p + 1 / 2 < s) (hk : α + 2 * s - 1 / 2 < 2 * k)
    {ν : Measure H} [SFinite ν] (hν : IsHomogeneous α ν)
    (hB : ν (Metric.closedBall 0 1) ≠ ⊤) (v : Y) {σ : ℝ → ℂ} (hσc : Continuous σ)
    (hσg : ∀ t : ℝ, ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p) (x : H) :
    ∫ q : H × ℝ, σ (⟪q.1, x⟫ - q.2) • gaussRayCoefficient k v q ∂(ν.prod volume) =
      sobolevPairing σ (gaussSobolevRay k α) • spectralTarget ν (gaussTarget v) x := by

Status: verified by comparator.