8.5.1. Definition 5.1 — Regularized synthesis (def:regularized-synthesis)🔗

Blueprint node: Definition 4.1.2. Status: verified (all 6 Lean theorems verified).

Formalization note. A real β ∈ 𝒮'(ℝ) is a TemperedDistribution ℝ ℂ fixed by the vendored distributional conjugation (IsRealDistribution); χ and (η_ε) are functions with the predicates IsCutoff ρ χ (even, C_c^∞(ℝ∖{0}), = 1 on a neighbourhood of supp ρ̂) and IsApproximateIdentity η (each η_ε smooth, compactly supported, even, nonnegative, of integral one, supports shrinking to {0}); β̂ * η_ε is the pairing ⟨β̂, η_ε(ω - ·)⟩ and β_ε is the real Schwartz map with Fourier transform χ(β̂ * η_ε), obtained by choice (junk 0). 𝓔_α', R_ρ on 𝓔_α ≅ 𝒦_α, and S_ρ = R_ρ' are the Section 4 objects SpectralAntiDual μ ν (= spectralRange μ ν →L⋆[ℂ] ℂ), ridgeletExtension μ ν ρ (the bounded extension of Theorem B(ii), chosen from its defining property) and synthesis μ ν ρ γ = (innerSLFlip ℂ γ).comp (ridgeletExtension μ ν ρ) of Reconstruction/Defs, so that S_{β_ε} γ = regularizedSynthesis = synthesis μ ν β_ε γ and (S_{β_ε} γ)[g] = ⟨γ, R_{β_ε} g⟩ holds by definition (the earlier local stand-ins Tempered.spectralAntiDual, Tempered.ridgeletExtension = G ↦ W_ρ G, and the choice-based Tempered.synthesisFunctional were removed in favour of these). S_β γ is the limit of S_{β_ε} γ in the norm of 𝓔_α' along ε ↓ 0, obtained by choice whenever it exists (junk 0). Parts i–vi are the claims implicit in the definition: existence of χ and of (η_ε), β̂_ε ∈ C_c^∞(ℝ∖{0}), existence and uniqueness of β_ε, and well-definedness of S_{β_ε} γ for γ ∈ Ran R_ρ = ridgeletRange μ ν ρ (part vi, which is now rfl).

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

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

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

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

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

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

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

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

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

/-- **Definition [def:regularized-synthesis]** Regularized synthesis.  For a band-pass `ρ` there
is an even `χ ∈ C_c^∞(ℝ ∖ {0})` equal to one on a neighbourhood of `supp ρ̂`. -/
theorem def_regularized_synthesis_i (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) :
    ∃ χ : ℝ → ℝ, IsCutoff ρ χ := by

Status: verified by comparator.

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

/-- **Definition [def:regularized-synthesis]** Regularized synthesis.  There is an even,
compactly supported, smooth approximate identity `(η_ε)_{ε>0}`. -/
theorem def_regularized_synthesis_ii : ∃ η : ℝ → ℝ → ℝ, IsApproximateIdentity η := by

Status: verified by comparator.

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

/-- **Definition [def:regularized-synthesis]** Regularized synthesis.  For real `β`, band-pass
`ρ`, a cutoff `χ`, and an approximate identity `(η_ε)`, the regularized spectrum
`β̂_ε = χ (β̂ * η_ε)` belongs to `C_c^∞(ℝ ∖ {0})` for every `ε > 0`. -/
theorem def_regularized_synthesis_iii (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β)
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε) :
    ContDiff ℝ (⊤ : ℕ∞) (regularizedSpectrum β χ η ε) ∧
      HasCompactSupport (regularizedSpectrum β χ η ε) ∧
      (0 : ℝ) ∉ tsupport (regularizedSpectrum β χ η ε) := by

Status: verified by comparator.

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

/-- **Definition [def:regularized-synthesis]** Regularized synthesis.  There is a real Schwartz
function `β_ε` with `β̂_ε = χ (β̂ * η_ε)`: the chosen `regularizedActivation` has this Fourier
transform. -/
theorem def_regularized_synthesis_iv (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β)
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε) :
    ∀ ω : ℝ, filterFourier (regularizedActivation β χ η ε) ω = regularizedSpectrum β χ η ε ω := by

Status: verified by comparator.

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

/-- **Definition [def:regularized-synthesis]** Regularized synthesis.  The real Schwartz function
`β_ε` with `β̂_ε = χ (β̂ * η_ε)` is unique. -/
theorem def_regularized_synthesis_v (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β)
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε) :
    ∀ b : SchwartzMap ℝ ℝ, (∀ ω : ℝ, filterFourier b ω = regularizedSpectrum β χ η ε ω) →
      b = regularizedActivation β χ η ε := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Definition [def:regularized-synthesis]** Regularized synthesis.  For `γ ∈ Ran R_ρ` the
regularized synthesis `S_{β_ε} γ = R'_{β_ε} γ` is a well-defined element of `𝓔_α'`: it is the
continuous anti-linear functional `g ↦ ⟨γ, R_{β_ε} g⟩_{L²(λ)}` (in the representation of
`OperatorRidgelet.Reconstruction.Defs`, where `S_ρ` is the transpose of the bounded extension
`R_ρ`, this holds by definition). -/
theorem def_regularized_synthesis_vi (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε) (γ : Lp ℂ 2 (parameterMeasure ν))
    (hγ : γ ∈ ridgeletRange μ ν ρ) :
    ∀ g : spectralRange μ ν,
      regularizedSynthesis μ ν β χ η ε γ g =
        inner ℂ (ridgeletExtension μ ν (regularizedActivation β χ η ε) g) γ := by

Status: verified by comparator.

8.5.2. Theorem 5.2 — Reconstruction with a tempered activation (thm:tempered-reconstruction)🔗

Blueprint node: Theorem 4.1.3. Status: verified (all 6 Lean theorems verified).

Formalization note. Stated for the abstract pair (μ, ν) of Appendix H (ν σ-finite, full support, homogeneous of degree α), of which the Gaussian pair is the instance; f ∈ 𝓔_α is f : spectralRange μ ν and R_ρ f is the Section 4 extension ridgeletExtension μ ν ρ f (Theorem B(ii); its identification with W_ρ f is Theorem C(iii)). Parts: existence of the limit in SpectralAntiDual μ ν, independence of χ and (η_ε), the frame identity S_β R_ρ f = C^{(α)}_{β,ρ} T_α f with T_α = rieszMap μ ν = innerSLFlip ℂ (T_α f [g] = ⟨f,g⟩_𝓔 = ⟪g,f⟫ in Mathlib's inner product), the two reconstruction formulas with T_α⁻¹ = rieszInv μ ν (the Riesz representation through InnerProductSpace.toDual, from Reconstruction/Defs; the local Tempered.* stand-ins were removed), and the existence of a band-pass ρ with C ≠ 0 for non-polynomial β (¬ IsPolynomialDistribution β: β does not act by integration against a polynomial, which is β ≠ 0 in 𝒮'/𝒫).

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

/-- **Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  For
every `f ∈ 𝓔_α` the limit `S_β R_ρ f = lim_{ε ↓ 0} S_{β_ε} R_ρ f` exists in `𝓔_α'`. -/
theorem thm_tempered_reconstruction_i (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (f : spectralRange μ ν) :
    ∃ F : SpectralAntiDual μ ν,
      Tendsto (fun ε : ℝ => regularizedSynthesis μ ν β χ η ε (ridgeletExtension μ ν ρ f))
        (𝓝[>] 0) (𝓝 F) := by

Status: verified by comparator.

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

/-- **Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  The
limit `S_β R_ρ f` does not depend on the cutoff `χ` or on the approximate identity `(η_ε)`. -/
theorem thm_tempered_reconstruction_ii (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (χ χ' : ℝ → ℝ) (hχ : IsCutoff ρ χ) (hχ' : IsCutoff ρ χ')
    (η η' : ℝ → ℝ → ℝ) (hη : IsApproximateIdentity η) (hη' : IsApproximateIdentity η')
    (f : spectralRange μ ν) :
    temperedSynthesis μ ν β χ η (ridgeletExtension μ ν ρ f) =
      temperedSynthesis μ ν β χ' η' (ridgeletExtension μ ν ρ f) := by

Status: verified by comparator.

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

/-- **Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  The
frame identity `S_β R_ρ f = C^{(α)}_{β,ρ} T_α f` for `f ∈ 𝓔_α`. -/
theorem thm_tempered_reconstruction_iii (μ ν : Measure H) [IsProbabilityMeasure μ]
    [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (f : spectralRange μ ν) :
    temperedSynthesis μ ν β χ η (ridgeletExtension μ ν ρ f) =
      temperedAdmissibilityConst α β ρ • rieszMap μ ν f := by

Status: verified by comparator.

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

/-- **Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  If
`C^{(α)}_{β,ρ} ≠ 0`, then `f = (C^{(α)}_{β,ρ})⁻¹ T_α⁻¹ S_β R_ρ f` for `f ∈ 𝓔_α`. -/
theorem thm_tempered_reconstruction_iv (μ ν : Measure H) [IsProbabilityMeasure μ]
    [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (hC : temperedAdmissibilityConst α β ρ ≠ 0)
    (f : spectralRange μ ν) :
    f = (temperedAdmissibilityConst α β ρ)⁻¹ •
      rieszInv μ ν
        (temperedSynthesis μ ν β χ η (ridgeletExtension μ ν ρ f)) := by

Status: verified by comparator.

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

/-- **Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  If
`C^{(α)}_{β,ρ} ≠ 0`, then `g = (C^{(α)}_{β,ρ})⁻¹ S_β (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`. -/
theorem thm_tempered_reconstruction_v (μ ν : Measure H) [IsProbabilityMeasure μ]
    [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (β : TemperedDistribution ℝ ℂ) (hβ : IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (χ : ℝ → ℝ) (hχ : IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
    (hη : IsApproximateIdentity η) (hC : temperedAdmissibilityConst α β ρ ≠ 0)
    (g : SpectralAntiDual μ ν) :
    g = (temperedAdmissibilityConst α β ρ)⁻¹ •
      temperedSynthesis μ ν β χ η
        (ridgeletExtension μ ν ρ (rieszInv μ ν g)) := by

Status: verified by comparator.

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

/-- **Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  If
`β` is not a polynomial (equivalently `β ≠ 0` in `𝒮'/𝒫`), then a band-pass `ρ` with
`C^{(α)}_{β,ρ} ≠ 0` exists. -/
theorem thm_tempered_reconstruction_vi {α : ℝ} (hα : 0 < α) (β : TemperedDistribution ℝ ℂ)
    (hβ : IsRealDistribution β) (hpoly : ¬ IsPolynomialDistribution β) :
    ∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧ temperedAdmissibilityConst α β ρ ≠ 0 := by

Status: verified by comparator.

8.5.3. Corollary 5.3 — ReLU is admissible (cor:relu-admissible)🔗

Blueprint node: Corollary 4.1.4. Status: verified (all 8 Lean theorems verified).

Formalization note. ReLU is the vendored reluTemperedDistribution 2 (acts by integration against max(t,0)). The Fourier identity ReLU^ = -fp(ω^{-2}) + iπδ₀' is stated tested against every Schwartz φ as the finite-part limit formula lim_{ε↓0}(∫_{|ω|>ε} φ ω^{-2} - 2φ(0)/ε) = -⟨ReLU^, φ⟩ - iπ φ'(0) (part i; fp is not constructed as a distribution), and away from the origin as ⟨ReLU^, φ⟩ = ∫ -ω^{-2} φ for φ supported away from 0 (part ii). 'ρ̂ nonzero, even, nonpositive' is IsBandPass ρ (includes ρ ≠ 0) with ρ̂ real, even, of nonpositive real part. Parts iii–iv: the constant equals -(2π)⁻¹ ∫ ρ̂(ω)|ω|^{-α-2} (reluAdmissibilityScale) and is positive; v: the rescaled filter reluNormalizedFilter is band-pass with constant one; vi–vii: the two reconstruction formulas of thm:tempered-reconstruction with ReLU synthesis and the rescaled filter (rieszInv, ridgeletExtension of Reconstruction/Defs); viii: Theorem A(iii) with ReLU synthesis, stated exactly as the instance b = ReLU of thm_A_iii_a–c: the frequency window is IsFrequencyWindow ρ I (symmetric compact I ⊆ ℝ∖{0} containing supp ρ̂, previously four separate hypotheses), regularity along rays is IsRegularAlongRays ν I G (ℝ≥0∞-valued ray moments), and g_G = spectralTarget ν G; the earlier local Tempered.IsRayRegular (real-valued ray bound, Bochner-integrable moment) and Tempered.spectralTarget were removed.

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

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

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

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  Under the manuscript's convention
`ReLU^ = -fp(ω^{-2}) + iπ δ₀'`: tested against a Schwartz function `φ`, the Hadamard finite part
`⟨fp(ω^{-2}), φ⟩ = lim_{ε ↓ 0} (∫_{|ω|>ε} φ(ω) ω^{-2} dω - 2 φ(0)/ε)` equals
`-⟨ReLU^, φ⟩ - iπ φ'(0)`. -/
theorem cor_relu_admissible_i :
    ∀ φ : SchwartzMap ℝ ℂ,
      Tendsto (fun ε : ℝ => (∫ ω in {ω : ℝ | ε < |ω|}, φ ω / (ω : ℂ) ^ 2) - 2 * φ 0 / (ε : ℂ))
        (𝓝[>] 0)
        (𝓝 (-(angularFourierDistribution reluDistribution φ) -
          (Real.pi : ℂ) * Complex.I * deriv φ 0)) := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  Away from the origin `ReLU^` equals
`-ω^{-2}`: `⟨ReLU^, φ⟩ = ∫ (-ω^{-2}) φ(ω) dω` for every Schwartz `φ` supported away from `0`. -/
theorem cor_relu_admissible_ii :
    ∀ φ : SchwartzMap ℝ ℂ, (0 : ℝ) ∉ tsupport φ →
      angularFourierDistribution reluDistribution φ = ∫ ω : ℝ, -((ω : ℂ) ^ 2)⁻¹ * φ ω := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  If `ρ̂ ∈ C_c^∞(ℝ ∖ {0})` is
nonzero, even, and nonpositive, then `C^{(α)}_{ReLU,ρ} = -(2π)⁻¹ ∫ ρ̂(ω) |ω|^{-α-2} dω`. -/
theorem cor_relu_admissible_iii {α : ℝ} (hα : 0 < α) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (hρ_real : ∀ ω : ℝ, (filterFourier ρ ω).im = 0)
    (hρ_even : ∀ ω : ℝ, filterFourier ρ (-ω) = filterFourier ρ ω)
    (hρ_nonpos : ∀ ω : ℝ, (filterFourier ρ ω).re ≤ 0) :
    temperedAdmissibilityConst α reluDistribution ρ = (reluAdmissibilityScale α ρ : ℂ) := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  Under the same hypotheses the
constant `-(2π)⁻¹ ∫ ρ̂(ω) |ω|^{-α-2} dω` is positive. -/
theorem cor_relu_admissible_iv {α : ℝ} (hα : 0 < α) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (hρ_real : ∀ ω : ℝ, (filterFourier ρ ω).im = 0)
    (hρ_even : ∀ ω : ℝ, filterFourier ρ (-ω) = filterFourier ρ ω)
    (hρ_nonpos : ∀ ω : ℝ, (filterFourier ρ ω).re ≤ 0) :
    0 < reluAdmissibilityScale α ρ := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  After rescaling, `ρ` is still
band-pass and `C^{(α)}_{ReLU,ρ} = 1`. -/
theorem cor_relu_admissible_v {α : ℝ} (hα : 0 < α) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (hρ_real : ∀ ω : ℝ, (filterFourier ρ ω).im = 0)
    (hρ_even : ∀ ω : ℝ, filterFourier ρ (-ω) = filterFourier ρ ω)
    (hρ_nonpos : ∀ ω : ℝ, (filterFourier ρ ω).re ≤ 0) :
    IsBandPass (reluNormalizedFilter α ρ) ∧
      temperedAdmissibilityConst α reluDistribution (reluNormalizedFilter α ρ) = 1 := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  With the rescaled filter the first
reconstruction formula holds with ReLU synthesis for every `α > 0`:
`f = T_α⁻¹ S_{ReLU} R_ρ f` for `f ∈ 𝓔_α`. -/
theorem cor_relu_admissible_vi (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (hρ_real : ∀ ω : ℝ, (filterFourier ρ ω).im = 0)
    (hρ_even : ∀ ω : ℝ, filterFourier ρ (-ω) = filterFourier ρ ω)
    (hρ_nonpos : ∀ ω : ℝ, (filterFourier ρ ω).re ≤ 0) (χ : ℝ → ℝ)
    (hχ : IsCutoff (reluNormalizedFilter α ρ) χ) (η : ℝ → ℝ → ℝ) (hη : IsApproximateIdentity η)
    (f : spectralRange μ ν) :
    f = rieszInv μ ν
      (temperedSynthesis μ ν reluDistribution χ η
        (ridgeletExtension μ ν (reluNormalizedFilter α ρ) f)) := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  With the rescaled filter the second
reconstruction formula holds with ReLU synthesis for every `α > 0`:
`g = S_{ReLU} (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`. -/
theorem cor_relu_admissible_vii (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsBandPass ρ) (hρ_real : ∀ ω : ℝ, (filterFourier ρ ω).im = 0)
    (hρ_even : ∀ ω : ℝ, filterFourier ρ (-ω) = filterFourier ρ ω)
    (hρ_nonpos : ∀ ω : ℝ, (filterFourier ρ ω).re ≤ 0) (χ : ℝ → ℝ)
    (hχ : IsCutoff (reluNormalizedFilter α ρ) χ) (η : ℝ → ℝ → ℝ) (hη : IsApproximateIdentity η)
    (g : SpectralAntiDual μ ν) :
    g = temperedSynthesis μ ν reluDistribution χ η
      (ridgeletExtension μ ν (reluNormalizedFilter α ρ) (rieszInv μ ν g)) := by

Status: verified by comparator.

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

/-- **Corollary [cor:relu-admissible]** ReLU is admissible.  With the rescaled filter Theorem
A(iii) holds with ReLU synthesis for every `α > 0`: for `G` regular along rays and every `x`,
the inner integral `∫ γ_G(a,c) ReLU(⟪a,x⟫ + c) dc` converges absolutely for `ν`-almost every
`a`, its `ν`-integral converges absolutely, and it equals `g_G(x)`. -/
theorem cor_relu_admissible_viii (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
    (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (hρ_real : ∀ ω : ℝ, (filterFourier ρ ω).im = 0)
    (hρ_even : ∀ ω : ℝ, filterFourier ρ (-ω) = filterFourier ρ ω)
    (hρ_nonpos : ∀ ω : ℝ, (filterFourier ρ ω).re ≤ 0) (I : Set ℝ) (hI : IsFrequencyWindow ρ I)
    (G : H → ℂ) (hG : IsRegularAlongRays ν I G) :
    ∀ x : H,
      (∀ᵐ a ∂ν, Integrable fun c : ℝ =>
        coefficientFormula (reluNormalizedFilter α ρ) G (a, c) * (relu (⟪a, x⟫ + c) : ℂ)) ∧
      Integrable (fun a : H => ∫ c : ℝ,
        coefficientFormula (reluNormalizedFilter α ρ) G (a, c) * (relu (⟪a, x⟫ + c) : ℂ)) ν ∧
      ∫ a : H, (∫ c : ℝ,
        coefficientFormula (reluNormalizedFilter α ρ) G (a, c) * (relu (⟪a, x⟫ + c) : ℂ)) ∂ν =
        spectralTarget ν G x := by

Status: verified by comparator.

8.5.4. Example 5.4 — Standard activations (ex:standard-activations)🔗

Blueprint node: Proposition 4.2.3. Status: verified (all 16 Lean theorems verified).

Formalization note. The three properties (membership in 𝒜_{0,2}, global Lipschitz continuity, not a polynomial) are the theorems of lem:standard-activation-class (shared); 'covered by thm:tempered-reconstruction, thm:A(iii), and Section 6' is stated as its instance: for every α > 0 there is a band-pass ρ with C^{(α)}_{β,ρ} ≠ 0, for β = ReLU, tanh, Φ = gaussianCdfDistribution, e^{-u²/2} = gaussianDistribution (the last two realized through weightedDistribution 2, which acts by integration against the function).

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.ex_standard_activations_relu, theorem in Challenge/Tempered.lean:

/-- **Example [ex:standard-activations]** Standard activations.  ReLU is covered by Theorem
`thm:tempered-reconstruction`, Theorem A(iii), and the finite-width bounds: for every `α > 0`
there is a band-pass `ρ` with `C^{(α)}_{ReLU,ρ} ≠ 0`. -/
theorem ex_standard_activations_relu {α : ℝ} (hα : 0 < α) :
    ∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧ temperedAdmissibilityConst α reluDistribution ρ ≠ 0 := by

Status: verified by comparator.

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

/-- **Example [ex:standard-activations]** Standard activations.  `tanh` is covered by Theorem
`thm:tempered-reconstruction`, Theorem A(iii), and the finite-width bounds: for every `α > 0`
there is a band-pass `ρ` with `C^{(α)}_{tanh,ρ} ≠ 0`. -/
theorem ex_standard_activations_tanh {α : ℝ} (hα : 0 < α) :
    ∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧ temperedAdmissibilityConst α tanhDistribution ρ ≠ 0 := by

Status: verified by comparator.

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

/-- **Example [ex:standard-activations]** Standard activations.  The Gaussian distribution
function `Φ` is covered by Theorem `thm:tempered-reconstruction`, Theorem A(iii), and the
finite-width bounds: for every `α > 0` there is a band-pass `ρ` with `C^{(α)}_{Φ,ρ} ≠ 0`. -/
theorem ex_standard_activations_gaussianCdf {α : ℝ} (hα : 0 < α) :
    ∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧
      temperedAdmissibilityConst α gaussianCdfDistribution ρ ≠ 0 := by

Status: verified by comparator.

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

/-- **Example [ex:standard-activations]** Standard activations.  The Gaussian `e^{-u²/2}` is
covered by Theorem `thm:tempered-reconstruction`, Theorem A(iii), and the finite-width bounds:
for every `α > 0` there is a band-pass `ρ` with `C^{(α)}_{e^{-u²/2},ρ} ≠ 0`. -/
theorem ex_standard_activations_gaussian {α : ℝ} (hα : 0 < α) :
    ∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧
      temperedAdmissibilityConst α gaussianDistribution ρ ≠ 0 := by

Status: verified by comparator.

8.5.5. Theorem 5.6 — Absolute synthesis from weak Sobolev regularity along rays (thm:weak-sobolev-synthesis)🔗

Blueprint node: Theorem 4.3.3. Status: verified (all 5 Lean theorems verified).

Formalization note. New in the 2026-09-13 revision; taken from supp.tex supp:thm:weak-sobolev-synthesis. Absolute synthesis for filters that need not be band pass, under Sobolev regularity of order s along rays. Formalized in the pair formulation of OperatorRidgelet.Sobolev.Defs: hypothesis 1 of the manuscript, a jointly measurable coefficient whose bias lines are the ray coefficients, is a jointly measurable γ : H × ℝ → Y (hγm) whose rays satisfy MemRaySobolev s (γ(a,·)) and rayProfile (γ(a,·)) ω = ρ̂(-ω) • g(ω a) for ν-almost every a; 𝔅_s(ρ,g) is the lower integral ∫⁻ (1+‖a‖)^s ‖h_a‖_{H^s_ω} dν, assumed finite. Hypothesis 3 is MemRaySobolev s γq together with rayProfile γq ω = ρ̂(-ω)|ω|^{-α}, and the cross constant C^{(α)}_{σ,ρ} = (2π)⁻¹⟨σ̂, q_{α,ρ}⟩ is the Sobolev pairing sobolevPairing σ γq of lem:sobolev-pairing. i is eq:sobolev-moments for every 0 ≤ r < s - 1/2; ii is the finite variation of Γ_g; iii is eq:weak-sobolev-synthesis, stated as the Bochner integral of σ(⟪a,x⟫ - b) • γ(a,b) over ν ⊗ db — this theorem is written in the manuscript's bias convention, since its coefficient is defined by its own Fourier relation, and the library lemma OperatorRidgelet.integral_synthesis_eq_integralNetworkDensity rewrites it as integralNetworkDensity of the transported coefficient γ ∘ τ, τ(a,c) = (a,-c); iv is the uniform integrable majorant on a ball of inputs; v is the continuity of the synthesis. Only strong measurability of g is needed for iii, as in the manuscript, which derives g ∈ L¹(ν;Y) from hypotheses 1 and 2; the final clause of the manuscript statement, that γ_g lies in L²(ν ⊗ db) with ‖γ_g‖² = ((ρ,ρ))_α ‖g‖²_{L²(ν)} when Y is Hilbert and g ∈ L²(ν;Y), is not part of the Lean statement. Neither the Lean statement nor the manuscript uses the inner product or separability of Y, the separability or completeness of H, or the admissibility of ρ, for iii.

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

/-- **Theorem [thm:weak-sobolev-synthesis]**(i) The coefficient moments `eq:sobolev-moments`:
for `0 ≤ r < s - 1/2`,
`∫ (1 + ‖a‖ + |b|)^r ‖γ_g(a,b)‖ dν db ≤ 2^{r/2} A_{s,r} 𝔅_s(ρ,g)`. -/
theorem thm_weak_sobolev_synthesis_i [CompleteSpace Y] {s r : ℝ} (hr0 : 0 ≤ r) (hrs : r + 1 / 2 < s)
    (ν : Measure H) [SFinite ν] {γ : H × ℝ → Y} (hγm : StronglyMeasurable γ)
    (hray : ∀ᵐ a ∂ν, MemRaySobolev s fun b => γ (a, b)) :
    ∫⁻ q : H × ℝ, ENNReal.ofReal ((1 + ‖q.1‖ + |q.2|) ^ r * ‖γ q‖) ∂(ν.prod volume) ≤
      ENNReal.ofReal ((2 : ℝ) ^ (r / 2) * sobolevMomentConst s r) *
        ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖) ^ s * raySobolevNorm s fun b => γ (a, b)) ∂ν := by

Status: verified by comparator.

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

/-- **Theorem [thm:weak-sobolev-synthesis]**(ii) The coefficient measure
`Γ_g = γ_g (ν ⊗ db)` is finite. -/
theorem thm_weak_sobolev_synthesis_ii [CompleteSpace Y] {s : ℝ} (hs : 1 / 2 < s)
    (ν : Measure H) [SFinite ν]
    {γ : H × ℝ → Y} (hγm : StronglyMeasurable γ)
    (hray : ∀ᵐ a ∂ν, MemRaySobolev s fun b => γ (a, b))
    (hB : ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖) ^ s * raySobolevNorm s fun b => γ (a, b)) ∂ν ≠ ⊤) :
    Integrable γ (ν.prod volume) := by

Status: verified by comparator.

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

/-- **Theorem [thm:weak-sobolev-synthesis]**(iii) The synthesis identity
`eq:weak-sobolev-synthesis`: the ordinary, absolutely convergent synthesis of the coefficient
is `C^{(α)}_{σ,ρ} f_g`, the cross constant being the Sobolev pairing of `σ` with the coefficient
of `q_{α,ρ}`. -/
theorem thm_weak_sobolev_synthesis_iii [CompleteSpace Y] {s p α Cσ : ℝ} (hp : 0 ≤ p)
    (hps : p + 1 / 2 < s)
    {ν : Measure H} [SFinite ν] (hν : IsHomogeneous α ν) {ρ : SchwartzMap ℝ ℝ}
    {g : H → Y} (hgm : StronglyMeasurable g) {σ : ℝ → ℂ} (hσc : Continuous σ)
    (hσg : ∀ t : ℝ, ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p) {γ : H × ℝ → Y} (hγm : StronglyMeasurable γ)
    (hray : ∀ᵐ a ∂ν, MemRaySobolev s fun b => γ (a, b))
    (hprofile : ∀ᵐ a ∂ν, ∀ ω : ℝ,
      rayProfile (fun b => γ (a, b)) ω = filterFourier ρ (-ω) • g (ω • a))
    (hB : ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖) ^ s * raySobolevNorm s fun b => γ (a, b)) ∂ν ≠ ⊤)
    {γq : ℝ → ℂ} (hγq : MemRaySobolev s γq)
    (hqprofile : ∀ ω : ℝ, rayProfile γq ω = filterFourier ρ (-ω) * ((|ω| ^ (-α) : ℝ) : ℂ))
    (x : H) :
    ∫ q : H × ℝ, σ (⟪q.1, x⟫ - q.2) • γ q ∂(ν.prod volume) =
      sobolevPairing σ γq • spectralTarget ν g x := by

Status: verified by comparator.

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

/-- **Theorem [thm:weak-sobolev-synthesis]**(iv) The absolute convergence is uniform on bounded
input sets: on `‖x‖ ≤ R` the synthesis integrand has one integrable majorant. -/
theorem thm_weak_sobolev_synthesis_iv [CompleteSpace Y] {s p Cσ R : ℝ} (hp : 0 ≤ p)
    (hps : p + 1 / 2 < s)
    {ν : Measure H} [SFinite ν] {σ : ℝ → ℂ}
    (hσg : ∀ t : ℝ, ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p) {γ : H × ℝ → Y} (hγm : StronglyMeasurable γ)
    (hray : ∀ᵐ a ∂ν, MemRaySobolev s fun b => γ (a, b))
    (hB : ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖) ^ s * raySobolevNorm s fun b => γ (a, b)) ∂ν ≠ ⊤) :
    ∃ M : H × ℝ → ℝ, Integrable M (ν.prod volume) ∧
      ∀ x : H, ‖x‖ ≤ R → ∀ q : H × ℝ, ‖σ (⟪q.1, x⟫ - q.2) • γ q‖ ≤ M q := by

Status: verified by comparator.

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

/-- **Theorem [thm:weak-sobolev-synthesis]**(v) The synthesis is continuous. -/
theorem thm_weak_sobolev_synthesis_v [CompleteSpace Y] {s p Cσ : ℝ} (hp : 0 ≤ p)
    (hps : p + 1 / 2 < s)
    {ν : Measure H} [SFinite ν] {σ : ℝ → ℂ} (hσc : Continuous σ)
    (hσg : ∀ t : ℝ, ‖σ t‖ ≤ Cσ * (1 + |t|) ^ p) {γ : H × ℝ → Y} (hγm : StronglyMeasurable γ)
    (hray : ∀ᵐ a ∂ν, MemRaySobolev s fun b => γ (a, b))
    (hB : ∫⁻ a : H, ENNReal.ofReal ((1 + ‖a‖) ^ s * raySobolevNorm s fun b => γ (a, b)) ∂ν ≠ ⊤) :
    Continuous fun x : H => ∫ q : H × ℝ, σ (⟪q.1, x⟫ - q.2) • γ q ∂(ν.prod volume) := by

Status: verified by comparator.