/-
Copyright (c) 2026 Sho Sonoda. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sho Sonoda, OpenAI Codex
-/
module

public import LeanRidgelet.HA

/-!
# Harmonic-analysis method: publication-order roadmap

Roadmap of the formalization of

> S. Sonoda, Y. Hashimoto, I. Ishikawa and M. Ikeda, *Deep Ridgelet Transform and Unified
> Universality Theorem for Deep and Shallow Joint-Group-Equivariant Machines*
> (arXiv:2405.13682).

The discovery principle is the short chain

`joint equivariance → intertwining maps → a commutant element → Schur scalarity → reconstruction`.

This file follows the article in publication order. The implementation modules are re-exported
through `LeanRidgelet.HA`, whose module documentation records their Lean dependency order.

## Sections 2 and 3: classical motivation and the abstract theorem

* Definitions 2.1 and 2.2 are represented by the affine ridge argument, its contragredient
  parameter action, and the corresponding Bochner synthesis and ridgelet formulas. Theorem 2.3 is
  identified with the classical declarations at homogeneity index zero: the affine Bochner pair is
  the Euclidean dual ridgelet transform and ridgelet transform of the L1 track, the classical
  synthesis integral of the L2 track is the same Bochner integral, and a Euclidean reconstruction
  identity reconstructs the composite with the same scalar. That identity is a hypothesis, as on
  the Fourier-slice side, because the L1 endpoints are truncated limits at index one.
* Theorem 2.4 is complete in `ToMathlib.LieGroup.Schur`. It proves the infinite-dimensional
  unitary Schur lemma and its converse using closed invariant subspaces and continuous functional
  calculus.
* For Theorem 2.5, the affine action, its Plancherel conjugate, the conull nonzero dual orbit, the
  inducing subgroup and character, the homogeneous-space `L²` model, the normalized-section
  induced model, its translation-character restriction, and its canonical indicator covariance
  are implemented. The spectral-projection criterion from Folland Theorem 4.44 is complete,
  including finite-measure density of Fourier characters. The operator-theoretic remainder of
  Theorem 6.28 is also proved using continuous spectral subspaces and the self-adjoint/skew-adjoint
  decomposition. Compact-kernel group-convolution continuity, pointwise representatives of
  `L²`-valued Bochner integrals, the approximate identity, compact cutoffs, and regular-section
  density required by Lemma 6.29 are proved. The extreme-subspace part of the inducing-fiber
  correspondence of Lemma 6.30 is now proved as well, from identity-coset evaluation of translated
  sections and from orthogonal-complement vanishing along a countable subcover of translates of a
  nonvanishing section. Lemma 6.29 is complete: the measurable induced-model lift, the slice
  integrability of its smoothing integrand, and the identification of the resulting pointwise
  convolution with the Bochner-smoothed class are proved, so Theorem 6.39 needs no analytic input.
  The one-dimensional fiber classification is proved. The induced-model and physical-space
  irreducibility theorems are unconditional.
* Definitions 3.1 and 3.2, Remark 3.3, and Lemmas 3.4 and 3.5 are implemented by the invariant or
  strongly quasi-invariant `L²` constructions and the pointwise joint-equivariance algebra.
* Definitions 3.6 and 3.8 and Lemmas 3.7 and 3.9 are implemented by the Bochner
  change-of-variables results and continuous intertwining maps. The implementation covers both
  individually bounded operators and the article's weaker bounded-extension hypothesis for the
  composite alone.
* Theorem 3.10 and Remark 3.11 are implemented as the Schur reduction and the normalized right
  inverse.

## Sections 4--8: examples and discussion

* Corollary 4.1 is proved for heterogeneous finite cascades.
* Section 5 feature covariance, the vector-valued product-group `L²` action, the standard
  complexified `O(m)` output representation, and the finite-output form of Lemma 5.1 are proved.
* The orbit-lift construction and Theorem 6.1 for group-convolutional networks are proved.
* The Section 7 quadratic-form example is carried to its endpoint. Its algebra is proved: the
  symmetric coefficients as a subspace of the self-adjoint continuous endomorphisms, the linear
  parameter action of the affine group, joint invariance of the scalar argument and hence of the
  feature for every activation, the group-action law, and the block factorization of the parameter
  determinant, whose congruence factor is computed in general. Its measure layer is proved twice:
  the quasi-invariant parameter measure and its `L²` representation, and then the relatively
  invariant measure that restores the density balance the quasi-invariant one breaks — with the
  additive Haar measure the two representations are not balanced, and no pair of intertwiners can be
  built. The reconstruction endpoint follows from bounded intertwiners by Schur, and the
  reconstruction scalar is named, computed by any probe, and shown to be nonzero as soon as one
  datum has nonzero image. The endpoint with an activation fixed in advance and an explicit
  constant is proved at a **fixed shape matrix** (`HA.QuadraticFixedShape`): for a self-adjoint
  invertible `A`, parameters the center and the level, and bounded integrable admissible profiles,
  the bounded ridgelet transform exists, the synthesis operator is its adjoint, and
  `S_σ R_ψ = c_A(σ, ψ) · id` with `c_A(σ, ψ) = ∫ 𝓕σ(ζ) conj(𝓕ψ(ζ)) π^m / (|2πζ|^m |det A|) dζ`,
  a positive real number for a common nonzero profile. See *Deviations from the article* for why
  the shape matrix is fixed. Section 8 contains no additional formal target.

The Euclidean bounded synthesis and ridgelet maps used by the examples are reused from the L2
theory through `HA.L2Bridge`; the HA development does not duplicate their boundedness proof.

## Appendices A--E

The `L²` unitarity needed from Appendix A is implemented, as are the finite-output case of its
tensor irreducibility step and the group-convolution reductions. Appendix B is covered by the
Section 2 affine instance. Appendix C's uniform approximation of an integral representation by
finite networks is proved in general form, for a Lipschitz Banach-valued integrand on a compact
metric parameter space, and specializes to bounded continuous functions on an arbitrary data space;
what remains there is its instantiation at concrete features. The Mackey route supplies most of the
input needed for Appendix E, and the Folland-6.29 measurable-lift step above completes it, so no
proof root remains there.

Appendix D is the one place where the formalization has to depart from the article; since
2026-09-08 the track has no proof root at all. Its Hilbert--Schmidt criterion is proved in
general form — a square-integrable kernel gives a bounded operator on `L²` — and instantiated for
the quadratic feature both for the feature itself (condition T2) and for the composite kernel alone
(condition T1). **Neither can give universality.** A square-integrable kernel makes the operator
compact, while a scalar operator on an infinite-dimensional space is compact only for the zero
scalar, so whenever those hypotheses hold the reconstruction constant vanishes; and for an
activation of polynomial growth, the rectified linear unit included, T2 is false outright. What the
L1 and L2 theories do instead is bound the analysis and the synthesis separately through a weighted
intermediate space, where neither operator is Hilbert--Schmidt. For the quadratic feature the weight
cannot go on the parameter measure, whose balance is pinned down above, so it goes on the
coefficient space, and the weight comes from smoothness: a derivative in the additive parameter
transfers onto the analysis feature. The intermediate space is therefore a Sobolev structure of
order `k` in the constant coefficient of the parameter, and it survives the action because the
action is a shear in that coefficient. That space is now built and not merely described: its
carrier, its completeness, its isometric action, its invariance, and its packaging as a
representation are proved, as are its seminorm, the identity computing the analysis transform's
seminorm from the features, the dual synthesis bound, and — from those two bounds — the bounded
equivariant endomorphism the Schur step consumes. A Plancherel description identifies it with the
frequency-weighted space the other route would have built, so the choice between the two was a
choice of which side to make the invariance visible on, not a choice of space.

The admissibility statement that route left open — the existence of a pair of features
satisfying both bounds and leaving the composite nonvanishing — was withdrawn on 2026-09-08 rather
than proved. Completing the square (`HA.QuadraticPositiveCone`) makes the feature family at a fixed
coefficient the translates and level shifts of one profile, and the energy identity of that family
(`ToMathlib.QuadraticLevelShift`, built on the unitarity of the chirp convolution in
`ToMathlib.QuadraticChirp`) evaluates the parameter-`L²` energy of the analysis transform at each
coefficient `A` exactly: `(∫ ‖𝓕ψ‖² π^m / (|2πζ|^m |det A|) dζ) ‖f‖²`. The geometric weight is
the hyperplane weight `|ζ|^{-m}` again, and the coefficient enters only through `|det A|⁻¹`; but
against the relatively invariant measure the coefficient marginal is the invariant measure of the
cone of shape matrices, whose mass is infinite, so no nonzero bounded integrable analysis feature
satisfies the analysis bound. What fails is the dilation direction of the parameter group, exactly
as a representation that is not square-integrable has no admissible vector. The true endpoint is
the network with one shape matrix fixed, and `HA.QuadraticFixedShape` proves it with the explicit
constant above, by the polarized energy identity — no Schur lemma is needed there, translation
equivariance and the chirp computation making the composite a Fourier multiplier that is constant
in the frequency. The second-difference reduction of the rectified linear unit to a hat function
(`HA.QuadraticSecondDifference`) is kept; combining it with the fixed-shape endpoint is future
work.

The Blueprint part `ha` has been published since 2026-08-19, with the child pages `overview-ha`,
`ha-representations`, `ha-affine`, `ha-architectures`, and `ha-quadratic`. This overview contains no
declaration or proof placeholder of its own.

## Deviations from the article

The complex reconstruction scalar is treated as sesquilinear rather than bilinear. The article's
general Bochner lemmas use invariant measures, whereas its affine examples require quasi-invariant
Lebesgue measures; `HA.BochnerIntertwining` therefore also states the corrected identities with
explicit pushforward densities and their square-root balance. `HA.Affine` derives the concrete
factors `‖det L‖₊` and `‖det L‖₊⁻¹` and instantiates that balance. For the quadratic feature the
parameter Jacobian is kept abstract where only its non-vanishing is used, but the congruence
determinant on symmetric coefficients is computed where the balance needs it, so the relative weight
`|det A|^{-(m+1)/2}` is exhibited rather than assumed. Individually bounded synthesis/ridgelet maps
and a bounded extension of their pointwise composite are exposed as separate APIs, matching the two
possible readings of the article's boundedness hypothesis. The intermediate coefficient space of the
Appendix D route is not in the article at all; it is what the L1 and L2 theories do, transported to
this parameter space. The Section 7 endpoint with an activation fixed in advance is stated with a
fixed shape matrix `A`, the parameters being the center and the level with Lebesgue measure, rather
than over the full affine parameter `(A, b, c)` with the relatively invariant measure: the
fixed-coefficient energy identity shows the analysis transform has infinite parameter-`L²` energy
against that measure for every nonzero bounded integrable profile, so the full-parameter statement
has no bounded ridgelet transform to speak of, while the fixed-shape statement is true with the
constant `c_A(σ, ψ) = ∫ 𝓕σ(ζ) conj(𝓕ψ(ζ)) π^m / (|2πζ|^m |det A|) dζ`. The reconstruction there
is stated through the adjoint synthesis operator; the pointwise synthesis integral of the analysis
transform need not converge absolutely, and its identity is proved under that convergence as a
hypothesis.
-/