The article convention in terms of Mathlib's `𝓕`: rescaling the frequency by `(2π)⁻¹`
turns `ĝ(ζ) = ∫ g(z) e^{-i z ζ} dz` into `𝓕 g`. This is the bridge used whenever a Mathlib
Fourier theorem has to be transported to the angular convention. 

A polynomial has vanishing Fourier data away from the origin: its distributional Fourier
transform is a combination of derivatives of `δ`, all supported at the origin. 

**Example 5.2**: a polynomial activation is never admissible, `K_{ψ,η} = 0` for every `ψ`.

The manuscript exhibits `η(z) = z`, `ψ = Λ G` with `G` the Gaussian, for which the two
groupings of `pv (1/|ζ|) × |ζ| G(ζ) × δ(ζ)` give `0` and `G(0) ≠ 0`; the admissibility integral
`eq:defK`, which removes the origin, gives `0`. In the Lizorkin quotient the reason is
structural and needs no computation: the Fourier data of a polynomial away from the origin
vanishes, so the admissibility density does too. This is why the article takes activations in
`𝒮'(ℝ)/𝒫 ≅ 𝒮₀'(ℝ)`. 

**Example 5.3**: the unit step `z₊^0` is not admissible with a filtered ridgelet function
`Λ^m φ` whose window has `φ̂ (0) ≠ 0`; the admissibility integral diverges at the origin.

The manuscript's instance is `m = 1`, `φ = G` the Gaussian and
`η(z) = z₊^0 + (2π)^{-1} e^{iz}`, where `K_{ψ,η} = ∞ + G(1)`. The second summand of `η` has a
point mass of `η̂` away from the origin and is outside the function-level framework, but it is
not the source of the divergence: by `l1_isAdmissiblePair_lambdaOperatorPow` the admissibility
density of `(Λ^m φ, z₊^0)` is `conj (φ̂ ζ) / (i ζ)`, which is not absolutely integrable at the
origin as soon as `φ̂ (0) ≠ 0`. Removing the origin from the integral, as `eq:defK` does, is
therefore not enough to make every pair admissible — the manuscript's point. 

Section 3.1 and the `L¹ × (L^p ∩ C⁰)` row of the balancing theorem `thm:existence`, strong
form: for `f ∈ L¹(ℝ^m)` and a bounded continuous `ψ`, the Euclidean ridgelet integral converges
absolutely at every parameter and satisfies `‖R_ψ f (a, b)‖ ≤ ‖f‖₁ ‖ψ‖_∞ ‖a‖^s`. 

Remark after Definition 4.1: for a locally integrable ridgelet function the weak (Radon)
definition of the ridgelet transform coincides with the strong Euclidean one at `s = 1`, via
`a = u / α`, `b = β / α`. 

Balancing theorem `thm:existence`, `L¹ × (L^p ∩ C⁰)` row, range statement: for `f ∈ L¹(ℝ^m)`
and a continuous `ψ ∈ L^p(ℝ)` with `1 ≤ p`, the weak ridgelet transform belongs to `L^p` in the
shift `β`, uniformly in the direction `u` and the scale `α`.

The proof is the convolution form `eq:convridge`,
`R_ψ f (u, α, β) = (R[f](u, ·) ⋆ conj ψ~_α)(β)`: the Radon factor is integrable on `ℝ` by
`integrable_radonTransform` and the dilated reflected kernel is in `L^p`, so Young's inequality
`L¹ ⋆ L^p ⊆ L^p` (`MeasureTheory.Integrable.convolution_memLp`) applies. The hypothesis
`1 ≤ p` is implicit in the manuscript's use of `L^p` as a Banach space; the continuity of `ψ`
belongs to the manuscript's class `L^p ∩ C⁰` but is not needed for the membership conclusion.
The remaining rows of `tab:weakridge` require the distribution classes on `𝕐^{m+1}` and are
deferred. 

The explicit constant behind `prop:conti.L1`: in the `s = 0` normalization the ridgelet
transform of an integrable signal is bounded at *every* parameter point by the sup norm of the
ridgelet function, `‖R⁰_ψ f (a, b)‖ ≤ ‖ψ‖_∞ ‖f‖₁`, with `‖ψ‖_∞` the Schwartz seminorm `(0, 0)`.
This is the witness used by `l1_ridgeletTransform_bounded_L1_Linfty`, and it is what makes the
value of the operator-norm bound checkable rather than existential. 

Proposition 4.3 (`prop:conti.L1`) in the `s = 0` normalization: for a Schwartz ridgelet
function, the ridgelet transform is bounded from `L¹(ℝ^m)` to `L^∞(𝕐^{m+1})` with operator
norm at most `‖ψ‖_∞`; the bound in fact holds at every parameter point, which is stronger
than the essential supremum with respect to any reference measure on `𝕐^{m+1}`.

**Normalization memo (author decision 2026-07-22).** The manuscript states this proposition
in the `s = 1` normalization, where its proof bounds the operator norm by
`sup_{r,β} |r ψ(r β)|`, which is infinite for every `ψ ≠ 0`. Adding `ψ 0 = 0` and all integer
vanishing moments does not repair it: in `m = 1` take `f (x) = |x|^{-1/2} 𝟙_{|x| ≤ 1} ∈ L¹`;
then `R_ψ f (a, 0) = a^{1/2} ∫_{-a}^{a} |z|^{-1/2} conj (ψ z) dz` for `a > 0`, and a `ψ` with
`ψ̂ ∈ C_c^∞` supported away from `0`, `∫ ψ̂ = 0`, and `∫ |ζ|^{-1/2} ψ̂ ζ dζ ≠ 0` has all
integer moments vanishing while the fractional moment `∫ |z|^{-1/2} conj (ψ z) dz` is nonzero,
so `|R_ψ f (a, 0)| → ∞` as `a → ∞`. Following the author's decision, the statement is read in
the `s = 0` normalization of Section 3 (Murata's Euclidean normalization, see the remark after
`eq:eucrid`), with no moment conditions; wherever boundedness of the ridgelet transform
matters, the L1 theory may be read in the `s = 0` normalization throughout, replacing the
weighted measure `‖a‖⁻² da db` of the `s = 1` pairing by the unweighted `da db`. 

Theorem 4.5 (`thm:dual`) at function level: the dual ridgelet transform is the dual operator
of the ridgelet transform with respect to the pairing of `L²(𝕐^{m+1}, ‖a‖⁻² da db)` and
`L²(ℝ^m)`. 

Section 5.1: the Fourier data away from the origin, hence the admissibility constant
`K_{ψ,η}`, is invariant under adding a polynomial to the activation. This is the function-level
form of working in the Lizorkin quotient `𝒮'(ℝ)/polynomials ≅ 𝒮₀'(ℝ)`. 

**Theorem 5.4 (`thm:eq.ac`), the structure theorem for admissible pairs**, at function
level: the pair `(ψ, η)` is admissible if and only if the backprojection equation
`Λ^m u = conj (ψ~) ⋆ (η - Q)` is solvable by a function `u` carrying Fourier data `Fu` that is
integrable away from the origin with nonzero integral.

The equation appears in the form "the Fourier data of `conj (ψ~) ⋆ (η - Q)` is `|ζ|^m Fu`",
which is the multiplier reading of `Λ^m u = conj (ψ~) ⋆ (η - Q)`; see the *Deviations* section
of this module. The content of the right-hand side is the existence of `u` **as a function**:
by `hasFourierAwayFromOrigin_reflectedConjConvolution` and `hasFourierAwayFromOrigin_ae_eq` the
second conjunct alone is equivalent to the spectral equation `conj (ψ̂) Fη = |ζ|^m Fu`, which
merely renames the admissibility density, whereas the first conjunct is the function-level
substitute for the manuscript's Fourier duality `𝒪_M ≅ 𝒪'_C`.

Here `Λ^m` is the standard Lambda-operator power (`lambdaOperatorPow`); relative to the
article's filter `eq:bp` this rescales the solution `u` by `i^{-m}`, which affects none of the
stated conditions. 

**The admissibility constant of a pair solving the backprojection equation in spectral
form**: `K_{ψ,η} = (2π)^{m-1} ∫ û`. This is the identity that fixes the normalization of
`eq:radon.ac`; see `LeanRidgelet.l1_reconstruction_formula_radon`. 

**Sufficiency half of the structure theorem `thm:eq.ac`, spectral form.** If the
backprojection equation holds in the Fourier data sense — `conj (ψ̂) Fη = |ζ|^m û` away from the
origin — with a Schwartz solution `u` whose transform has a nonzero total integral, then the pair
`(ψ, η)` is admissible, with `K_{ψ,η} = (2π)^{m-1} ∫ û`. 

**Sufficiency half of the structure theorem `thm:eq.ac`, physical form.** If the
manuscript's backprojection equation `Λ^m u = conj (ψ~) ⋆ (η - Q)` holds pointwise for a
Schwartz solution `u` with `∫ û ≠ 0`, then the pair `(ψ, η)` is admissible, with
`K_{ψ,η} = (2π)^{m-1} ∫ û`.

For a Schwartz `u` the pointwise principal value defining `Λ^m u` converges, so the physical
form is available; the translation to the spectral form is the convolution theorem away from
the origin (`hasFourierAwayFromOrigin_reflectedConjConvolution`) together with the multiplier
property (`hasFourierAwayFromOrigin_lambdaOperatorPow`) and the uniqueness of Fourier data
(`hasFourierAwayFromOrigin_ae_eq`). The polynomial `Q` is invisible throughout
(`l1_hasFourierAwayFromOrigin_add_polynomial`), as it must be in the Lizorkin quotient. 

**`cor:const.ap` in sharpened form: exact criterion for a filtered ridgelet function.**
For a Schwartz `φ` whose filtered version `Λ^m φ` is integrable, the pair `(Λ^m φ, η)` is
admissible *if and only if* `conj (φ̂) Fη` is integrable away from the origin with nonzero
integral. The factor `|ζ|^m` of `(Λ^m φ)^` cancels the factor `|ζ|^{-m}` of the admissibility
density exactly, which is the whole mechanism of the manuscript's construction.

Integrability of `Λ^m φ` is automatic (`integrable_lambdaOperatorPow`): for even `m` the
filtered function is Schwartz, and for odd `m` it is the Hilbert transform of a derivative,
whose integral vanishes. 

**Corollary 5.5 (`cor:const.ap`), construction of admissible pairs**: if `ψ₀` is a Schwartz
function with `∫ ζ^k conj (ψ̂₀ ζ) Fη ζ dζ` absolutely convergent and nonzero, then
`ψ = Λ^m ψ₀^{(k)}` is admissible with `η`.

**Deviations from the article (2026-08-05).**
* The integrability of the constructed ridgelet function is a hypothesis. It is automatic for
  even `m` (`Λ^m ψ₀^{(k)} = ± ψ₀^{(m+k)}` is Schwartz) and, for odd `m`, is the `L¹` decay
  estimate for the Hilbert transform of a Schwartz function still missing from the development;
  it also holds whenever `ψ̂₀` vanishes near the origin, since then `Λ^m ψ₀^{(k)}` is Schwartz.
  The manuscript takes admissible pairs in `𝒮(ℝ) × 𝒮'(ℝ)`, but for odd `m` the constructed
  `ψ` is *not* Schwartz: its Fourier transform `|ζ|^m (iζ)^k ψ̂₀ ζ` is continuous and rapidly
  decreasing yet not smooth at the origin, so `ψ` only decays algebraically. This is why
  `IsAdmissiblePair` asks for `Integrable ψ` (paper gap memo, 2026-07-19).
* The manuscript's continuity hypothesis on `ζ^k η̂ (ζ)` near the origin is dropped: it serves
  to make the admissibility integral converge near the origin, which the explicit integrability
  hypothesis already provides. 

The angular derivative rule iterated: `(φ^{(k)})^(ζ) = (i ζ)^k φ̂(ζ)`.