4.1. Harmonic-analysis method: arXiv:2405.13682 implementation map🔗

This chapter follows Sonoda--Hashimoto--Ishikawa--Ikeda, Deep Ridgelet Transform and Unified Universality Theorem for Deep and Shallow Joint-Group-Equivariant Machines (arXiv:2405.13682), in publication order. It records article-facing coverage only; the next chapter explains helper constructions and proofs in Lean dependency order. A node without a Lean link is a deferred target and creates no assumption in the Lean project.

The formalized discovery principle is \text{joint equivariance}\Rightarrow\text{intertwiners}\Rightarrow\text{commutant} \Rightarrow\text{Schur scalarity}\Rightarrow\text{reconstruction}.

Section 2: the classical ridgelet formula and irreducibility

Definition4.1.1

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 4.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Definitions 2.1 and 2.2. The affine ridge argument, the depth-two feature, its joint invariance, and the synthesis/ridgelet Bochner covariance formulas are formalized. The bounded Euclidean operators themselves are reused from the L2 theory.

Lean code for Definition4.1.1●5 declarations

defdefined in LeanRidgelet/HA/Affine.lean

complete

def LeanRidgelet.affineRidgeArgument.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) (p : E × ℝ) : ℝ

def LeanRidgelet.affineRidgeArgument.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x : E)
  (p : E × ℝ) : ℝ

Implementation after :=

:= ⟪p.1, x⟫_ℝ - p.2

The scalar affine functional used by a ridge feature.

defdefined in LeanRidgelet/HA/Affine.lean

complete

def LeanRidgelet.affineFeature.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Y : Type u_2}
  (σ : ℝ → Y) (x : E) (p : E × ℝ) : Y

def LeanRidgelet.affineFeature.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {Y : Type u_2}
  (σ : ℝ → Y) (x : E) (p : E × ℝ) : Y

Implementation after :=

:=
  σ (affineRidgeArgument x p)

A vector-valued fully-connected depth-two feature.

theoremdefined in LeanRidgelet/HA/Affine.lean

complete

theorem LeanRidgelet.affineFeature_jointInvariant.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (σ : ℝ → Y) (g : E ≃ᵃ[ℝ] E) (x : E) (p : E × ℝ) :
  LeanRidgelet.affineFeature σ (g • x) (g • p) =
    ↑(1 g) (LeanRidgelet.affineFeature σ x p)

theorem LeanRidgelet.affineFeature_jointInvariant.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (σ : ℝ → Y)
  (g : E ≃ᵃ[ℝ] E) (x : E) (p : E × ℝ) :
  LeanRidgelet.affineFeature σ (g • x)
      (g • p) =
    ↑(1 g)
      (LeanRidgelet.affineFeature σ x p)

A fully-connected affine feature is jointly invariant; equivalently, it is jointly equivariant
for the trivial output representation.

theoremdefined in LeanRidgelet/HA/Affine.lean

complete

theorem LeanRidgelet.affineBochnerSynthesis_intertwines.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (ν : MeasureTheory.Measure (E × ℝ))
  [ν.IsAddHaarMeasure] (σ : ℝ → Y) (g : E ≃ᵃ[ℝ] E) (γ : E × ℝ → ℂ)
  (x : E) :
  LeanRidgelet.bochnerSynthesis ν (LeanRidgelet.affineFeature σ)
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineParameterJacobian)
        g γ)
      x =
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      (LeanRidgelet.bochnerSynthesis ν (LeanRidgelet.affineFeature σ) γ)
      x

theorem LeanRidgelet.affineBochnerSynthesis_intertwines.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (ν : MeasureTheory.Measure (E × ℝ))
  [ν.IsAddHaarMeasure] (σ : ℝ → Y)
  (g : E ≃ᵃ[ℝ] E) (γ : E × ℝ → ℂ)
  (x : E) :
  LeanRidgelet.bochnerSynthesis ν
      (LeanRidgelet.affineFeature σ)
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineParameterJacobian)
        g γ)
      x =
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      (LeanRidgelet.bochnerSynthesis ν
        (LeanRidgelet.affineFeature σ) γ)
      x

The quasi-invariant Bochner synthesis identity instantiated for the affine fully-connected
feature.

theoremdefined in LeanRidgelet/HA/Affine.lean

complete

theorem LeanRidgelet.affineBochnerRidgelet_intertwines.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ψ : ℝ → Y)
  (g : E ≃ᵃ[ℝ] E) (f : E → Y) (p : E × ℝ) :
  LeanRidgelet.bochnerRidgelet μ (LeanRidgelet.affineFeature ψ)
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1 g f)
      p =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g
      (LeanRidgelet.bochnerRidgelet μ (LeanRidgelet.affineFeature ψ) f)
      p

theorem LeanRidgelet.affineBochnerRidgelet_intertwines.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (ψ : ℝ → Y)
  (g : E ≃ᵃ[ℝ] E) (f : E → Y)
  (p : E × ℝ) :
  LeanRidgelet.bochnerRidgelet μ
      (LeanRidgelet.affineFeature ψ)
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1
        g f)
      p =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g
      (LeanRidgelet.bochnerRidgelet μ
        (LeanRidgelet.affineFeature ψ) f)
      p

The quasi-invariant Bochner ridgelet identity instantiated for the affine fully-connected
feature.

Theorem4.1.2

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Theorem 2.3. At homogeneity index zero the affine depth-two Bochner synthesis and ridgelet are the classical Euclidean dual ridgelet transform and ridgelet transform on the nose, and the classical synthesis integral of the L2 track is the same Bochner integral. Any Euclidean reconstruction identity therefore reconstructs the harmonic-analysis composite with the same scalar. That identity enters as a hypothesis, as it does on the Fourier-slice side.

Lean code for Theorem4.1.2●5 theorems

theoremdefined in LeanRidgelet/HA/ClassicalComparison.lean

complete

theorem LeanRidgelet.bochnerSynthesis_affineFeature_eq_euclideanDualRidgeletTransform
  {m : ℕ} (η : ℝ → ℂ) (T : LeanRidgelet.RidgeletParameterSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.bochnerSynthesis MeasureTheory.volume
      (LeanRidgelet.affineFeature η) T x =
    LeanRidgelet.euclideanDualRidgeletTransform m 0 η T x

theorem LeanRidgelet.bochnerSynthesis_affineFeature_eq_euclideanDualRidgeletTransform
  {m : ℕ} (η : ℝ → ℂ)
  (T :
    LeanRidgelet.RidgeletParameterSpace
        m →
      ℂ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.bochnerSynthesis
      MeasureTheory.volume
      (LeanRidgelet.affineFeature η) T x =
    LeanRidgelet.euclideanDualRidgeletTransform
      m 0 η T x

The affine Bochner synthesis integral against Lebesgue measure on the ridge parameters is the
classical dual ridgelet transform at homogeneity index `s = 0`. Both sides are literally the same
integral: `•` on `ℂ` is multiplication and the weight `‖a‖^0` is `1`.

theoremdefined in LeanRidgelet/HA/ClassicalComparison.lean

complete

theorem LeanRidgelet.bochnerRidgelet_affineFeature_eq_euclideanRidgeletTransform
  {m : ℕ} (ψ : ℝ → ℂ) (f : LeanRidgelet.InputSpace m → ℂ)
  (p : LeanRidgelet.RidgeletParameterSpace m) :
  LeanRidgelet.bochnerRidgelet MeasureTheory.volume
      (LeanRidgelet.affineFeature ψ) f p =
    LeanRidgelet.euclideanRidgeletTransform m 0 ψ f p

theorem LeanRidgelet.bochnerRidgelet_affineFeature_eq_euclideanRidgeletTransform
  {m : ℕ} (ψ : ℝ → ℂ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (p :
    LeanRidgelet.RidgeletParameterSpace
      m) :
  LeanRidgelet.bochnerRidgelet
      MeasureTheory.volume
      (LeanRidgelet.affineFeature ψ) f p =
    LeanRidgelet.euclideanRidgeletTransform
      m 0 ψ f p

The affine Bochner ridgelet pairing against Lebesgue measure on the data is the classical
Euclidean ridgelet transform at homogeneity index `s = 0`. Mathlib's inner product on `ℂ` is
conjugate-linear in its first argument, which is exactly the conjugation on the analysing
function in the classical formula.

theoremdefined in LeanRidgelet/HA/ClassicalComparison.lean

complete

theorem LeanRidgelet.bochnerSynthesis_affineFeature_eq_classicalSynthesisIntegral
  {m : ℕ} (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (σcl : ℝ → ℂ) (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.bochnerSynthesis MeasureTheory.volume
      (LeanRidgelet.affineFeature σcl) (⇑γ) x =
    LeanRidgelet.classicalSynthesisIntegral γ σcl x

theorem LeanRidgelet.bochnerSynthesis_affineFeature_eq_classicalSynthesisIntegral
  {m : ℕ}
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (σcl : ℝ → ℂ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.bochnerSynthesis
      MeasureTheory.volume
      (LeanRidgelet.affineFeature σcl)
      (⇑γ) x =
    LeanRidgelet.classicalSynthesisIntegral
      γ σcl x

The affine Bochner synthesis integral of a Schwartz coefficient function is the `L²` track's
classical network integral.

theoremdefined in LeanRidgelet/HA/ClassicalComparison.lean

complete

theorem LeanRidgelet.affineBochner_reconstruction_of_euclidean {m : ℕ}
  {η ψ : ℝ → ℂ} {c : ℂ}
  (hrec :
    ∀ (F : LeanRidgelet.InputSpace m → ℂ)
      (y : LeanRidgelet.InputSpace m),
      LeanRidgelet.euclideanDualRidgeletTransform m 0 η
          (LeanRidgelet.euclideanRidgeletTransform m 0 ψ F) y =
        c * F y)
  (f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.bochnerSynthesis MeasureTheory.volume
      (LeanRidgelet.affineFeature η)
      (LeanRidgelet.bochnerRidgelet MeasureTheory.volume
        (LeanRidgelet.affineFeature ψ) f)
      x =
    c * f x

theorem LeanRidgelet.affineBochner_reconstruction_of_euclidean
  {m : ℕ} {η ψ : ℝ → ℂ} {c : ℂ}
  (hrec :
    ∀ (F : LeanRidgelet.InputSpace m → ℂ)
      (y : LeanRidgelet.InputSpace m),
      LeanRidgelet.euclideanDualRidgeletTransform
          m 0 η
          (LeanRidgelet.euclideanRidgeletTransform
            m 0 ψ F)
          y =
        c * F y)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.bochnerSynthesis
      MeasureTheory.volume
      (LeanRidgelet.affineFeature η)
      (LeanRidgelet.bochnerRidgelet
        MeasureTheory.volume
        (LeanRidgelet.affineFeature ψ) f)
      x =
    c * f x

**The classical reconstruction formula for the affine depth-two Bochner pair.** Whenever the
classical Euclidean dual ridgelet transform inverts the classical Euclidean ridgelet transform up
to a constant `c`, the affine Bochner synthesis inverts the affine Bochner ridgelet transform up
to the same constant, pointwise and with no hypothesis on the target.

The Euclidean reconstruction formula is a hypothesis rather than a fixed theorem, as in
`LeanRidgelet.fs_groupConv_synthesis_ridgelet`, so that any of them may be used; see the module
docstring for why the `L¹` endpoints of this repository do not currently supply it.

theoremdefined in LeanRidgelet/HA/ClassicalComparison.lean

complete

theorem LeanRidgelet.networkSynthesis_ae_eq_bochnerSynthesis_affineFeature
  {m : ℕ} [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  {σcl : ℝ → ℂ}
  (hσcl :
    ∀ (φ : SchwartzMap ℝ ℂ),
      ((LeanRidgelet.activationRealization s t) σ) φ =
        ∫ (z : ℝ), φ z * σcl z)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume)
  (hint :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable (fun p ↦ γ p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t σ)
          (LeanRidgelet.parameterSchwartzRealization s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.bochnerSynthesis MeasureTheory.volume
      (LeanRidgelet.affineFeature σcl) ⇑γ

theorem LeanRidgelet.networkSynthesis_ae_eq_bochnerSynthesis_affineFeature
  {m : ℕ} [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  {σcl : ℝ → ℂ}
  (hσcl :
    ∀ (φ : SchwartzMap ℝ ℂ),
      ((LeanRidgelet.activationRealization
              s t)
            σ)
          φ =
        ∫ (z : ℝ), φ z * σcl z)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume)
  (hint :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable
        (fun p ↦
          γ p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t
            σ)
          (LeanRidgelet.parameterSchwartzRealization
            s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.bochnerSynthesis
      MeasureTheory.volume
      (LeanRidgelet.affineFeature σcl) ⇑γ

On the Schwartz compatibility domain of the `L²` track, the bounded synthesis operator is
almost everywhere the affine Bochner synthesis integral. This is what connects the operator-level
bridge of `LeanRidgelet.HA.L2Bridge` to the integral formulas above; the hypotheses are exactly
those of `LeanRidgelet.networkSynthesis_parameterSchwartzRealization_classical_ae`.

Definition4.1.3

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 4.1.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Unitary representations and topological irreducibility. Closed invariant subspaces, rather than algebraic subrepresentations, express the article's infinite-dimensional notion.

Lean code for Definition4.1.3●3 definitions

abbrevdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

abbrev UnitaryRepresentation.{u_3, u_4} (G : Type u_3) (H : Type u_4) [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :
  Type (max u_3 u_4)

abbrev UnitaryRepresentation.{u_3, u_4}
  (G : Type u_3) (H : Type u_4) [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] : Type (max u_3 u_4)

Implementation after :=

:=
  G →* unitary (H →L[ℂ] H)

A unitary representation of a group on a complex Hilbert space, expressed using the unitary
group of the C\*-algebra of bounded operators. No continuity in the group variable is imposed;
the Schur argument only uses the algebraic action and unitarity.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

def UnitaryRepresentation.IsInvariant.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) (K : ClosedSubmodule ℂ H) : Prop

def UnitaryRepresentation.IsInvariant.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H)
  (K : ClosedSubmodule ℂ H) : Prop

Implementation after :=

:=
  ∀ (g : G) ⦃x : H⦄, x ∈ K → (π g : H →L[ℂ] H) x ∈ K

A closed subspace is invariant under a unitary representation when every group element maps
it into itself. Since inverses also occur in the representation, inclusion automatically upgrades
to equality; the inclusion form is more convenient for applications.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

def UnitaryRepresentation.IsTopologicallyIrreducible.{u_1, u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) : Prop

def UnitaryRepresentation.IsTopologicallyIrreducible.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H) : Prop

Implementation after :=

:=
  Nontrivial H ∧ ∀ K : ClosedSubmodule ℂ H, π.IsInvariant K → K = ⊥ ∨ K = ⊤

Topological irreducibility for a unitary representation: the Hilbert space is nonzero and its
only closed invariant subspaces are zero and the whole space.

Theorem4.1.4

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.1.6

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Theorem 2.4. The infinite-dimensional unitary Schur lemma and its converse are proved. Continuous positive-part spectral cutoffs produce a nontrivial closed invariant subspace without introducing a Borel spectral-projection hypothesis.

Lean code for Theorem4.1.4●3 theorems

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.hasSchurProperty_of_isTopologicallyIrreducible.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) (hπ : π.IsTopologicallyIrreducible) :
  π.HasSchurProperty

theorem UnitaryRepresentation.hasSchurProperty_of_isTopologicallyIrreducible.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H)
  (hπ : π.IsTopologicallyIrreducible) :
  π.HasSchurProperty

The infinite-dimensional unitary form of **Schur's lemma**.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.isTopologicallyIrreducible_of_hasSchurProperty.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H]
  (π : UnitaryRepresentation G H) (hπ : π.HasSchurProperty) :
  π.IsTopologicallyIrreducible

theorem UnitaryRepresentation.isTopologicallyIrreducible_of_hasSchurProperty.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [Nontrivial H]
  (π : UnitaryRepresentation G H)
  (hπ : π.HasSchurProperty) :
  π.IsTopologicallyIrreducible

The converse to the unitary Schur lemma: if every bounded operator in the commutant is
scalar, then the representation is topologically irreducible.  Indeed, the orthogonal projection
onto an invariant closed subspace is scalar; if the subspace is nonzero, evaluating that scalar
projection on a nonzero vector in the subspace forces the scalar to be one.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.isTopologicallyIrreducible_iff_hasSchurProperty.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H]
  (π : UnitaryRepresentation G H) :
  π.IsTopologicallyIrreducible ↔ π.HasSchurProperty

theorem UnitaryRepresentation.isTopologicallyIrreducible_iff_hasSchurProperty.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [Nontrivial H]
  (π : UnitaryRepresentation G H) :
  π.IsTopologicallyIrreducible ↔
    π.HasSchurProperty

For a nonzero complex Hilbert space, topological irreducibility is equivalent to the scalar
commutant property.  This is the commutant formulation used by Mackey's imprimitivity argument.

Definition4.1.5

uses 1used by 1✓L∃∀N

Affine representations. Data and parameter Lebesgue measures have reciprocal determinant densities. Their square-root-corrected pullbacks give the two unitary L^2 representations. Deviation. The article's invariant-measure presentation is extended to the quasi-invariant affine measures actually used by the example.

Lean code for Definition4.1.5●4 definitions

defdefined in LeanRidgelet/HA/Affine.lean

complete

def LeanRidgelet.affineDataJacobian.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (g : E ≃ᵃ[ℝ] E) :
  E → NNReal

def LeanRidgelet.affineDataJacobian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (g : E ≃ᵃ[ℝ] E) : E → NNReal

Implementation after :=

:=
  fun _ ↦ ‖LinearMap.det (g.linear : E →ₗ[ℝ] E)‖₊

The constant Radon--Nikodym density for the inverse affine data action.

defdefined in LeanRidgelet/HA/Affine.lean

complete

def LeanRidgelet.affineParameterJacobian.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (g : E ≃ᵃ[ℝ] E) :
  E × ℝ → NNReal

def LeanRidgelet.affineParameterJacobian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (g : E ≃ᵃ[ℝ] E) : E × ℝ → NNReal

Implementation after :=

:=
  fun _ ↦ ‖LinearMap.det (g.linear : E →ₗ[ℝ] E)‖₊⁻¹

The constant Radon--Nikodym density for the inverse contragredient parameter action.

defdefined in LeanRidgelet/HA/Affine.lean

complete

def LeanRidgelet.affineDataLpUnitaryRepresentation.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  [MeasureTheory.SigmaFinite μ] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E) ↥(MeasureTheory.Lp Y 2 μ)

def LeanRidgelet.affineDataLpUnitaryRepresentation.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  [MeasureTheory.SigmaFinite μ] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E)
    ↥(MeasureTheory.Lp Y 2 μ)

Implementation after :=

:=
  quasiInvariantLpUnitaryRepresentation (E := Y) affineDataJacobian
    affineData_measurable (affineData_group_map_eq_withDensity μ)
    affineDataJacobian_measurable affineDataJacobian_ne_zero
    affineDataJacobian_one affineDataJacobian_cocycle

The Radon--Nikodym-corrected affine data representation on Bochner `L²`.

defdefined in LeanRidgelet/HA/Affine.lean

complete

def LeanRidgelet.affineParameterLpUnitaryRepresentation.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (ν : MeasureTheory.Measure (E × ℝ))
  [ν.IsAddHaarMeasure] [MeasureTheory.SigmaFinite ν] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E) ↥(MeasureTheory.Lp ℂ 2 ν)

def LeanRidgelet.affineParameterLpUnitaryRepresentation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (ν : MeasureTheory.Measure (E × ℝ))
  [ν.IsAddHaarMeasure]
  [MeasureTheory.SigmaFinite ν] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E)
    ↥(MeasureTheory.Lp ℂ 2 ν)

Implementation after :=

:=
  quasiInvariantLpUnitaryRepresentation affineParameterJacobian
    affineParameter_measurable (affineParameter_group_map_eq_withDensity ν)
    affineParameterJacobian_measurable affineParameterJacobian_ne_zero
    affineParameterJacobian_one affineParameterJacobian_cocycle

The Radon--Nikodym-corrected contragredient parameter representation on scalar `L²`.

Theorem4.1.6

Statement uses 4

Statement dependency previews

Preview

Theorem 4.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Lemma 4.1.20

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Theorem 2.5. The physical affine representation is related by invertible bounded intertwiners to its Fourier, conull-orbit, homogeneous-space, and normalized-section induced models. The inducing subgroup and its irreducible character, the quotient-orbit homeomorphism, the quasi-invariant measure, the explicit induced action, its translation-character restriction, the equality with a bundled Fourier-character multiplier, and the canonical indicator covariance are proved. Finite-character density for an arbitrary finite measure and the resulting general L^2 multiplier form of Theorem 4.44 are proved, upgrading the translation commutant to indicator spectral projections. The continuous-functional-calculus and self-adjoint decomposition part of Theorem 6.28 is also proved. For Lemma 6.29, compactly supported Haar probability kernels shrinking to the identity are constructed, and their smoothing stays in an invariant closed subspace and converges in L². Indicator stability is upgraded to compactly supported continuous multiplier stability; Urysohn cutoff and a diagonal argument then prove regular-section density from a continuous representative of each smoothed vector. Compact-kernel group-convolution continuity and the pointwise-representative theorem for L²-valued Bochner integrals are proved generally. The needed part of Lemma 6.30, identifying the extreme cases of a system-invariant closed subspace with those of the extracted inducing fiber, is proved from translated sections, transitivity, and a countable subcover of nonvanishing sets. The Lemma 6.29 measurable lift, the slice integrability of its smoothing integrand, and the identification of the resulting pointwise convolution with the Bochner-smoothed class are proved as well, so the chapter has no named sorry root. The one-dimensional fiber classification and the combination of the two lemmas are proved. Schur's converse derives induced irreducibility and the transports derive the article theorem. The group is the full GL(m) affine group: positive dilations alone would leave two frequency orbits in dimension one.

Lean code for Theorem4.1.6●19 declarations

theoremdefined in LeanRidgelet/HA/AffineMackeyInduction.lean

complete

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_indicator_covariant.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (g : AffineEquiv.TopologicalSemidirectProduct E)
  (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
  (hs : MeasurableSet s) :
  let t := (fun q ↦ g • q) ⁻¹' s;
  MeasureTheory.indicatorLp s hs ∘SL
      ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi)
          g) =
    ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi)
          g) ∘SL
      MeasureTheory.indicatorLp t ⋯

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_indicator_covariant.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (g :
    AffineEquiv.TopologicalSemidirectProduct
      E)
  (s :
    Set
      (LeanRidgelet.AffineTopologicalMackeyQuotient
        xi))
  (hs : MeasurableSet s) :
  let t := (fun q ↦ g • q) ⁻¹' s;
  MeasureTheory.indicatorLp s hs ∘SL
      ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi)
          g) =
    ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi)
          g) ∘SL
      MeasureTheory.indicatorLp t ⋯

The measurable-set multiplication projections on the homogeneous quotient form the canonical
system of imprimitivity for the normalized-section induced representation.  In operator form,
restricting the output to `s` and then acting by `g` is the same as first restricting to the
inverse translate of `s` and then acting by `g`.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_apply_ae.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0) (b : E)
  (f :
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
  ↑↑(↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
                (LeanRidgelet.affineTranslation b)))
          f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi]
    fun q ↦
    ↑((LeanRidgelet.affineTranslationCharacter
            ↑((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                  hxi)
                q))
          b) *
      ↑↑f q

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_apply_ae.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0) (b : E)
  (f :
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi))) :
  ↑↑(↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
                hxi)
              ((AffineEquiv.topologicalSemidirectProductEquiv
                    E).symm
                (LeanRidgelet.affineTranslation
                  b)))
          f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
      hxi]
    fun q ↦
    ↑((LeanRidgelet.affineTranslationCharacter
            ↑((LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit
                  hxi)
                q))
          b) *
      ↑↑f q

The restriction of the normalized-section induced representation to translations is the
pointwise translation-character representation on the frequency orbit.  In particular, both the
homogeneous-space motion and the Radon--Nikodym factor disappear; only the character at the
frequency represented by the coset remains.

defdefined in LeanRidgelet/HA/AffineMackey.lean

complete

def LeanRidgelet.affineTopologicalMackeyTranslationMultiplier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {xi : E}
  (hxi : xi ≠ 0) (b : E) :
  ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi)) ≃ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))

def LeanRidgelet.affineTopologicalMackeyTranslationMultiplier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0) (b : E) :
  ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi)) ≃ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi))

Implementation after :=

:=
  MeasureTheory.fourierCharacterLpMultiplier
    (μ := affineTopologicalMackeyQuotientMeasure hxi)
    (affineTopologicalMackeyFrequencyEmbedding hxi)
    (affineTopologicalMackeyFrequencyEmbedding_measurableEmbedding hxi).measurable b

Multiplication by the character through which a pure translation acts on the Mackey
quotient.  Bundling this operator separately makes the spectral-projection step independent of
the group-representation implementation: its only input is commutation with these concrete
Fourier-character multipliers.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_eq_multiplier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0) (b : E) :
  ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi)
        ((AffineEquiv.topologicalSemidirectProductEquiv E).symm
          (LeanRidgelet.affineTranslation b))) =
    ↑↑(LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi b)

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_eq_multiplier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0) (b : E) :
  ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi)
        ((AffineEquiv.topologicalSemidirectProductEquiv
              E).symm
          (LeanRidgelet.affineTranslation
            b))) =
    ↑↑(LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
          hxi b)

On the translation subgroup, the normalized-section induced representation is the concrete
Mackey character multiplier.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.ContinuousLinearMap.commutes_indicatorLp_of_commutes_fourierCharacter.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : MeasurableEmbedding j)
  (T : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ))
  (hchar :
    ∀ (b : V),
      T ∘SL ↑↑(MeasureTheory.fourierCharacterLpMultiplier j ⋯ b) =
        ↑↑(MeasureTheory.fourierCharacterLpMultiplier j ⋯ b) ∘SL T)
  (s : Set X) (hs : MeasurableSet s) :
  T ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs ∘SL T

theorem MeasureTheory.ContinuousLinearMap.commutes_indicatorLp_of_commutes_fourierCharacter.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : MeasurableEmbedding j)
  (T :
    ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (hchar :
    ∀ (b : V),
      T ∘SL
          ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j ⋯ b) =
        ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j ⋯ b) ∘SL
          T)
  (s : Set X) (hs : MeasurableSet s) :
  T ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs ∘SL T

A bounded operator commuting with every pulled-back Fourier-character multiplier commutes
with every measurable indicator projection.

This is the minimal `L²` multiplier consequence of the spectral-projection commutant criterion:
the measurable embedding ensures that the restricted characters generate the measurable
structure on `X`.  No general projection-valued-measure object is needed.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_commutes_indicator_of_commutes_translation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {xi : E}
  (hxi : xi ≠ 0)
  (T :
    ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (htranslation :
    ∀ (b : E),
      T ∘SL
          ↑↑(LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                hxi b) =
        ↑↑(LeanRidgelet.affineTopologicalMackeyTranslationMultiplier hxi
                b) ∘SL
          T)
  (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
  (hs : MeasurableSet s) :
  T ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs ∘SL T

theorem LeanRidgelet.affineMackey_commutes_indicator_of_commutes_translation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (T :
    ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (htranslation :
    ∀ (b : E),
      T ∘SL
          ↑↑(LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                hxi b) =
        ↑↑(LeanRidgelet.affineTopologicalMackeyTranslationMultiplier
                hxi b) ∘SL
          T)
  (s :
    Set
      (LeanRidgelet.AffineTopologicalMackeyQuotient
        xi))
  (hs : MeasurableSet s) :
  T ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs ∘SL T

Specialization of the commutant criterion in Folland Theorem 4.44 to the translation
restriction of the affine induced model.  Since translations act by the characters displayed in
`affineTopologicalMackeySectionInducedLpUnitaryRepresentation_translation_apply_ae`, their spectral
projections are the canonical measurable-set multiplication operators on the quotient orbit.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackeySmoothedVector_exists_continuousRepresentative.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (ψ :
    CompactlySupportedContinuousMap
      (AffineEquiv.TopologicalSemidirectProduct E) ℂ)
  (f :
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
  ∃ g,
    Continuous g ∧
      MeasureTheory.MemLp g 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi) ∧
        ↑↑(LeanRidgelet.affineMackeySmoothedVector hxi ψ
                f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi]
          g

theorem LeanRidgelet.affineMackeySmoothedVector_exists_continuousRepresentative.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (ψ :
    CompactlySupportedContinuousMap
      (AffineEquiv.TopologicalSemidirectProduct
        E)
      ℂ)
  (f :
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
          hxi))) :
  ∃ g,
    Continuous g ∧
      MeasureTheory.MemLp g 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi) ∧
        ↑↑(LeanRidgelet.affineMackeySmoothedVector
                hxi ψ
                f) =ᵐ[LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi]
          g

Haar smoothing of the normalized-section induced model has a continuous representative on the
homogeneous quotient.  A measurable representative of the quotient class lifts to the group so that
the smoothing integral becomes a compact-kernel group convolution: the convolution is continuous by
`LeanRidgelet.continuous_affineMackeySmoothingIntegral`, its slices over the finite-measure parts
of the quotient are integrable by
`LeanRidgelet.integrable_uncurry_affineMackeySmoothingIntegrand`, and
`MeasureTheory.integral_L2_coeFn_ae_of_restrict` therefore identifies the `L²`-valued Bochner
integral defining the smoothed vector with that pointwise integral.  The subsequent compact cutoff
and density argument is proved below.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_regularSection_dense.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
  (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀ (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection) :
  Dense
    (Set.range fun f ↦
      ⟨(LeanRidgelet.affineMackeyRegularSectionToLp hxi) ↑f, ⋯⟩)

theorem LeanRidgelet.affineMackey_regularSection_dense.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL
          MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL
          (↑K).starProjection) :
  Dense
    (Set.range fun f ↦
      ⟨(LeanRidgelet.affineMackeyRegularSectionToLp
            hxi)
          ↑f,
        ⋯⟩)

Folland Lemma 6.29 in the normalized quotient model: regular sections belonging to a closed
subspace invariant under the system of imprimitivity are dense in that subspace.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackeyRegularSectionToLp_smul.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [Nontrivial E] [MeasurableSpace E] [BorelSpace E] {xi : E}
  (hxi : xi ≠ 0) (g : AffineEquiv.TopologicalSemidirectProduct E)
  (r :
    CompactlySupportedContinuousMap
      (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ℂ) :
  (LeanRidgelet.affineMackeyRegularSectionToLp hxi)
      (LeanRidgelet.affineMackeyRegularSectionSMul hxi g r) =
    ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi)
          g)
      ((LeanRidgelet.affineMackeyRegularSectionToLp hxi) r)

theorem LeanRidgelet.affineMackeyRegularSectionToLp_smul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (g :
    AffineEquiv.TopologicalSemidirectProduct
      E)
  (r :
    CompactlySupportedContinuousMap
      (LeanRidgelet.AffineTopologicalMackeyQuotient
        xi)
      ℂ) :
  (LeanRidgelet.affineMackeyRegularSectionToLp
        hxi)
      (LeanRidgelet.affineMackeyRegularSectionSMul
        hxi g r) =
    ↑((LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
            hxi)
          g)
      ((LeanRidgelet.affineMackeyRegularSectionToLp
          hxi)
        r)

The `L²` class of a translated section is the induced action applied to the `L²` class of the
section.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackeyInducingFiber_eq_bot_iff.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))) :
  LeanRidgelet.affineMackeyInducingFiber hxi K = ⊥ ↔
    ∀
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ℂ),
      (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r ∈ K → r ↑1 = 0

theorem LeanRidgelet.affineMackeyInducingFiber_eq_bot_iff.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi))) :
  LeanRidgelet.affineMackeyInducingFiber
        hxi K =
      ⊥ ↔
    ∀
      (r :
        CompactlySupportedContinuousMap
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi)
          ℂ),
      (LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            r ∈
          K →
        r ↑1 = 0

The inducing fiber is trivial exactly when every regular section of the subspace vanishes at
the identity coset.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackeyInducingFiber_eq_top_of_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {xi : E}
  (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (r :
    CompactlySupportedContinuousMap
      (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ℂ)
  (hr : (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r ∈ K)
  (hr0 : r ↑1 ≠ 0) : LeanRidgelet.affineMackeyInducingFiber hxi K = ⊤

theorem LeanRidgelet.affineMackeyInducingFiber_eq_top_of_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (r :
    CompactlySupportedContinuousMap
      (LeanRidgelet.AffineTopologicalMackeyQuotient
        xi)
      ℂ)
  (hr :
    (LeanRidgelet.affineMackeyRegularSectionToLp
          hxi)
        r ∈
      K)
  (hr0 : r ↑1 ≠ 0) :
  LeanRidgelet.affineMackeyInducingFiber
      hxi K =
    ⊤

One regular section of the subspace that does not vanish at the identity coset already spans
the whole one-dimensional inducing fiber.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_eq_bot_of_inducingFiber_eq_bot.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hregular :
    Dense
      (Set.range fun f ↦
        ⟨(LeanRidgelet.affineMackeyRegularSectionToLp hxi) ↑f, ⋯⟩))
  (hfiber : LeanRidgelet.affineMackeyInducingFiber hxi K = ⊥) : K = ⊥

theorem LeanRidgelet.affineMackey_eq_bot_of_inducingFiber_eq_bot.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hregular :
    Dense
      (Set.range fun f ↦
        ⟨(LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            ↑f,
          ⋯⟩))
  (hfiber :
    LeanRidgelet.affineMackeyInducingFiber
        hxi K =
      ⊥) :
  K = ⊥

A subspace with trivial inducing fiber is trivial.  Every regular section it contains vanishes
identically, and regular sections are dense in it by the Folland-6.29 density theorem.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_eq_top_of_regularSection_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀ (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection)
  (r :
    CompactlySupportedContinuousMap
      (LeanRidgelet.AffineTopologicalMackeyQuotient xi) ℂ)
  (hr : (LeanRidgelet.affineMackeyRegularSectionToLp hxi) r ∈ K)
  (hr0 : r ↑1 ≠ 0) : K = ⊤

theorem LeanRidgelet.affineMackey_eq_top_of_regularSection_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL
          MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL
          (↑K).starProjection)
  (r :
    CompactlySupportedContinuousMap
      (LeanRidgelet.AffineTopologicalMackeyQuotient
        xi)
      ℂ)
  (hr :
    (LeanRidgelet.affineMackeyRegularSectionToLp
          hxi)
        r ∈
      K)
  (hr0 : r ↑1 ≠ 0) : K = ⊤

A subspace containing one regular section that does not vanish at the identity coset is
everything.  Orthogonality to the subspace forces a vector to vanish almost everywhere on the
nonvanishing set of every translate of that section, and countably many translates already cover the
homogeneous quotient.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_closedSubspace_extreme_iff_inducingFiber_extreme.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀ (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection)
  (hregular :
    Dense
      (Set.range fun f ↦
        ⟨(LeanRidgelet.affineMackeyRegularSectionToLp hxi) ↑f, ⋯⟩)) :
  (K = ⊥ ↔ LeanRidgelet.affineMackeyInducingFiber hxi K = ⊥) ∧
    (K = ⊤ ↔ LeanRidgelet.affineMackeyInducingFiber hxi K = ⊤)

theorem LeanRidgelet.affineMackey_closedSubspace_extreme_iff_inducingFiber_extreme.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL
          MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL
          (↑K).starProjection)
  (hregular :
    Dense
      (Set.range fun f ↦
        ⟨(LeanRidgelet.affineMackeyRegularSectionToLp
              hxi)
            ↑f,
          ⋯⟩)) :
  (K = ⊥ ↔
      LeanRidgelet.affineMackeyInducingFiber
          hxi K =
        ⊥) ∧
    (K = ⊤ ↔
      LeanRidgelet.affineMackeyInducingFiber
          hxi K =
        ⊤)

Folland Lemma 6.30, restricted to the two conclusions needed for the one-dimensional affine
inducing fiber.  The regular-section fiber is zero exactly when the induced closed subspace is
zero, and it is the whole scalar fiber exactly when that subspace is the whole `L²` space.

Both directions are assembled from the four lemmas above: identity-coset evaluation of translated
sections for the zero case, together with the density hypothesis supplied by Folland 6.29, and
orthogonal-complement vanishing along a countable subcover of translates for the full case.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_systemInvariant_closedSubspace_eq_bot_or_top.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀ (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection) :
  K = ⊥ ∨ K = ⊤

theorem LeanRidgelet.affineMackey_systemInvariant_closedSubspace_eq_bot_or_top.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (hrepresentation :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      (↑K).starProjection)
  (hindicator :
    ∀
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s),
      (↑K).starProjection ∘SL
          MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL
          (↑K).starProjection) :
  K = ⊥ ∨ K = ⊤

Folland Lemmas 6.29--6.30 for the canonical affine system with one-dimensional inducing
fiber. A closed subspace whose orthogonal projection commutes with both the induced action and all
quotient-orbit indicator projections is zero or the whole `L²` space.

The regular-section density theorem above is a completed consequence of the named
measurable-lift/product-integrability/convolution-formula placeholder, and the inducing-fiber
correspondence is now proved. This theorem combines them with the proved classification of closed
complex subspaces of the one-dimensional inducing fiber and contains no `sorry` of its own.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineMackey_scalar_of_commutes_indicators.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0)
  (T :
    ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi)))
  (hT :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      T)
  (hindicator :
    ∀ (s : Set (LeanRidgelet.AffineTopologicalMackeyQuotient xi))
      (hs : MeasurableSet s),
      T ∘SL MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL T) :
  ∃ c,
    T =
      c •
        ContinuousLinearMap.id ℂ
          ↥(MeasureTheory.Lp ℂ 2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure hxi))

theorem LeanRidgelet.affineMackey_scalar_of_commutes_indicators.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0)
  (T :
    ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
            hxi)))
  (hT :
    (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
          hxi).Commutes
      T)
  (hindicator :
    ∀
      (s :
        Set
          (LeanRidgelet.AffineTopologicalMackeyQuotient
            xi))
      (hs : MeasurableSet s),
      T ∘SL
          MeasureTheory.indicatorLp s hs =
        MeasureTheory.indicatorLp s hs ∘SL
          T) :
  ∃ c,
    T =
      c •
        ContinuousLinearMap.id ℂ
          ↥(MeasureTheory.Lp ℂ 2
              (LeanRidgelet.affineTopologicalMackeyQuotientMeasure
                hxi))

Specialization of Folland Theorem 6.28 to the canonical affine system of imprimitivity.
Commutation with the induced action and all quotient-orbit indicator projections identifies `T`
with an operator in the commutant of the one-dimensional inducing character, hence with a scalar.

The only unproved input is the Folland-6.29 smoothed-vector continuous-representative theorem
used by the completed regular-section density argument. The spectral-subspace argument, the
inducing-fiber correspondence, and the decomposition into two self-adjoint operators are proved
here.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_hasSchurProperty.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0) :
  (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
      hxi).HasSchurProperty

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_hasSchurProperty.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0) :
  (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
      hxi).HasSchurProperty

The assembled commutant form of the Mackey irreducibility step for the normalized-section
induced model. An operator commuting with the induced affine action first commutes with the
spectral projections of the translation subgroup, hence belongs to the commutant of the canonical
system of imprimitivity; the imprimitivity commutant theorem then identifies it with the commutant
of the inducing one-dimensional character, so it is scalar.

All group, orbit, quotient-measure, section-cocycle, continuity, inducing-character,
translation-spectral, and inducing-fiber inputs have already been constructed above. The remaining
analytic input is the named Folland-6.29 smoothed-vector continuous-representative theorem used by
the completed density argument; this assembly contains no source-level placeholder and uses no
induction or imprimitivity assumptions structure.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {xi : E} (hxi : xi ≠ 0) :
  (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
      hxi).IsTopologicallyIrreducible

theorem LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {xi : E} (hxi : xi ≠ 0) :
  (LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation
      hxi).IsTopologicallyIrreducible

Folland Theorem 6.39, irreducibility direction, for the normalized-section affine induced
model.  Once its commutant is scalar, the converse direction of the unitary Schur lemma turns the
commutant statement into topological irreducibility.

theoremdefined in LeanRidgelet/HA/AffineMackey.lean

complete

theorem LeanRidgelet.affineDataLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] :
  (LeanRidgelet.affineDataLpUnitaryRepresentation
      MeasureTheory.volume).IsTopologicallyIrreducible

theorem LeanRidgelet.affineDataLpUnitaryRepresentation_isTopologicallyIrreducible.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E] :
  (LeanRidgelet.affineDataLpUnitaryRepresentation
      MeasureTheory.volume).IsTopologicallyIrreducible

Theorem 2.5 of arXiv:2405.13682: the scalar quasi-regular representation of the full affine
group is topologically irreducible.

The Fourier-conjugated representation has now been transported first to the intrinsic `L²` space
on the conull nonzero-frequency subtype and then, through
`affineTopologicalMackeyQuotientHomeomorphDualOrbit`, to the actual homogeneous-space
`L²(G/H)`. Both transports have explicit inverse bounded intertwiners, and the homeomorphism is
proved equivariant for left translation and the dual action. The closed locally compact inducing
subgroup and its strongly continuous irreducible character representation are
`affineTopologicalMackeySubgroup` and `affineTopologicalMackeyUnitaryRepresentation`, with the
required translation and little-group restriction formulas.

The normalized equivariant-section realization of unitary induction is now constructed explicitly:
its reentry cocycle is `s(q)⁻¹ g s(g⁻¹q)`, its character phase is proved equal to the Fourier
phase, and the resulting unitary representation is proved equal to the transported homogeneous
model. The paper endpoint is derived from the commutant form of Folland Theorem 6.39 above. Its
translation-spectral, spectral-subspace, compact-kernel convolution continuity, compact-cutoff,
regular-section density, and 6.30 inducing-fiber inputs are complete, while its Folland-6.29
measurable lift with product integrability and convolution formula is the one remaining HA
placeholder. Mathlib's algebraic
`Representation.ind` is not the quasi-invariant Hilbert-space construction and Mathlib has no
imprimitivity theorem.

Section 3: joint equivariance and the reconstruction theorem

Definition4.1.7

uses 1

Used by 3

Reverse dependency previews

Preview

Definition 4.1.12

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Definition 3.1. Invariant and strongly quasi-invariant pullbacks are bundled on Bochner L^2; the latter use the square-root Radon--Nikodym correction. A measurable unimodular cocycle supplies the character-twisted form used by the affine induced model.

Lean code for Definition4.1.7●3 definitions

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.invariantLpUnitaryRepresentation.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SMulInvariantMeasure G X μ] [MeasurableConstSMul G X] :
  UnitaryRepresentation G ↥(MeasureTheory.Lp E 2 μ)

def LeanRidgelet.invariantLpUnitaryRepresentation.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SMulInvariantMeasure G X
      μ]
  [MeasurableConstSMul G X] :
  UnitaryRepresentation G
    ↥(MeasureTheory.Lp E 2 μ)

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    { toFun := fun g ↦ invariantLpLinearIsometryEquiv (toDomMulActInv g)
      map_one' := by
        apply LinearIsometryEquiv.ext
        intro f
        simp [toDomMulActInv]
      map_mul' := by
        intro g h
        apply LinearIsometryEquiv.ext
        intro f
        simp [toDomMulActInv, mul_smul] }

An invariant measurable action induces a unitary representation on Bochner `L²`.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.quasiInvariantLpUnitaryRepresentation.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero : ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (h_one : ∀ (x : X), jacobian 1 x = 1)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x = jacobian g (h • x) * jacobian h x) :
  UnitaryRepresentation G ↥(MeasureTheory.Lp E 2 μ)

def LeanRidgelet.quasiInvariantLpUnitaryRepresentation.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero :
    ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (h_one : ∀ (x : X), jacobian 1 x = 1)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x =
        jacobian g (h • x) *
          jacobian h x) :
  UnitaryRepresentation G
    ↥(MeasureTheory.Lp E 2 μ)

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    (quasiInvariantLpLinearIsometryEquivMonoidHom jacobian h_measurable h_map h_jacobian
      h_ne_zero h_one h_cocycle)

A strongly quasi-invariant measure with a measurable positive Radon--Nikodym cocycle induces
Folland's unitary representation on Bochner `L²`.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.twistedQuasiInvariantLpUnitaryRepresentation.{u_1, u_2}
  {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X]
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero : ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (h_one : ∀ (x : X), jacobian 1 x = 1)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x = jacobian g (h • x) * jacobian h x)
  (phase : G → X → ℂ)
  (h_phase_measurable :
    ∀ (g : G), MeasureTheory.AEStronglyMeasurable (phase g) μ)
  (h_phase_norm : ∀ (g : G), ∀ᵐ (x : X) ∂μ, ‖phase g x‖ = 1)
  (h_phase_one : ∀ (x : X), phase 1 x = 1)
  (h_phase_cocycle :
    ∀ (g h : G) (x : X),
      phase (g * h) x = phase g x * phase h (g⁻¹ • x)) :
  UnitaryRepresentation G ↥(MeasureTheory.Lp ℂ 2 μ)

def LeanRidgelet.twistedQuasiInvariantLpUnitaryRepresentation.{u_1,
    u_2}
  {G : Type u_1} {X : Type u_2} [Group G]
  [MulAction G X] [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero :
    ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (h_one : ∀ (x : X), jacobian 1 x = 1)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x =
        jacobian g (h • x) * jacobian h x)
  (phase : G → X → ℂ)
  (h_phase_measurable :
    ∀ (g : G),
      MeasureTheory.AEStronglyMeasurable
        (phase g) μ)
  (h_phase_norm :
    ∀ (g : G),
      ∀ᵐ (x : X) ∂μ, ‖phase g x‖ = 1)
  (h_phase_one : ∀ (x : X), phase 1 x = 1)
  (h_phase_cocycle :
    ∀ (g h : G) (x : X),
      phase (g * h) x =
        phase g x * phase h (g⁻¹ • x)) :
  UnitaryRepresentation G
    ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    (twistedQuasiInvariantLpLinearIsometryEquivMonoidHom jacobian h_measurable h_map
      h_jacobian h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm
      h_phase_one h_phase_cocycle)

A strongly quasi-invariant measure together with a measurable unimodular multiplier cocycle
gives the character-twisted quasi-regular unitary representation on scalar `L²`.

Definition4.1.8

uses 0

Used by 6

Reverse dependency previews

Preview

Lemma 4.1.9

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Definition 3.2. A feature \phi:X\times\Xi\to Y is joint-G-equivariant when the simultaneous action on input and parameter agrees with the output action.

Lean code for Definition4.1.8●1 definition

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

def LeanRidgelet.IsJointEquivariant.{u_1, u_2, u_3, u_4} {G : Type u_1}
  {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [SMul G X] [SMul G Ξ]
  [SMul G Y] (φ : X → Ξ → Y) : Prop

def LeanRidgelet.IsJointEquivariant.{u_1, u_2,
    u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [SMul G X]
  [SMul G Ξ] [SMul G Y] (φ : X → Ξ → Y) :
  Prop

Implementation after :=

:=
  ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = g • φ x ξ

A feature map is joint-`G`-equivariant when simultaneous actions on its data and parameter
arguments agree with the action on its output. This is Definition 3.2.

Lemma4.1.9

uses 1used by 0✓L∃∀N

Remark 3.3. Ordinary equivariance is the special case of a fixed parameter.

Lean code for Lemma4.1.9●2 declarations

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

def LeanRidgelet.IsEquivariant.{u_1, u_2, u_4} {G : Type u_1} {X : Type u_2}
  {Y : Type u_4} [SMul G X] [SMul G Y] (φ : X → Y) : Prop

def LeanRidgelet.IsEquivariant.{u_1, u_2, u_4}
  {G : Type u_1} {X : Type u_2}
  {Y : Type u_4} [SMul G X] [SMul G Y]
  (φ : X → Y) : Prop

Implementation after :=

:=
  ∀ (g : G) (x : X), φ (g • x) = g • φ x

Ordinary equivariance of a map between two `G`-spaces.

theoremdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

theorem LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed.{u_1, u_2, u_3,
    u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [SMul G X]
  [SMul G Ξ] [SMul G Y] {φ : X → Ξ → Y}
  (hφ : ∀ (ξ : Ξ), LeanRidgelet.IsEquivariant fun x ↦ φ x ξ)
  (hfixed : ∀ (g : G) (ξ : Ξ), g • ξ = ξ) :
  LeanRidgelet.IsJointEquivariant φ

theorem LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [SMul G X]
  [SMul G Ξ] [SMul G Y] {φ : X → Ξ → Y}
  (hφ :
    ∀ (ξ : Ξ),
      LeanRidgelet.IsEquivariant fun x ↦
        φ x ξ)
  (hfixed :
    ∀ (g : G) (ξ : Ξ), g • ξ = ξ) :
  LeanRidgelet.IsJointEquivariant φ

Remark 3.3: ordinary equivariance is joint equivariance when the parameter action is trivial.

Lemma4.1.10

uses 1used by 0✓L∃∀N

Lemma 3.4. An arbitrary seed produces a joint-equivariant orbit feature.

Lean code for Lemma4.1.10●2 declarations

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

def LeanRidgelet.orbitFeature.{u_1, u_2, u_4} {G : Type u_1} {X : Type u_2}
  {Y : Type u_4} [Group G] [MulAction G X] [MulAction G Y] (φ₀ : X → Y)
  (x : X) (h : G) : Y

def LeanRidgelet.orbitFeature.{u_1, u_2, u_4}
  {G : Type u_1} {X : Type u_2}
  {Y : Type u_4} [Group G] [MulAction G X]
  [MulAction G Y] (φ₀ : X → Y) (x : X)
  (h : G) : Y

Implementation after :=

:=
  h • φ₀ (h⁻¹ • x)

The orbit feature generated from an arbitrary seed map, as in Lemma 3.4.

theoremdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

theorem LeanRidgelet.isJointEquivariant_orbitFeature.{u_1, u_2, u_4}
  {G : Type u_1} {X : Type u_2} {Y : Type u_4} [Group G] [MulAction G X]
  [MulAction G Y] (φ₀ : X → Y) :
  LeanRidgelet.IsJointEquivariant (LeanRidgelet.orbitFeature φ₀)

theorem LeanRidgelet.isJointEquivariant_orbitFeature.{u_1,
    u_2, u_4}
  {G : Type u_1} {X : Type u_2}
  {Y : Type u_4} [Group G] [MulAction G X]
  [MulAction G Y] (φ₀ : X → Y) :
  LeanRidgelet.IsJointEquivariant
    (LeanRidgelet.orbitFeature φ₀)

Lemma 3.4: the orbit feature of any seed map is joint-equivariant.

Lemma4.1.11

uses 1

Used by 2

Reverse dependency previews

Preview

Corollary 4.1.18

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Lemma 3.5. Binary cascade preserves joint equivariance, and a dependent finite tuple extends the calculation to heterogeneous depth.

Lean code for Lemma4.1.11●5 declarations

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

def LeanRidgelet.jointCascade.{u_2, u_3, u_4, u_5, u_6} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} {Ω : Type u_5} {Z : Type u_6}
  (φ : X → Ξ → Y) (ψ : Y → Ω → Z) (x : X) (p : Ξ × Ω) : Z

def LeanRidgelet.jointCascade.{u_2, u_3, u_4,
    u_5, u_6}
  {X : Type u_2} {Ξ : Type u_3}
  {Y : Type u_4} {Ω : Type u_5}
  {Z : Type u_6} (φ : X → Ξ → Y)
  (ψ : Y → Ω → Z) (x : X) (p : Ξ × Ω) : Z

Implementation after :=

:=
  ψ (φ x p.1) p.2

Cascade composition of two parametrized feature maps.

theoremdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

theorem LeanRidgelet.IsJointEquivariant.jointCascade.{u_1, u_2, u_3, u_4, u_5,
    u_6}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4}
  {Ω : Type u_5} {Z : Type u_6} [Monoid G] [MulAction G X]
  [MulAction G Ξ] [MulAction G Y] [MulAction G Ω] [MulAction G Z]
  {φ : X → Ξ → Y} {ψ : Y → Ω → Z}
  (hφ : LeanRidgelet.IsJointEquivariant φ)
  (hψ : LeanRidgelet.IsJointEquivariant ψ) :
  LeanRidgelet.IsJointEquivariant (LeanRidgelet.jointCascade φ ψ)

theorem LeanRidgelet.IsJointEquivariant.jointCascade.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4}
  {Ω : Type u_5} {Z : Type u_6} [Monoid G]
  [MulAction G X] [MulAction G Ξ]
  [MulAction G Y] [MulAction G Ω]
  [MulAction G Z] {φ : X → Ξ → Y}
  {ψ : Y → Ω → Z}
  (hφ : LeanRidgelet.IsJointEquivariant φ)
  (hψ :
    LeanRidgelet.IsJointEquivariant ψ) :
  LeanRidgelet.IsJointEquivariant
    (LeanRidgelet.jointCascade φ ψ)

The binary form of Lemma 3.5: a cascade of joint-equivariant layers is joint-equivariant.

inductive(2 constructors, 2 parameters)defined in LeanRidgelet/HA/Deep.lean

complete

inductive LeanRidgelet.DeepParameters.{u_2} (Ξ : ℕ → Type u_2) : ℕ → Type u_2

inductive LeanRidgelet.DeepParameters.{u_2}
  (Ξ : ℕ → Type u_2) : ℕ → Type u_2

A finite heterogeneous parameter tuple, built by appending the parameter of each layer.

Constructors

LeanRidgelet.DeepParameters.nil.{u_2} {Ξ : ℕ → Type u_2} :
  LeanRidgelet.DeepParameters Ξ 0

The empty parameter tuple.

LeanRidgelet.DeepParameters.snoc.{u_2} {Ξ : ℕ → Type u_2}
  {n : ℕ} :
  LeanRidgelet.DeepParameters Ξ n →
    Ξ n → LeanRidgelet.DeepParameters Ξ (n + 1)

Append the parameter of layer `n` to a tuple for the preceding layers.

defdefined in LeanRidgelet/HA/Deep.lean

complete

def LeanRidgelet.deepFeature.{u_2, u_3} {X : ℕ → Type u_2}
  {Ξ : ℕ → Type u_3} (φ : (i : ℕ) → X i → Ξ i → X (i + 1)) (n : ℕ) :
  X 0 → LeanRidgelet.DeepParameters Ξ n → X n

def LeanRidgelet.deepFeature.{u_2, u_3}
  {X : ℕ → Type u_2} {Ξ : ℕ → Type u_3}
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (n : ℕ) :
  X 0 →
    LeanRidgelet.DeepParameters Ξ n → X n

Composition of a finite heterogeneous family of parametrized layers.

theoremdefined in LeanRidgelet/HA/Deep.lean

complete

theorem LeanRidgelet.isJointEquivariant_deepFeature.{u_1, u_2, u_3}
  {G : Type u_1} {X : ℕ → Type u_2} {Ξ : ℕ → Type u_3} [Monoid G]
  [(i : ℕ) → MulAction G (X i)] [(i : ℕ) → MulAction G (Ξ i)]
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (hφ : ∀ (i : ℕ), LeanRidgelet.IsJointEquivariant (φ i)) (n : ℕ) :
  LeanRidgelet.IsJointEquivariant (LeanRidgelet.deepFeature φ n)

theorem LeanRidgelet.isJointEquivariant_deepFeature.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : ℕ → Type u_2}
  {Ξ : ℕ → Type u_3} [Monoid G]
  [(i : ℕ) → MulAction G (X i)]
  [(i : ℕ) → MulAction G (Ξ i)]
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (hφ :
    ∀ (i : ℕ),
      LeanRidgelet.IsJointEquivariant
        (φ i))
  (n : ℕ) :
  LeanRidgelet.IsJointEquivariant
    (LeanRidgelet.deepFeature φ n)

Lemma 3.5 in heterogeneous finite-depth form.

Definition4.1.12

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Lemma 4.1.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Definition 3.6. A bounded machine is a continuous intertwining map from the parameter representation to the data representation.

Lean code for Definition4.1.12●1 definition

abbrevdefined in LeanRidgelet/HA/Operators.lean

complete

abbrev LeanRidgelet.JointEquivariantMachine.{u_1, u_2, u_3} {G : Type u_1}
  {H : Type u_2} {K : Type u_3} [Monoid G] [NormedAddCommGroup H]
  [NormedSpace ℂ H] [NormedAddCommGroup K] [NormedSpace ℂ K]
  (πParameter : ContRepresentation ℂ G K)
  (πData : ContRepresentation ℂ G H) : Type (max u_3 u_2)

abbrev LeanRidgelet.JointEquivariantMachine.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Monoid G]
  [NormedAddCommGroup H] [NormedSpace ℂ H]
  [NormedAddCommGroup K] [NormedSpace ℂ K]
  (πParameter : ContRepresentation ℂ G K)
  (πData : ContRepresentation ℂ G H) :
  Type (max u_3 u_2)

Implementation after :=

:=
  πParameter →ⁱL πData

A bounded joint-equivariant machine from parameter space to data space.

Lemma4.1.13

uses 1used by 1✓L∃∀N

Lemma 3.7. Bochner change of variables and joint equivariance make synthesis an intertwiner. The quasi-invariant form records the reciprocal Jacobian balance required by affine actions.

Lean code for Lemma4.1.13●4 declarations

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.bochnerSynthesis_intertwines.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ) (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_preserving :
    ∀ (g : G), MeasureTheory.MeasurePreserving (fun ξ ↦ g • ξ) μ μ)
  (h_embedding : ∀ (g : G), MeasurableEmbedding fun ξ ↦ g • ξ) (g : G)
  (γ : Ξ → ℂ) (x : X) :
  LeanRidgelet.bochnerSynthesis μ φ
      (LeanRidgelet.scalarPullbackAction g γ) x =
    LeanRidgelet.unitaryPullbackAction υ g
      (LeanRidgelet.bochnerSynthesis μ φ γ) x

theorem LeanRidgelet.bochnerSynthesis_intertwines.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_preserving :
    ∀ (g : G),
      MeasureTheory.MeasurePreserving
        (fun ξ ↦ g • ξ) μ μ)
  (h_embedding :
    ∀ (g : G),
      MeasurableEmbedding fun ξ ↦ g • ξ)
  (g : G) (γ : Ξ → ℂ) (x : X) :
  LeanRidgelet.bochnerSynthesis μ φ
      (LeanRidgelet.scalarPullbackAction g
        γ)
      x =
    LeanRidgelet.unitaryPullbackAction υ g
      (LeanRidgelet.bochnerSynthesis μ φ
        γ)
      x

Joint equivariance plus an invariant parameter measure makes the Bochner synthesis integral
intertwine the scalar pullback and the unitary data action.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.bochnerSynthesis_quasi_intertwines.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ) (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_parameter_measurable : ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun ξ ↦ g⁻¹ • ξ) μ =
        μ.withDensity fun ξ ↦ ↑(parameterJacobian g ξ))
  (h_parameter_jacobian : ∀ (g : G), Measurable (parameterJacobian g))
  (h_parameter_ne_zero : ∀ (g : G) (ξ : Ξ), parameterJacobian g ξ ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (parameterJacobian g ξ)) =
        LeanRidgelet.radonNikodymWeight dataJacobian g x)
  (g : G) (γ : Ξ → ℂ) (x : X) :
  LeanRidgelet.bochnerSynthesis μ φ
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight parameterJacobian) g γ)
      x =
    LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g
      (LeanRidgelet.bochnerSynthesis μ φ γ) x

theorem LeanRidgelet.bochnerSynthesis_quasi_intertwines.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_parameter_measurable :
    ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun ξ ↦ g⁻¹ • ξ) μ =
        μ.withDensity fun ξ ↦
          ↑(parameterJacobian g ξ))
  (h_parameter_jacobian :
    ∀ (g : G),
      Measurable (parameterJacobian g))
  (h_parameter_ne_zero :
    ∀ (g : G) (ξ : Ξ),
      parameterJacobian g ξ ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt
              (parameterJacobian g ξ)) =
        LeanRidgelet.radonNikodymWeight
          dataJacobian g x)
  (g : G) (γ : Ξ → ℂ) (x : X) :
  LeanRidgelet.bochnerSynthesis μ φ
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          parameterJacobian)
        g γ)
      x =
    LeanRidgelet.quasiUnitaryPullbackAction
      dataJacobian υ g
      (LeanRidgelet.bochnerSynthesis μ φ
        γ)
      x

Joint equivariance intertwines quasi-invariant Bochner synthesis actions when the parameter
Jacobian's square root equals the data-side Radon--Nikodym multiplier. This is the explicit
Jacobian cancellation missing from the invariant-measure statement.

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerSynthesisIntertwiningMap.{u_1, u_2, u_3, u_4, u_5,
    u_6}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  {K : Type u_5} {H : Type u_6} [NormedAddCommGroup K] [NormedSpace ℂ K]
  [NormedAddCommGroup H] [NormedSpace ℂ H] (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (πParameter : ContRepresentation ℂ G K)
  (πData : ContRepresentation ℂ G H) (coefficient : K → Ξ → ℂ)
  (value : H → X → Y) (h_value : Function.Injective value)
  (M : K →L[ℂ] H) (φ : X → Ξ → Y)
  (hM :
    ∀ (k : K),
      value (M k) = LeanRidgelet.bochnerSynthesis μ φ (coefficient k))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.scalarPullbackAction g (coefficient k))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.unitaryPullbackAction υ g (value f))
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_preserving :
    ∀ (g : G), MeasureTheory.MeasurePreserving (fun ξ ↦ g • ξ) μ μ)
  (h_embedding : ∀ (g : G), MeasurableEmbedding fun ξ ↦ g • ξ) :
  LeanRidgelet.JointEquivariantMachine πParameter πData

def LeanRidgelet.bochnerSynthesisIntertwiningMap.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {K : Type u_5}
  {H : Type u_6} [NormedAddCommGroup K]
  [NormedSpace ℂ K] [NormedAddCommGroup H]
  [NormedSpace ℂ H]
  (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (πParameter : ContRepresentation ℂ G K)
  (πData : ContRepresentation ℂ G H)
  (coefficient : K → Ξ → ℂ)
  (value : H → X → Y)
  (h_value : Function.Injective value)
  (M : K →L[ℂ] H) (φ : X → Ξ → Y)
  (hM :
    ∀ (k : K),
      value (M k) =
        LeanRidgelet.bochnerSynthesis μ φ
          (coefficient k))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.scalarPullbackAction
          g (coefficient k))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.unitaryPullbackAction
          υ g (value f))
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_preserving :
    ∀ (g : G),
      MeasureTheory.MeasurePreserving
        (fun ξ ↦ g • ξ) μ μ)
  (h_embedding :
    ∀ (g : G),
      MeasurableEmbedding fun ξ ↦ g • ξ) :
  LeanRidgelet.JointEquivariantMachine
    πParameter πData

Implementation after :=

:= M
  isIntertwining' g := by
    ext k
    apply h_value
    calc
      value (M (πParameter g k)) =
          bochnerSynthesis μ φ (coefficient (πParameter g k)) := hM _
      _ = bochnerSynthesis μ φ (scalarPullbackAction g (coefficient k)) := by
        rw [h_parameter]
      _ = unitaryPullbackAction υ g (bochnerSynthesis μ φ (coefficient k)) :=
        funext fun x ↦ bochnerSynthesis_intertwines μ υ φ h_joint h_preserving h_embedding g _ x
      _ = unitaryPullbackAction υ g (value (M k)) := by rw [hM]
      _ = value (πData g (M k)) := (h_data _ _).symm

Bundle a bounded Bochner synthesis map as a continuous intertwiner once its coordinate
formula and the coordinate formulas for the two representations are known. This is the formal
bridge from the integral identity above to the operator-level `JointEquivariantMachine` API.

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerSynthesisQuasiIntertwiningMap.{u_1, u_2, u_3, u_4,
    u_5, u_6}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  {K : Type u_5} {H : Type u_6} [NormedAddCommGroup K] [NormedSpace ℂ K]
  [NormedAddCommGroup H] [NormedSpace ℂ H] (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (πParameter : ContRepresentation ℂ G K)
  (πData : ContRepresentation ℂ G H) (coefficient : K → Ξ → ℂ)
  (value : H → X → Y) (h_value : Function.Injective value)
  (M : K →L[ℂ] H) (φ : X → Ξ → Y) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (hM :
    ∀ (k : K),
      value (M k) = LeanRidgelet.bochnerSynthesis μ φ (coefficient k))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight parameterJacobian) g
          (coefficient k))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g
          (value f))
  (h_parameter_measurable : ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun ξ ↦ g⁻¹ • ξ) μ =
        μ.withDensity fun ξ ↦ ↑(parameterJacobian g ξ))
  (h_parameter_jacobian : ∀ (g : G), Measurable (parameterJacobian g))
  (h_parameter_ne_zero : ∀ (g : G) (ξ : Ξ), parameterJacobian g ξ ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (parameterJacobian g ξ)) =
        LeanRidgelet.radonNikodymWeight dataJacobian g x) :
  LeanRidgelet.JointEquivariantMachine πParameter πData

def LeanRidgelet.bochnerSynthesisQuasiIntertwiningMap.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {K : Type u_5}
  {H : Type u_6} [NormedAddCommGroup K]
  [NormedSpace ℂ K] [NormedAddCommGroup H]
  [NormedSpace ℂ H]
  (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (πParameter : ContRepresentation ℂ G K)
  (πData : ContRepresentation ℂ G H)
  (coefficient : K → Ξ → ℂ)
  (value : H → X → Y)
  (h_value : Function.Injective value)
  (M : K →L[ℂ] H) (φ : X → Ξ → Y)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (hM :
    ∀ (k : K),
      value (M k) =
        LeanRidgelet.bochnerSynthesis μ φ
          (coefficient k))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight
            parameterJacobian)
          g (coefficient k))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.quasiUnitaryPullbackAction
          dataJacobian υ g (value f))
  (h_parameter_measurable :
    ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun ξ ↦ g⁻¹ • ξ) μ =
        μ.withDensity fun ξ ↦
          ↑(parameterJacobian g ξ))
  (h_parameter_jacobian :
    ∀ (g : G),
      Measurable (parameterJacobian g))
  (h_parameter_ne_zero :
    ∀ (g : G) (ξ : Ξ),
      parameterJacobian g ξ ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt
              (parameterJacobian g ξ)) =
        LeanRidgelet.radonNikodymWeight
          dataJacobian g x) :
  LeanRidgelet.JointEquivariantMachine
    πParameter πData

Implementation after :=

:= M
  isIntertwining' g := by
    ext k
    apply h_value
    calc
      value (M (πParameter g k)) =
          bochnerSynthesis μ φ (coefficient (πParameter g k)) := hM _
      _ = bochnerSynthesis μ φ
          (quasiRegularAction (radonNikodymWeight parameterJacobian) g (coefficient k)) := by
        rw [h_parameter]
      _ = quasiUnitaryPullbackAction dataJacobian υ g
          (bochnerSynthesis μ φ (coefficient k)) :=
        funext fun x ↦ bochnerSynthesis_quasi_intertwines μ υ φ dataJacobian
          parameterJacobian h_parameter_measurable h_parameter_map h_parameter_jacobian
          h_parameter_ne_zero h_joint h_balance g _ x
      _ = quasiUnitaryPullbackAction dataJacobian υ g (value (M k)) := by rw [hM]
      _ = value (πData g (M k)) := (h_data _ _).symm

Bundle a bounded quasi-invariant Bochner synthesis map as a continuous intertwiner. The
coordinate actions carry the same Radon--Nikodym weights as
`bochnerSynthesis_quasi_intertwines`.

Definition4.1.14

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Lemma 4.1.15

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Definition 3.8. A bounded ridgelet transform is a continuous intertwining map in the reverse direction.

Lean code for Definition4.1.14●1 definition

abbrevdefined in LeanRidgelet/HA/Operators.lean

complete

abbrev LeanRidgelet.JointEquivariantRidgelet.{u_1, u_2, u_3} {G : Type u_1}
  {H : Type u_2} {K : Type u_3} [Monoid G] [NormedAddCommGroup H]
  [NormedSpace ℂ H] [NormedAddCommGroup K] [NormedSpace ℂ K]
  (πData : ContRepresentation ℂ G H)
  (πParameter : ContRepresentation ℂ G K) : Type (max u_2 u_3)

abbrev LeanRidgelet.JointEquivariantRidgelet.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Monoid G]
  [NormedAddCommGroup H] [NormedSpace ℂ H]
  [NormedAddCommGroup K] [NormedSpace ℂ K]
  (πData : ContRepresentation ℂ G H)
  (πParameter :
    ContRepresentation ℂ G K) :
  Type (max u_2 u_3)

Implementation after :=

:=
  πData →ⁱL πParameter

A bounded joint-equivariant ridgelet transform from data space to parameter space.

Lemma4.1.15

uses 1used by 1✓L∃∀N

Lemma 3.9. The corresponding invariant or quasi-invariant change of variables makes ridgelet analysis an intertwiner.

Lean code for Lemma4.1.15●4 declarations

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.bochnerRidgelet_intertwines.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure X) (υ : UnitaryRepresentation G Y)
  (ψ : X → Ξ → Y)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_preserving :
    ∀ (g : G), MeasureTheory.MeasurePreserving (fun x ↦ g • x) μ μ)
  (h_embedding : ∀ (g : G), MeasurableEmbedding fun x ↦ g • x) (g : G)
  (f : X → Y) (ξ : Ξ) :
  LeanRidgelet.bochnerRidgelet μ ψ
      (LeanRidgelet.unitaryPullbackAction υ g f) ξ =
    LeanRidgelet.scalarPullbackAction g
      (LeanRidgelet.bochnerRidgelet μ ψ f) ξ

theorem LeanRidgelet.bochnerRidgelet_intertwines.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (ψ : X → Ξ → Y)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_preserving :
    ∀ (g : G),
      MeasureTheory.MeasurePreserving
        (fun x ↦ g • x) μ μ)
  (h_embedding :
    ∀ (g : G),
      MeasurableEmbedding fun x ↦ g • x)
  (g : G) (f : X → Y) (ξ : Ξ) :
  LeanRidgelet.bochnerRidgelet μ ψ
      (LeanRidgelet.unitaryPullbackAction
        υ g f)
      ξ =
    LeanRidgelet.scalarPullbackAction g
      (LeanRidgelet.bochnerRidgelet μ ψ f)
      ξ

Joint equivariance plus an invariant data measure makes the Bochner ridgelet pairing
intertwine the unitary data action and scalar pullback on parameters.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.bochnerRidgelet_quasi_intertwines.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure X) (υ : UnitaryRepresentation G Y)
  (ψ : X → Ξ → Y) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_data_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(dataJacobian g x))
  (h_data_jacobian : ∀ (g : G), Measurable (dataJacobian g))
  (h_data_ne_zero : ∀ (g : G) (x : X), dataJacobian g x ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight parameterJacobian g ξ)
  (g : G) (f : X → Y) (ξ : Ξ) :
  LeanRidgelet.bochnerRidgelet μ ψ
      (LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g f) ξ =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight parameterJacobian) g
      (LeanRidgelet.bochnerRidgelet μ ψ f) ξ

theorem LeanRidgelet.bochnerRidgelet_quasi_intertwines.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (ψ : X → Ξ → Y)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_data_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(dataJacobian g x))
  (h_data_jacobian :
    ∀ (g : G),
      Measurable (dataJacobian g))
  (h_data_ne_zero :
    ∀ (g : G) (x : X),
      dataJacobian g x ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight
          parameterJacobian g ξ)
  (g : G) (f : X → Y) (ξ : Ξ) :
  LeanRidgelet.bochnerRidgelet μ ψ
      (LeanRidgelet.quasiUnitaryPullbackAction
        dataJacobian υ g f)
      ξ =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        parameterJacobian)
      g
      (LeanRidgelet.bochnerRidgelet μ ψ f)
      ξ

Joint equivariance intertwines a quasi-invariant Bochner ridgelet pairing when the data
Jacobian's square root equals the parameter-side Radon--Nikodym multiplier.

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerRidgeletIntertwiningMap.{u_1, u_2, u_3, u_4, u_5,
    u_6}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  {K : Type u_5} {H : Type u_6} [NormedAddCommGroup K] [NormedSpace ℂ K]
  [NormedAddCommGroup H] [NormedSpace ℂ H] (μ : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y) (πData : ContRepresentation ℂ G H)
  (πParameter : ContRepresentation ℂ G K) (value : H → X → Y)
  (coefficient : K → Ξ → ℂ)
  (h_coefficient : Function.Injective coefficient) (R : H →L[ℂ] K)
  (ψ : X → Ξ → Y)
  (hR :
    ∀ (f : H),
      coefficient (R f) = LeanRidgelet.bochnerRidgelet μ ψ (value f))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.unitaryPullbackAction υ g (value f))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.scalarPullbackAction g (coefficient k))
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_preserving :
    ∀ (g : G), MeasureTheory.MeasurePreserving (fun x ↦ g • x) μ μ)
  (h_embedding : ∀ (g : G), MeasurableEmbedding fun x ↦ g • x) :
  LeanRidgelet.JointEquivariantRidgelet πData πParameter

def LeanRidgelet.bochnerRidgeletIntertwiningMap.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {K : Type u_5}
  {H : Type u_6} [NormedAddCommGroup K]
  [NormedSpace ℂ K] [NormedAddCommGroup H]
  [NormedSpace ℂ H]
  (μ : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (πData : ContRepresentation ℂ G H)
  (πParameter : ContRepresentation ℂ G K)
  (value : H → X → Y)
  (coefficient : K → Ξ → ℂ)
  (h_coefficient :
    Function.Injective coefficient)
  (R : H →L[ℂ] K) (ψ : X → Ξ → Y)
  (hR :
    ∀ (f : H),
      coefficient (R f) =
        LeanRidgelet.bochnerRidgelet μ ψ
          (value f))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.unitaryPullbackAction
          υ g (value f))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.scalarPullbackAction
          g (coefficient k))
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_preserving :
    ∀ (g : G),
      MeasureTheory.MeasurePreserving
        (fun x ↦ g • x) μ μ)
  (h_embedding :
    ∀ (g : G),
      MeasurableEmbedding fun x ↦ g • x) :
  LeanRidgelet.JointEquivariantRidgelet
    πData πParameter

Implementation after :=

:= R
  isIntertwining' g := by
    ext f
    apply h_coefficient
    calc
      coefficient (R (πData g f)) = bochnerRidgelet μ ψ (value (πData g f)) := hR _
      _ = bochnerRidgelet μ ψ (unitaryPullbackAction υ g (value f)) := by rw [h_data]
      _ = scalarPullbackAction g (bochnerRidgelet μ ψ (value f)) :=
        funext fun ξ ↦ bochnerRidgelet_intertwines μ υ ψ h_joint h_preserving h_embedding g _ ξ
      _ = scalarPullbackAction g (coefficient (R f)) := by rw [hR]
      _ = coefficient (πParameter g (R f)) := (h_parameter _ _).symm

Bundle a bounded Bochner ridgelet map as a continuous intertwiner once its coordinate
formula and the coordinate formulas for the two representations are known.

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerRidgeletQuasiIntertwiningMap.{u_1, u_2, u_3, u_4,
    u_5, u_6}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  {K : Type u_5} {H : Type u_6} [NormedAddCommGroup K] [NormedSpace ℂ K]
  [NormedAddCommGroup H] [NormedSpace ℂ H] (μ : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y) (πData : ContRepresentation ℂ G H)
  (πParameter : ContRepresentation ℂ G K) (value : H → X → Y)
  (coefficient : K → Ξ → ℂ)
  (h_coefficient : Function.Injective coefficient) (R : H →L[ℂ] K)
  (ψ : X → Ξ → Y) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (hR :
    ∀ (f : H),
      coefficient (R f) = LeanRidgelet.bochnerRidgelet μ ψ (value f))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g
          (value f))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight parameterJacobian) g
          (coefficient k))
  (h_data_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(dataJacobian g x))
  (h_data_jacobian : ∀ (g : G), Measurable (dataJacobian g))
  (h_data_ne_zero : ∀ (g : G) (x : X), dataJacobian g x ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight parameterJacobian g ξ) :
  LeanRidgelet.JointEquivariantRidgelet πData πParameter

def LeanRidgelet.bochnerRidgeletQuasiIntertwiningMap.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {K : Type u_5}
  {H : Type u_6} [NormedAddCommGroup K]
  [NormedSpace ℂ K] [NormedAddCommGroup H]
  [NormedSpace ℂ H]
  (μ : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (πData : ContRepresentation ℂ G H)
  (πParameter : ContRepresentation ℂ G K)
  (value : H → X → Y)
  (coefficient : K → Ξ → ℂ)
  (h_coefficient :
    Function.Injective coefficient)
  (R : H →L[ℂ] K) (ψ : X → Ξ → Y)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (hR :
    ∀ (f : H),
      coefficient (R f) =
        LeanRidgelet.bochnerRidgelet μ ψ
          (value f))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.quasiUnitaryPullbackAction
          dataJacobian υ g (value f))
  (h_parameter :
    ∀ (g : G) (k : K),
      coefficient ((πParameter g) k) =
        LeanRidgelet.quasiRegularAction
          (LeanRidgelet.radonNikodymWeight
            parameterJacobian)
          g (coefficient k))
  (h_data_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(dataJacobian g x))
  (h_data_jacobian :
    ∀ (g : G),
      Measurable (dataJacobian g))
  (h_data_ne_zero :
    ∀ (g : G) (x : X),
      dataJacobian g x ≠ 0)
  (h_joint :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight
          parameterJacobian g ξ) :
  LeanRidgelet.JointEquivariantRidgelet
    πData πParameter

Implementation after :=

:= R
  isIntertwining' g := by
    ext f
    apply h_coefficient
    calc
      coefficient (R (πData g f)) = bochnerRidgelet μ ψ (value (πData g f)) := hR _
      _ = bochnerRidgelet μ ψ (quasiUnitaryPullbackAction dataJacobian υ g (value f)) := by
        rw [h_data]
      _ = quasiRegularAction (radonNikodymWeight parameterJacobian) g
          (bochnerRidgelet μ ψ (value f)) :=
        funext fun ξ ↦ bochnerRidgelet_quasi_intertwines μ υ ψ dataJacobian
          parameterJacobian h_data_measurable h_data_map h_data_jacobian h_data_ne_zero
          h_joint h_balance g _ ξ
      _ = quasiRegularAction (radonNikodymWeight parameterJacobian) g
          (coefficient (R f)) := by rw [hR]
      _ = coefficient (πParameter g (R f)) := (h_parameter _ _).symm

Bundle a bounded quasi-invariant Bochner ridgelet map as a continuous intertwiner.

Theorem4.1.16

Statement uses 3

Statement dependency previews

Preview

Theorem 4.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 4.1.17

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Theorem 3.10. The composite M_\phi R_\psi belongs to the commutant and is therefore c_{\phi,\psi}\,\mathrm{id}. The formalization covers both individually bounded intertwiners and the weaker hypothesis that only the pointwise composite has a bounded extension. Deviation. Over \mathbb C, the displayed scalar is sesquilinear rather than bilinear in the two features.

Lean code for Theorem4.1.16●3 declarations

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerReconstructionQuasiIntertwiningMap.{u_1, u_2, u_3,
    u_4, u_6}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [MeasurableSpace Ξ] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {H : Type u_6} [NormedAddCommGroup H]
  [NormedSpace ℂ H] (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X) (υ : UnitaryRepresentation G Y)
  (πData : ContRepresentation ℂ G H) (value : H → X → Y)
  (h_value : Function.Injective value) (T : H →L[ℂ] H) (φ ψ : X → Ξ → Y)
  (dataJacobian : G → X → NNReal) (parameterJacobian : G → Ξ → NNReal)
  (hT :
    ∀ (f : H),
      value (T f) =
        LeanRidgelet.bochnerSynthesis μParameter φ
          (LeanRidgelet.bochnerRidgelet μData ψ (value f)))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g
          (value f))
  (h_parameter_measurable : ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun ξ ↦ g⁻¹ • ξ) μParameter =
        μParameter.withDensity fun ξ ↦ ↑(parameterJacobian g ξ))
  (h_parameter_jacobian : ∀ (g : G), Measurable (parameterJacobian g))
  (h_parameter_ne_zero : ∀ (g : G) (ξ : Ξ), parameterJacobian g ξ ≠ 0)
  (h_data_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μData =
        μData.withDensity fun x ↦ ↑(dataJacobian g x))
  (h_data_jacobian : ∀ (g : G), Measurable (dataJacobian g))
  (h_data_ne_zero : ∀ (g : G) (x : X), dataJacobian g x ≠ 0)
  (h_joint_φ :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_joint_ψ :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_synthesis_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (parameterJacobian g ξ)) =
        LeanRidgelet.radonNikodymWeight dataJacobian g x)
  (h_ridgelet_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight parameterJacobian g ξ) :
  LeanRidgelet.JointEquivariantMachine πData πData

def LeanRidgelet.bochnerReconstructionQuasiIntertwiningMap.{u_1,
    u_2, u_3, u_4, u_6}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {H : Type u_6}
  [NormedAddCommGroup H] [NormedSpace ℂ H]
  (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (πData : ContRepresentation ℂ G H)
  (value : H → X → Y)
  (h_value : Function.Injective value)
  (T : H →L[ℂ] H) (φ ψ : X → Ξ → Y)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (hT :
    ∀ (f : H),
      value (T f) =
        LeanRidgelet.bochnerSynthesis
          μParameter φ
          (LeanRidgelet.bochnerRidgelet
            μData ψ (value f)))
  (h_data :
    ∀ (g : G) (f : H),
      value ((πData g) f) =
        LeanRidgelet.quasiUnitaryPullbackAction
          dataJacobian υ g (value f))
  (h_parameter_measurable :
    ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun ξ ↦ g⁻¹ • ξ) μParameter =
        μParameter.withDensity fun ξ ↦
          ↑(parameterJacobian g ξ))
  (h_parameter_jacobian :
    ∀ (g : G),
      Measurable (parameterJacobian g))
  (h_parameter_ne_zero :
    ∀ (g : G) (ξ : Ξ),
      parameterJacobian g ξ ≠ 0)
  (h_data_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μData =
        μData.withDensity fun x ↦
          ↑(dataJacobian g x))
  (h_data_jacobian :
    ∀ (g : G),
      Measurable (dataJacobian g))
  (h_data_ne_zero :
    ∀ (g : G) (x : X),
      dataJacobian g x ≠ 0)
  (h_joint_φ :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_joint_ψ :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_synthesis_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt
              (parameterJacobian g ξ)) =
        LeanRidgelet.radonNikodymWeight
          dataJacobian g x)
  (h_ridgelet_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        LeanRidgelet.radonNikodymWeight
          parameterJacobian g ξ) :
  LeanRidgelet.JointEquivariantMachine
    πData πData

Implementation after :=

:= T
  isIntertwining' g := by
    ext f
    apply h_value
    calc
      value (T (πData g f)) =
          bochnerSynthesis μParameter φ (bochnerRidgelet μData ψ (value (πData g f))) := hT _
      _ = bochnerSynthesis μParameter φ
          (bochnerRidgelet μData ψ
            (quasiUnitaryPullbackAction dataJacobian υ g (value f))) := by
        rw [h_data]
      _ = bochnerSynthesis μParameter φ
          (quasiRegularAction (radonNikodymWeight parameterJacobian) g
            (bochnerRidgelet μData ψ (value f))) := by
        congr 1
        exact funext fun ξ ↦ bochnerRidgelet_quasi_intertwines μData υ ψ
          dataJacobian parameterJacobian h_data_measurable h_data_map h_data_jacobian
          h_data_ne_zero h_joint_ψ h_ridgelet_balance g _ ξ
      _ = quasiUnitaryPullbackAction dataJacobian υ g
          (bochnerSynthesis μParameter φ (bochnerRidgelet μData ψ (value f))) :=
        funext fun x ↦ bochnerSynthesis_quasi_intertwines μParameter υ φ
          dataJacobian parameterJacobian h_parameter_measurable h_parameter_map
          h_parameter_jacobian h_parameter_ne_zero h_joint_φ h_synthesis_balance g _ x
      _ = quasiUnitaryPullbackAction dataJacobian υ g (value (T f)) := by rw [hT]
      _ = value (πData g (T f)) := (h_data _ _).symm

Bundle a bounded extension of the *composite* pointwise Bochner synthesis/ridgelet formula as
an endomorphism intertwiner. Unlike `bochnerSynthesisQuasiIntertwiningMap` followed by
`bochnerRidgeletQuasiIntertwiningMap`, this construction assumes only that the composite `T` is
bounded. The two intermediate integrals remain pointwise functions and need not separately define
bounded maps between `L²` spaces. This is the weak boundedness interpretation used in Theorem 3.10
of the article.

theoremdefined in LeanRidgelet/HA/Reconstruction.lean

complete

theorem LeanRidgelet.ha_reconstruction_of_hasSchurProperty.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [NormedSpace ℂ K]
  (πData : UnitaryRepresentation G H) (hschur : πData.HasSchurProperty)
  (πParameter : ContRepresentation ℂ G K)
  (M :
    LeanRidgelet.JointEquivariantMachine πParameter
      πData.toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet πData.toContRepresentation
      πParameter) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator M R =
      c • ContinuousLinearMap.id ℂ H

theorem LeanRidgelet.ha_reconstruction_of_hasSchurProperty.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [NormedSpace ℂ K]
  (πData : UnitaryRepresentation G H)
  (hschur : πData.HasSchurProperty)
  (πParameter : ContRepresentation ℂ G K)
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter
      πData.toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData.toContRepresentation
      πParameter) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator
        M R =
      c • ContinuousLinearMap.id ℂ H

Theorem 3.10 conditional on precisely the Schur property it uses. This version has no hidden
analytic assumption and no dependency on a placeholder.

theoremdefined in LeanRidgelet/HA/Reconstruction.lean

complete

theorem LeanRidgelet.ha_reconstruction_formula.{u_1, u_2, u_3} {G : Type u_1}
  {H : Type u_2} {K : Type u_3} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup K]
  [NormedSpace ℂ K] (πData : UnitaryRepresentation G H)
  (hirr : πData.IsTopologicallyIrreducible)
  (πParameter : ContRepresentation ℂ G K)
  (M :
    LeanRidgelet.JointEquivariantMachine πParameter
      πData.toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet πData.toContRepresentation
      πParameter) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator M R =
      c • ContinuousLinearMap.id ℂ H

theorem LeanRidgelet.ha_reconstruction_formula.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [NormedSpace ℂ K]
  (πData : UnitaryRepresentation G H)
  (hirr :
    πData.IsTopologicallyIrreducible)
  (πParameter : ContRepresentation ℂ G K)
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter
      πData.toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData.toContRepresentation
      πParameter) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator
        M R =
      c • ContinuousLinearMap.id ℂ H

The paper-level reconstruction formula, stated from topological irreducibility.

Theorem4.1.17

uses 1used by 0✓L∃∀N

Remark 3.11. A nonzero reconstruction scalar gives the normalized ridgelet right inverse.

Lean code for Theorem4.1.17●1 theorem

theoremdefined in LeanRidgelet/HA/Reconstruction.lean

complete

theorem LeanRidgelet.ha_normalizedRidgelet_rightInverse.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K]
  [NormedSpace ℂ K] {πData : ContRepresentation ℂ G H}
  {πParameter : ContRepresentation ℂ G K}
  (M : LeanRidgelet.JointEquivariantMachine πParameter πData)
  (R : LeanRidgelet.JointEquivariantRidgelet πData πParameter) {c : ℂ}
  (hrec :
    LeanRidgelet.jointReconstructionOperator M R =
      c • ContinuousLinearMap.id ℂ H)
  (hc : c ≠ 0) :
  Function.RightInverse ⇑(c⁻¹ • R.toContinuousLinearMap) ⇑M

theorem LeanRidgelet.ha_normalizedRidgelet_rightInverse.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup K] [NormedSpace ℂ K]
  {πData : ContRepresentation ℂ G H}
  {πParameter : ContRepresentation ℂ G K}
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter πData)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData πParameter)
  {c : ℂ}
  (hrec :
    LeanRidgelet.jointReconstructionOperator
        M R =
      c • ContinuousLinearMap.id ℂ H)
  (hc : c ≠ 0) :
  Function.RightInverse
    ⇑(c⁻¹ • R.toContinuousLinearMap) ⇑M

A nonzero reconstruction scalar makes the normalized ridgelet transform a right inverse of
the machine. This is the constructive universality conclusion following Theorem 3.10.

Sections 4--8: architectures and discussion

Corollary4.1.18

Statement uses 2

Statement dependency previews

Preview

Lemma 4.1.11

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Corollary 4.1. The reconstruction theorem applies to a heterogeneous finite cascade.

Lean code for Corollary4.1.18●2 theorems

theoremdefined in LeanRidgelet/HA/Deep.lean

complete

theorem LeanRidgelet.deepRidgelet_reconstruction_formula.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [NormedSpace ℂ K]
  (πData : UnitaryRepresentation G H)
  (hirr : πData.IsTopologicallyIrreducible)
  (πParameter : ContRepresentation ℂ G K)
  (M :
    LeanRidgelet.JointEquivariantMachine πParameter
      πData.toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet πData.toContRepresentation
      πParameter) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator M R =
      c • ContinuousLinearMap.id ℂ H

theorem LeanRidgelet.deepRidgelet_reconstruction_formula.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [NormedSpace ℂ K]
  (πData : UnitaryRepresentation G H)
  (hirr :
    πData.IsTopologicallyIrreducible)
  (πParameter : ContRepresentation ℂ G K)
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter
      πData.toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData.toContRepresentation
      πParameter) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator
        M R =
      c • ContinuousLinearMap.id ℂ H

Corollary 4.1 at bounded-operator level. The finite-depth construction contributes joint
equivariance through `isJointEquivariant_deepFeature`; boundedness and the integral formulas are
supplied independently by the Bochner bridge or by the L2 operator theory.

theoremdefined in LeanRidgelet/HA/Deep.lean

complete

theorem LeanRidgelet.deepRidgelet_normalized_rightInverse.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K]
  [NormedSpace ℂ K] {πData : ContRepresentation ℂ G H}
  {πParameter : ContRepresentation ℂ G K}
  (M : LeanRidgelet.JointEquivariantMachine πParameter πData)
  (R : LeanRidgelet.JointEquivariantRidgelet πData πParameter) {c : ℂ}
  (hrec :
    LeanRidgelet.jointReconstructionOperator M R =
      c • ContinuousLinearMap.id ℂ H)
  (hc : c ≠ 0) :
  Function.RightInverse ⇑(c⁻¹ • R.toContinuousLinearMap) ⇑M

theorem LeanRidgelet.deepRidgelet_normalized_rightInverse.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup K] [NormedSpace ℂ K]
  {πData : ContRepresentation ℂ G H}
  {πParameter : ContRepresentation ℂ G K}
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter πData)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData πParameter)
  {c : ℂ}
  (hrec :
    LeanRidgelet.jointReconstructionOperator
        M R =
      c • ContinuousLinearMap.id ℂ H)
  (hc : c ≠ 0) :
  Function.RightInverse
    ⇑(c⁻¹ • R.toContinuousLinearMap) ⇑M

A nonzero reconstruction scalar makes the normalized deep ridgelet a right inverse.

Definition4.1.19

uses 1used by 1✓L∃∀N

Section 5 feature covariance. The affine input action is absorbed by the first parameter and the output action by the final readout; both identities propagate through arbitrary finite depth.

Lean code for Definition4.1.19●2 declarations

defdefined in LeanRidgelet/HA/FullyConnected.lean

complete

def LeanRidgelet.deepFullyConnectedFeature.{u_1, u_2, u_3}
  {X : ℕ → Type u_1} {P : ℕ → Type u_2} {Q : ℕ → Type u_3}
  [(i : ℕ) → AddCommGroup (X i)] [(i : ℕ) → Module ℝ (X i)]
  [(i : ℕ) → AddCommGroup (P i)] [(i : ℕ) → Module ℝ (P i)]
  [(i : ℕ) → AddCommGroup (Q i)] [(i : ℕ) → Module ℝ (Q i)]
  (σ : (i : ℕ) → P i → Q i) (n : ℕ) :
  X 0 →
    LeanRidgelet.DeepParameters
        (fun i ↦
          LeanRidgelet.FullyConnectedParameter (X i) (P i) (Q i)
            (X (i + 1)))
        n →
      X n

def LeanRidgelet.deepFullyConnectedFeature.{u_1,
    u_2, u_3}
  {X : ℕ → Type u_1} {P : ℕ → Type u_2}
  {Q : ℕ → Type u_3}
  [(i : ℕ) → AddCommGroup (X i)]
  [(i : ℕ) → Module ℝ (X i)]
  [(i : ℕ) → AddCommGroup (P i)]
  [(i : ℕ) → Module ℝ (P i)]
  [(i : ℕ) → AddCommGroup (Q i)]
  [(i : ℕ) → Module ℝ (Q i)]
  (σ : (i : ℕ) → P i → Q i) (n : ℕ) :
  X 0 →
    LeanRidgelet.DeepParameters
        (fun i ↦
          LeanRidgelet.FullyConnectedParameter
            (X i) (P i) (Q i) (X (i + 1)))
        n →
      X n

Implementation after :=

:=
  deepFeature (fun i ↦ fullyConnectedFeature (σ i)) n

The depth-`n+1` fully-connected feature associated with heterogeneous activations.

theoremdefined in LeanRidgelet/HA/FullyConnected.lean

complete

theorem LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant.{u_1, u_2,
    u_3}
  {X : ℕ → Type u_1} {P : ℕ → Type u_2} {Q : ℕ → Type u_3}
  [(i : ℕ) → AddCommGroup (X i)] [(i : ℕ) → Module ℝ (X i)]
  [(i : ℕ) → AddCommGroup (P i)] [(i : ℕ) → Module ℝ (P i)]
  [(i : ℕ) → AddCommGroup (Q i)] [(i : ℕ) → Module ℝ (Q i)]
  (σ : (i : ℕ) → P i → Q i) (n : ℕ) (L : X 0 ≃ₗ[ℝ] X 0) (t : X 0)
  (R : X (n + 1) ≃ₗ[ℝ] X (n + 1)) (x : X 0)
  (ξ :
    LeanRidgelet.DeepParameters
      (fun i ↦
        LeanRidgelet.FullyConnectedParameter (X i) (P i) (Q i)
          (X (i + 1)))
      (n + 1)) :
  LeanRidgelet.deepFullyConnectedFeature σ (n + 1) (L x + t)
      (LeanRidgelet.DeepParameters.mapLast
        (LeanRidgelet.fullyConnectedOutputParameterTransform R)
        (LeanRidgelet.DeepParameters.mapFirst
          (LeanRidgelet.fullyConnectedInputParameterTransform L t) ξ)) =
    R (LeanRidgelet.deepFullyConnectedFeature σ (n + 1) x ξ)

theorem LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant.{u_1,
    u_2, u_3}
  {X : ℕ → Type u_1} {P : ℕ → Type u_2}
  {Q : ℕ → Type u_3}
  [(i : ℕ) → AddCommGroup (X i)]
  [(i : ℕ) → Module ℝ (X i)]
  [(i : ℕ) → AddCommGroup (P i)]
  [(i : ℕ) → Module ℝ (P i)]
  [(i : ℕ) → AddCommGroup (Q i)]
  [(i : ℕ) → Module ℝ (Q i)]
  (σ : (i : ℕ) → P i → Q i) (n : ℕ)
  (L : X 0 ≃ₗ[ℝ] X 0) (t : X 0)
  (R : X (n + 1) ≃ₗ[ℝ] X (n + 1))
  (x : X 0)
  (ξ :
    LeanRidgelet.DeepParameters
      (fun i ↦
        LeanRidgelet.FullyConnectedParameter
          (X i) (P i) (Q i) (X (i + 1)))
      (n + 1)) :
  LeanRidgelet.deepFullyConnectedFeature σ
      (n + 1) (L x + t)
      (LeanRidgelet.DeepParameters.mapLast
        (LeanRidgelet.fullyConnectedOutputParameterTransform
          R)
        (LeanRidgelet.DeepParameters.mapFirst
          (LeanRidgelet.fullyConnectedInputParameterTransform
            L t)
          ξ)) =
    R
      (LeanRidgelet.deepFullyConnectedFeature
        σ (n + 1) x ξ)

Section 5 joint-equivariance calculation: the affine input transformation is absorbed by the
first parameters and the output transformation by the final readout, for every finite depth and
every choice of activation functions.

Lemma4.1.20

Statement uses 2

Statement dependency previews

Preview

Theorem 4.1.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Lemma 5.1. The concrete complexified O(m)\times\operatorname{Aff}(m) action on vector-valued L^2 is implemented. Finite coordinate reconstruction and two Schur arguments prove the needed finite-output product irreducibility, conditional only on the scalar affine endpoint.

Lean code for Lemma4.1.20●3 declarations

defdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

def LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation.{u_4}
  {ι : Type u_4} [Fintype ι] [DecidableEq ι]
  [MeasurableSpace (EuclideanSpace ℝ ι)]
  [BorelSpace (EuclideanSpace ℝ ι)] :
  UnitaryRepresentation
    (↥(Matrix.orthogonalGroup ι ℝ) ×
      (EuclideanSpace ℝ ι ≃ᵃ[ℝ] EuclideanSpace ℝ ι))
    ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 MeasureTheory.volume)

def LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation.{u_4}
  {ι : Type u_4} [Fintype ι]
  [DecidableEq ι]
  [MeasurableSpace (EuclideanSpace ℝ ι)]
  [BorelSpace (EuclideanSpace ℝ ι)] :
  UnitaryRepresentation
    (↥(Matrix.orthogonalGroup ι ℝ) ×
      (EuclideanSpace ℝ ι ≃ᵃ[ℝ]
        EuclideanSpace ℝ ι))
    ↥(MeasureTheory.Lp
        (EuclideanSpace ℂ ι) 2
        MeasureTheory.volume)

Implementation after :=

:=
  fullyConnectedLpUnitaryRepresentation
    (Matrix.standardComplexOrthogonalRepresentation (ι := ι))

The concrete Section 5 representation of
`O(ι) × Aff(EuclideanSpace ℝ ι)` on vector-valued `L²`, with the standard orthogonal action on
the complexified output coordinates.

theoremdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

theorem LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation_apply_ae.{u_4}
  {ι : Type u_4} [Fintype ι] [DecidableEq ι]
  [MeasurableSpace (EuclideanSpace ℝ ι)]
  [BorelSpace (EuclideanSpace ℝ ι)]
  (g :
    ↥(Matrix.orthogonalGroup ι ℝ) ×
      (EuclideanSpace ℝ ι ≃ᵃ[ℝ] EuclideanSpace ℝ ι))
  (f :
    ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 MeasureTheory.volume)) :
  ↑↑(↑(LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation g)
          f) =ᵐ[MeasureTheory.volume]
    fun x ↦
    LeanRidgelet.radonNikodymWeight LeanRidgelet.affineDataJacobian g.2
        x •
      WithLp.toLp 2
        (((↑g.1).map RCLike.ofReal).mulVec (↑↑f (g.2⁻¹ • x)).ofLp)

theorem LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation_apply_ae.{u_4}
  {ι : Type u_4} [Fintype ι]
  [DecidableEq ι]
  [MeasurableSpace (EuclideanSpace ℝ ι)]
  [BorelSpace (EuclideanSpace ℝ ι)]
  (g :
    ↥(Matrix.orthogonalGroup ι ℝ) ×
      (EuclideanSpace ℝ ι ≃ᵃ[ℝ]
        EuclideanSpace ℝ ι))
  (f :
    ↥(MeasureTheory.Lp
        (EuclideanSpace ℂ ι) 2
        MeasureTheory.volume)) :
  ↑↑(↑(LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation
              g)
          f) =ᵐ[MeasureTheory.volume]
    fun x ↦
    LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineDataJacobian
        g.2 x •
      WithLp.toLp 2
        (((↑g.1).map RCLike.ofReal).mulVec
          (↑↑f (g.2⁻¹ • x)).ofLp)

The standard `O(ι) × Aff(ι)` representation acts by the article's determinant-corrected
affine pullback followed by complexified orthogonal matrix multiplication.

theoremdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

theorem LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation_isTopologicallyIrreducible_of.{u_4}
  {ι : Type u_4} [Fintype ι] [DecidableEq ι]
  [MeasurableSpace (EuclideanSpace ℝ ι)]
  [BorelSpace (EuclideanSpace ℝ ι)] [Nonempty ι]
  (hAffine :
    (LeanRidgelet.affineDataLpUnitaryRepresentation
        MeasureTheory.volume).IsTopologicallyIrreducible) :
  LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation.IsTopologicallyIrreducible

theorem LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation_isTopologicallyIrreducible_of.{u_4}
  {ι : Type u_4} [Fintype ι]
  [DecidableEq ι]
  [MeasurableSpace (EuclideanSpace ℝ ι)]
  [BorelSpace (EuclideanSpace ℝ ι)]
  [Nonempty ι]
  (hAffine :
    (LeanRidgelet.affineDataLpUnitaryRepresentation
        MeasureTheory.volume).IsTopologicallyIrreducible) :
  LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation.IsTopologicallyIrreducible

Lemma 5.1 for the standard complexified orthogonal output action, conditional only on scalar
affine irreducibility.  The latter remains the separately named Mackey-imprimitivity endpoint.

Theorem4.1.21

uses 1used by 1✓L∃∀N

Theorem 6.1. The group-convolutional orbit lift reduces at the identity to the base machine, so a base reconstruction identity transports to the group-valued output.

Lean code for Theorem4.1.21●3 declarations

defdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

def LeanRidgelet.groupConvolutionalFeature.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (υ : UnitaryRepresentation G Y) (φ : X → Ξ → Y)
  (x : X) (ξ : Ξ) (g : G) : Y

def LeanRidgelet.groupConvolutionalFeature.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (x : X) (ξ : Ξ)
  (g : G) : Y

Implementation after :=

:=
  (υ g : Y →L[ℂ] Y) (φ (g⁻¹ • x) ξ)

The `G`-convolutional/orbit lift of a base feature map.

theoremdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

theorem LeanRidgelet.groupConvolutionalFeature_equivariant.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (υ : UnitaryRepresentation G Y) (φ : X → Ξ → Y)
  (ξ : Ξ) :
  LeanRidgelet.IsGroupConvolutionEquivariant υ fun x g ↦
    LeanRidgelet.groupConvolutionalFeature υ φ x ξ g

theorem LeanRidgelet.groupConvolutionalFeature_equivariant.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (ξ : Ξ) :
  LeanRidgelet.IsGroupConvolutionEquivariant
    υ fun x g ↦
    LeanRidgelet.groupConvolutionalFeature
      υ φ x ξ g

Section 6.2: the orbit-lifted feature is `G`-equivariant for every base feature.

theoremdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

theorem LeanRidgelet.groupConvolutional_synthesis_ridgelet.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MeasurableSpace X] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X) (υ : UnitaryRepresentation G Y)
  (φ ψ : X → Ξ → Y) (f : X → G → Y)
  (hf : LeanRidgelet.IsGroupConvolutionEquivariant υ f) (c : ℂ)
  (hrec :
    ∀ (x : X),
      LeanRidgelet.bochnerSynthesis μParameter φ
          (LeanRidgelet.bochnerRidgelet μData ψ fun y ↦ f y 1) x =
        c • f x 1)
  (x : X) (g : G) :
  LeanRidgelet.groupConvolutionalSynthesis μParameter υ φ
      (LeanRidgelet.groupConvolutionalRidgelet μData ψ f) x g =
    c • f x g

theorem LeanRidgelet.groupConvolutional_synthesis_ridgelet.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MeasurableSpace X]
  [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (φ ψ : X → Ξ → Y) (f : X → G → Y)
  (hf :
    LeanRidgelet.IsGroupConvolutionEquivariant
      υ f)
  (c : ℂ)
  (hrec :
    ∀ (x : X),
      LeanRidgelet.bochnerSynthesis
          μParameter φ
          (LeanRidgelet.bochnerRidgelet
            μData ψ fun y ↦ f y 1)
          x =
        c • f x 1)
  (x : X) (g : G) :
  LeanRidgelet.groupConvolutionalSynthesis
      μParameter υ φ
      (LeanRidgelet.groupConvolutionalRidgelet
        μData ψ f)
      x g =
    c • f x g

Theorem 6.1 with the convolutional ridgelet inserted explicitly.

Definition4.1.22

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.8

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Section 7. A quadratic form followed by an arbitrary activation, with symmetric coefficients represented as self-adjoint continuous endomorphisms. The parameter action of the affine group is linear, the scalar argument of the activation is invariant under the data and parameter actions together, and the action law follows because a parameter is determined by its scalar functional. The parameter determinant factors through the congruence on symmetric coefficients; that factor is kept abstract, since only its non-vanishing is used, and it is exactly the Radon--Nikodym density of the parameter action, so the quasi-invariant parameter measure and its L² representation are obtained from it. That measure is then replaced by a relatively invariant one, weighted by a power of the determinant of the symmetric coefficient, which restores the balance the quasi-invariant Bochner identities need; with it the synthesis and ridgelet identities hold in their untwisted form, and Schur's lemma applied to the proved irreducibility of the data representation gives the reconstruction scalar and the right inverse. Boundedness of the two operators is the one input.

Lean code for Definition4.1.22●16 declarations

abbrevdefined in LeanRidgelet/HA/Quadratic.lean

complete

abbrev LeanRidgelet.QuadraticParameter.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : Type u_2

abbrev LeanRidgelet.QuadraticParameter.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : Type u_2

Implementation after :=

:= QuadraticSymmetric E × E × ℝ

The parameter space `(A, b, c)` of a quadratic-form feature.

defdefined in LeanRidgelet/HA/Quadratic.lean

complete

def LeanRidgelet.quadraticFeature.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (σ : ℝ → ℝ) (x : E) (ξ : LeanRidgelet.QuadraticParameter E) : ℝ

def LeanRidgelet.quadraticFeature.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (σ : ℝ → ℝ)
  (x : E)
  (ξ :
    LeanRidgelet.QuadraticParameter E) :
  ℝ

Implementation after :=

:=
  σ (quadraticArgument x ξ)

The quadratic-form feature `σ(xᵀ A x + xᵀ b + c)` of Section 7.

defdefined in LeanRidgelet/HA/Quadratic.lean

complete

def LeanRidgelet.quadraticParameterLinearEquiv.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) :
  LeanRidgelet.QuadraticParameter E ≃ₗ[ℝ]
    LeanRidgelet.QuadraticParameter E

def LeanRidgelet.quadraticParameterLinearEquiv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) :
  LeanRidgelet.QuadraticParameter E ≃ₗ[ℝ]
    LeanRidgelet.QuadraticParameter E

Implementation after :=

:=
  (quadraticCongr g.linear.symm).skewProd (quadraticLinearEquiv g) (quadraticSymmetricShear g)

The parameter action of the affine group on quadratic parameters.  If `g x = L x + t`, it
sends `(A, b, c)` to `(L⁻ᵀ A L⁻¹, L⁻ᵀ b - 2 L⁻ᵀ A L⁻¹ t, c + tᵀ L⁻ᵀ A L⁻¹ t - tᵀ L⁻ᵀ b)`.

theoremdefined in LeanRidgelet/HA/Quadratic.lean

complete

theorem LeanRidgelet.quadraticArgument_invariant.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) (x : E) (ξ : LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.quadraticArgument (g x)
      ((LeanRidgelet.quadraticParameterLinearEquiv g) ξ) =
    LeanRidgelet.quadraticArgument x ξ

theorem LeanRidgelet.quadraticArgument_invariant.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (g : E ≃ᵃ[ℝ] E)
  (x : E)
  (ξ :
    LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.quadraticArgument (g x)
      ((LeanRidgelet.quadraticParameterLinearEquiv
          g)
        ξ) =
    LeanRidgelet.quadraticArgument x ξ

The quadratic functional is invariant under the joint affine data/parameter action.  This is
the computation of Section 7 and Appendix F of the article.

theoremdefined in LeanRidgelet/HA/Quadratic.lean

complete

theorem LeanRidgelet.quadraticFeature_invariant.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (σ : ℝ → ℝ) (g : E ≃ᵃ[ℝ] E) (x : E)
  (ξ : LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.quadraticFeature σ (g x)
      ((LeanRidgelet.quadraticParameterLinearEquiv g) ξ) =
    LeanRidgelet.quadraticFeature σ x ξ

theorem LeanRidgelet.quadraticFeature_invariant.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (σ : ℝ → ℝ)
  (g : E ≃ᵃ[ℝ] E) (x : E)
  (ξ :
    LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.quadraticFeature σ (g x)
      ((LeanRidgelet.quadraticParameterLinearEquiv
          g)
        ξ) =
    LeanRidgelet.quadraticFeature σ x ξ

The quadratic feature is invariant under the joint affine data/parameter action.

defdefined in LeanRidgelet/HA/Quadratic.lean

complete

def LeanRidgelet.quadraticParameterMulAction.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  MulAction (E ≃ᵃ[ℝ] E) (LeanRidgelet.QuadraticParameter E)

def LeanRidgelet.quadraticParameterMulAction.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  MulAction (E ≃ᵃ[ℝ] E)
    (LeanRidgelet.QuadraticParameter E)

Implementation after :=

:= by
    apply quadraticArgument_parameter_injective
    funext x
    change quadraticArgument x (quadraticParameterLinearEquiv (AffineEquiv.refl ℝ E) ξ) =
      quadraticArgument x ξ
    simpa using quadraticArgument_invariant (AffineEquiv.refl ℝ E) x ξ
  mul_smul g h ξ := by
    apply quadraticArgument_parameter_injective
    funext x
    have hgh := quadraticArgument_invariant (g * h) ((g * h).symm x) ξ
    have hg := quadraticArgument_invariant g (g.symm x) (quadraticParameterLinearEquiv h ξ)
    have hh := quadraticArgument_invariant h (h.symm (g.symm x)) ξ
    have hgh' : quadraticArgument x (quadraticParameterLinearEquiv (g * h) ξ) =
        quadraticArgument ((g * h).symm x) ξ := by simpa using hgh
    have hg' : quadraticArgument x
          (quadraticParameterLinearEquiv g (quadraticParameterLinearEquiv h ξ)) =
        quadraticArgument (g.symm x) (quadraticParameterLinearEquiv h ξ) := by
      simpa using hg
    have hh' : quadraticArgument (g.symm x) (quadraticParameterLinearEquiv h ξ) =
        quadraticArgument (h.symm (g.symm x)) ξ := by simpa using hh
    exact hgh'.trans <| by
      rw [show (g * h).symm x = h.symm (g.symm x) by rfl]
      exact (hg'.trans hh').symm

The joint affine action on quadratic parameters.

theoremdefined in LeanRidgelet/HA/Quadratic.lean

complete

theorem LeanRidgelet.det_quadraticParameterLinearEquiv.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) :
  LinearMap.det ↑(LeanRidgelet.quadraticParameterLinearEquiv g) =
    LinearMap.det ↑(LeanRidgelet.quadraticCongr g.linear.symm) *
      (LinearMap.det ↑g.linear)⁻¹

theorem LeanRidgelet.det_quadraticParameterLinearEquiv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) :
  LinearMap.det
      ↑(LeanRidgelet.quadraticParameterLinearEquiv
          g) =
    LinearMap.det
        ↑(LeanRidgelet.quadraticCongr
            g.linear.symm) *
      (LinearMap.det ↑g.linear)⁻¹

The determinant of the quadratic parameter action is the determinant of its symmetric
congruence block times the reciprocal determinant of the linear part.

defdefined in LeanRidgelet/HA/QuadraticMeasure.lean

complete

def LeanRidgelet.quadraticParameterJacobian.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) : LeanRidgelet.QuadraticParameter E → NNReal

def LeanRidgelet.quadraticParameterJacobian.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (g : E ≃ᵃ[ℝ] E) :
  LeanRidgelet.QuadraticParameter E →
    NNReal

Implementation after :=

:=
  fun _ ↦ ‖LinearMap.det
    (quadraticParameterLinearEquiv g : QuadraticParameter E →ₗ[ℝ] QuadraticParameter E)‖₊

The constant Radon--Nikodym density for the inverse quadratic parameter action.  It is the
absolute determinant of the parameter equivalence, left unevaluated.

theoremdefined in LeanRidgelet/HA/QuadraticMeasure.lean

complete

theorem LeanRidgelet.quadraticParameterJacobian_cocycle.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (g h : E ≃ᵃ[ℝ] E) (ξ : LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.quadraticParameterJacobian (g * h) ξ =
    LeanRidgelet.quadraticParameterJacobian g (h • ξ) *
      LeanRidgelet.quadraticParameterJacobian h ξ

theorem LeanRidgelet.quadraticParameterJacobian_cocycle.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (g h : E ≃ᵃ[ℝ] E)
  (ξ :
    LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.quadraticParameterJacobian
      (g * h) ξ =
    LeanRidgelet.quadraticParameterJacobian
        g (h • ξ) *
      LeanRidgelet.quadraticParameterJacobian
        h ξ

The parameter Jacobian obeys the Radon--Nikodym cocycle law.

theoremdefined in LeanRidgelet/HA/QuadraticMeasure.lean

complete

theorem LeanRidgelet.quadraticParameter_group_map_eq_withDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace (LeanRidgelet.QuadraticSymmetric E)]
  (ν : MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E))
  [ν.IsAddHaarMeasure] (g : E ≃ᵃ[ℝ] E) :
  MeasureTheory.Measure.map (fun ξ ↦ g⁻¹ • ξ) ν =
    ν.withDensity fun ξ ↦ ↑(LeanRidgelet.quadraticParameterJacobian g ξ)

theorem LeanRidgelet.quadraticParameter_group_map_eq_withDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  (ν :
    MeasureTheory.Measure
      (LeanRidgelet.QuadraticParameter E))
  [ν.IsAddHaarMeasure] (g : E ≃ᵃ[ℝ] E) :
  MeasureTheory.Measure.map
      (fun ξ ↦ g⁻¹ • ξ) ν =
    ν.withDensity fun ξ ↦
      ↑(LeanRidgelet.quadraticParameterJacobian
          g ξ)

The parameter pushforward formula expressed through the affine-group action instance.  This is
the strong quasi-invariance hypothesis of the generic `L²` construction.

defdefined in LeanRidgelet/HA/QuadraticMeasure.lean

complete

def LeanRidgelet.quadraticParameterLpUnitaryRepresentation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace (LeanRidgelet.QuadraticSymmetric E)]
  (ν : MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E))
  [ν.IsAddHaarMeasure] [MeasureTheory.SigmaFinite ν] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E) ↥(MeasureTheory.Lp ℂ 2 ν)

def LeanRidgelet.quadraticParameterLpUnitaryRepresentation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  (ν :
    MeasureTheory.Measure
      (LeanRidgelet.QuadraticParameter E))
  [ν.IsAddHaarMeasure]
  [MeasureTheory.SigmaFinite ν] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E)
    ↥(MeasureTheory.Lp ℂ 2 ν)

Implementation after :=

:=
  quasiInvariantLpUnitaryRepresentation quadraticParameterJacobian
    quadraticParameter_measurable (quadraticParameter_group_map_eq_withDensity ν)
    quadraticParameterJacobian_measurable quadraticParameterJacobian_ne_zero
    quadraticParameterJacobian_one quadraticParameterJacobian_cocycle

The Radon--Nikodym-corrected quadratic parameter representation on scalar `L²`.

defdefined in LeanRidgelet/HA/QuadraticRelativeMeasure.lean

complete

def LeanRidgelet.quadraticRelativeMeasure.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E]
  [MeasurableSpace (LeanRidgelet.QuadraticSymmetric E)]
  (lam : MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E)) :
  MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E)

def LeanRidgelet.quadraticRelativeMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E]
  [MeasurableSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  (lam :
    MeasureTheory.Measure
      (LeanRidgelet.QuadraticParameter
        E)) :
  MeasureTheory.Measure
    (LeanRidgelet.QuadraticParameter E)

Implementation after :=

:=
  (lam.restrict (quadraticNondegenerate E)).withDensity quadraticRelativeWeight

**The relatively invariant parameter measure.**  An additive Haar measure `lam` on the
quadratic parameter space, restricted to the nondegenerate locus and weighted by
`LeanRidgelet.quadraticRelativeWeight`.  It is σ-finite but, for `m ≥ 1`, not locally finite; see
the module docstring.

defdefined in LeanRidgelet/HA/QuadraticRelativeMeasure.lean

complete

def LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace (LeanRidgelet.QuadraticSymmetric E)]
  (lam : MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E))
  [lam.IsAddHaarMeasure] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E)
    ↥(MeasureTheory.Lp ℂ 2 (LeanRidgelet.quadraticRelativeMeasure lam))

def LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  (lam :
    MeasureTheory.Measure
      (LeanRidgelet.QuadraticParameter E))
  [lam.IsAddHaarMeasure] :
  UnitaryRepresentation (E ≃ᵃ[ℝ] E)
    ↥(MeasureTheory.Lp ℂ 2
        (LeanRidgelet.quadraticRelativeMeasure
          lam))

Implementation after :=

:=
  quasiInvariantLpUnitaryRepresentation quadraticRelativeParameterJacobian
    quadraticParameter_measurable
    (quadraticRelativeParameter_group_map_eq_withDensity lam)
    quadraticRelativeParameterJacobian_measurable quadraticRelativeParameterJacobian_ne_zero
    quadraticRelativeParameterJacobian_one quadraticRelativeParameterJacobian_cocycle

The Radon--Nikodym-corrected quadratic parameter representation on scalar `L²`, built from the
relatively invariant measure.  Compare `LeanRidgelet.quadraticParameterLpUnitaryRepresentation`,
which uses the Haar measure and therefore a different, unbalanced, cocycle.

theoremdefined in LeanRidgelet/HA/QuadraticRelativeMeasure.lean

complete

theorem LeanRidgelet.quadraticRelativeBochnerSynthesis_intertwines.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace (LeanRidgelet.QuadraticSymmetric E)] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (lam : MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E))
  [lam.IsAddHaarMeasure] (σ : ℝ → Y) (g : E ≃ᵃ[ℝ] E)
  (γ : LeanRidgelet.QuadraticParameter E → ℂ) (x : E) :
  LeanRidgelet.bochnerSynthesis
      (LeanRidgelet.quadraticRelativeMeasure lam)
      (LeanRidgelet.quadraticVectorFeature σ)
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          LeanRidgelet.quadraticRelativeParameterJacobian)
        g γ)
      x =
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      (LeanRidgelet.bochnerSynthesis
        (LeanRidgelet.quadraticRelativeMeasure lam)
        (LeanRidgelet.quadraticVectorFeature σ) γ)
      x

theorem LeanRidgelet.quadraticRelativeBochnerSynthesis_intertwines.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (lam :
    MeasureTheory.Measure
      (LeanRidgelet.QuadraticParameter E))
  [lam.IsAddHaarMeasure] (σ : ℝ → Y)
  (g : E ≃ᵃ[ℝ] E)
  (γ :
    LeanRidgelet.QuadraticParameter E → ℂ)
  (x : E) :
  LeanRidgelet.bochnerSynthesis
      (LeanRidgelet.quadraticRelativeMeasure
        lam)
      (LeanRidgelet.quadraticVectorFeature
        σ)
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          LeanRidgelet.quadraticRelativeParameterJacobian)
        g γ)
      x =
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      (LeanRidgelet.bochnerSynthesis
        (LeanRidgelet.quadraticRelativeMeasure
          lam)
        (LeanRidgelet.quadraticVectorFeature
          σ)
        γ)
      x

**The payoff, synthesis half.**  The untwisted quasi-invariant Bochner synthesis identity for
the quadratic feature, available because the relatively invariant parameter measure balances the
data measure exactly.  Compare `LeanRidgelet.affineBochnerSynthesis_intertwines`.

theoremdefined in LeanRidgelet/HA/QuadraticRelativeMeasure.lean

complete

theorem LeanRidgelet.quadraticRelativeBochnerRidgelet_intertwines.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  (ψ : ℝ → Y) (g : E ≃ᵃ[ℝ] E) (f : E → Y)
  (ξ : LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.bochnerRidgelet μ (LeanRidgelet.quadraticVectorFeature ψ)
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1 g f)
      ξ =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.quadraticRelativeParameterJacobian)
      g
      (LeanRidgelet.bochnerRidgelet μ
        (LeanRidgelet.quadraticVectorFeature ψ) f)
      ξ

theorem LeanRidgelet.quadraticRelativeBochnerRidgelet_intertwines.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (ψ : ℝ → Y)
  (g : E ≃ᵃ[ℝ] E) (f : E → Y)
  (ξ :
    LeanRidgelet.QuadraticParameter E) :
  LeanRidgelet.bochnerRidgelet μ
      (LeanRidgelet.quadraticVectorFeature
        ψ)
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1
        g f)
      ξ =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.quadraticRelativeParameterJacobian)
      g
      (LeanRidgelet.bochnerRidgelet μ
        (LeanRidgelet.quadraticVectorFeature
          ψ)
        f)
      ξ

**The payoff, ridgelet half.**  The untwisted quasi-invariant Bochner ridgelet identity for the
quadratic feature.  Only the data measure enters, so this half needs neither the parameter measure
nor the congruence-determinant hypothesis; what it needs is the parameter Jacobian of the
relatively invariant measure, through the balance
`LeanRidgelet.quadraticRelative_ridgelet_radonNikodym_balance`.  Compare
`LeanRidgelet.affineBochnerRidgelet_intertwines`.

theoremdefined in LeanRidgelet/HA/QuadraticReconstruction.lean

complete

theorem LeanRidgelet.quadratic_reconstruction.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [Nontrivial E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace (LeanRidgelet.QuadraticSymmetric E)]
  (lam : MeasureTheory.Measure (LeanRidgelet.QuadraticParameter E))
  [lam.IsAddHaarMeasure]
  (M :
    LeanRidgelet.JointEquivariantMachine
      (LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation
          lam).toContRepresentation
      (LeanRidgelet.affineDataLpUnitaryRepresentation
          MeasureTheory.volume).toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      (LeanRidgelet.affineDataLpUnitaryRepresentation
          MeasureTheory.volume).toContRepresentation
      (LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation
          lam).toContRepresentation) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator M R =
        c •
          ContinuousLinearMap.id ℂ
            ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) ∧
      (c ≠ 0 →
        Function.RightInverse ⇑(c⁻¹ • R.toContinuousLinearMap) ⇑M)

theorem LeanRidgelet.quadratic_reconstruction.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  [BorelSpace
      (LeanRidgelet.QuadraticSymmetric E)]
  (lam :
    MeasureTheory.Measure
      (LeanRidgelet.QuadraticParameter E))
  [lam.IsAddHaarMeasure]
  (M :
    LeanRidgelet.JointEquivariantMachine
      (LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation
          lam).toContRepresentation
      (LeanRidgelet.affineDataLpUnitaryRepresentation
          MeasureTheory.volume).toContRepresentation)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      (LeanRidgelet.affineDataLpUnitaryRepresentation
          MeasureTheory.volume).toContRepresentation
      (LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation
          lam).toContRepresentation) :
  ∃ c,
    LeanRidgelet.jointReconstructionOperator
          M R =
        c •
          ContinuousLinearMap.id ℂ
            ↥(MeasureTheory.Lp ℂ 2
                MeasureTheory.volume) ∧
      (c ≠ 0 →
        Function.RightInverse
          ⇑(c⁻¹ • R.toContinuousLinearMap)
          ⇑M)

Section 7 of the article: the quadratic-form network reconstructs the data space.  The
reconstruction operator is a scalar, and a nonzero scalar turns the normalized quadratic ridgelet
transform into a right inverse of the quadratic machine.

Section 8 discusses scope and consequences and adds no numbered formal target.

Appendices A--E

Lemma4.1.23

uses 1used by 0✓L∃∀N

Lemmas A.1 and A.2. The invariant and strongly quasi-invariant L^2 constructions supply the unitary representations used in the main text.

Lean code for Lemma4.1.23●2 definitions

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.invariantLpUnitaryRepresentation.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SMulInvariantMeasure G X μ] [MeasurableConstSMul G X] :
  UnitaryRepresentation G ↥(MeasureTheory.Lp E 2 μ)

def LeanRidgelet.invariantLpUnitaryRepresentation.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SMulInvariantMeasure G X
      μ]
  [MeasurableConstSMul G X] :
  UnitaryRepresentation G
    ↥(MeasureTheory.Lp E 2 μ)

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    { toFun := fun g ↦ invariantLpLinearIsometryEquiv (toDomMulActInv g)
      map_one' := by
        apply LinearIsometryEquiv.ext
        intro f
        simp [toDomMulActInv]
      map_mul' := by
        intro g h
        apply LinearIsometryEquiv.ext
        intro f
        simp [toDomMulActInv, mul_smul] }

An invariant measurable action induces a unitary representation on Bochner `L²`.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.quasiInvariantLpUnitaryRepresentation.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero : ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (h_one : ∀ (x : X), jacobian 1 x = 1)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x = jacobian g (h • x) * jacobian h x) :
  UnitaryRepresentation G ↥(MeasureTheory.Lp E 2 μ)

def LeanRidgelet.quasiInvariantLpUnitaryRepresentation.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero :
    ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (h_one : ∀ (x : X), jacobian 1 x = 1)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x =
        jacobian g (h • x) *
          jacobian h x) :
  UnitaryRepresentation G
    ↥(MeasureTheory.Lp E 2 μ)

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    (quasiInvariantLpLinearIsometryEquivMonoidHom jacobian h_measurable h_map h_jacobian
      h_ne_zero h_one h_cocycle)

A strongly quasi-invariant measure with a measurable positive Radon--Nikodym cocycle induces
Folland's unitary representation on Bochner `L²`.

Lemma4.1.24

uses 1used by 0✓L∃∀N

Lemma A.3. The finite-dimensional-output case needed in Section 5 is proved directly on Bochner L^2. A general completed-Hilbert-tensor theorem remains optional upstream work.

Lean code for Lemma4.1.24●1 theorem

theoremdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

theorem LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of.{u_1,
    u_2, u_3}
  {G : Type u_1} {E : Type u_2} {Y : Type u_3} [Group G]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [FiniteDimensional ℂ Y]
  (υ : UnitaryRepresentation G Y) (hυ : υ.IsTopologicallyIrreducible)
  (hAffine :
    (LeanRidgelet.affineDataLpUnitaryRepresentation
        MeasureTheory.volume).IsTopologicallyIrreducible) :
  (LeanRidgelet.fullyConnectedLpUnitaryRepresentation
      υ).IsTopologicallyIrreducible

theorem LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of.{u_1,
    u_2, u_3}
  {G : Type u_1} {E : Type u_2}
  {Y : Type u_3} [Group G]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [FiniteDimensional ℂ Y]
  (υ : UnitaryRepresentation G Y)
  (hυ : υ.IsTopologicallyIrreducible)
  (hAffine :
    (LeanRidgelet.affineDataLpUnitaryRepresentation
        MeasureTheory.volume).IsTopologicallyIrreducible) :
  (LeanRidgelet.fullyConnectedLpUnitaryRepresentation
      υ).IsTopologicallyIrreducible

The finite-output Bochner-`L²` form of Folland Theorem 7.12 needed in Section 5:
irreducibility of the value representation and of the scalar affine representation implies
irreducibility of their commuting product on `L²(E;Y)`.

The proof uses the finite-coordinate version in `ToMathlib.LieGroup.UnitaryLp`.  Naturality of
the affine pullback with respect to coordinate embeddings and projections replaces the unavailable
completed-Hilbert-tensor identification.

Lemma4.1.25

uses 1used by 0✓L∃∀N

Lemmas A.4 and A.5. Synthesis is the orbit lift of base synthesis, and the identity-component ridgelet is the base ridgelet.

Lean code for Lemma4.1.25●2 theorems

theoremdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

theorem LeanRidgelet.groupConvolutionalSynthesis_eq_orbit.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MeasurableSpace Ξ] [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ) (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (γ : Ξ → ℂ) (x : X) (g : G) :
  LeanRidgelet.groupConvolutionalSynthesis μ υ φ γ x g =
    ↑(υ g) (LeanRidgelet.bochnerSynthesis μ φ γ (g⁻¹ • x))

theorem LeanRidgelet.groupConvolutionalSynthesis_eq_orbit.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (γ : Ξ → ℂ) (x : X)
  (g : G) :
  LeanRidgelet.groupConvolutionalSynthesis
      μ υ φ γ x g =
    ↑(υ g)
      (LeanRidgelet.bochnerSynthesis μ φ γ
        (g⁻¹ • x))

Appendix A.4: GCN synthesis is the orbit lift of the base synthesis.

theoremdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

theorem LeanRidgelet.groupConvolutionalRidgelet_eq_base.{u_1, u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MeasurableSpace X] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (μ : MeasureTheory.Measure X) (ψ : X → Ξ → Y) (f : X → G → Y) :
  LeanRidgelet.groupConvolutionalRidgelet μ ψ f =
    LeanRidgelet.bochnerRidgelet μ ψ fun x ↦ f x 1

theorem LeanRidgelet.groupConvolutionalRidgelet_eq_base.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (μ : MeasureTheory.Measure X)
  (ψ : X → Ξ → Y) (f : X → G → Y) :
  LeanRidgelet.groupConvolutionalRidgelet
      μ ψ f =
    LeanRidgelet.bochnerRidgelet μ ψ
      fun x ↦ f x 1

Appendix A.5: the convolutional ridgelet is definitionally the base ridgelet at `1_G`.

Definition4.1.26

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0XL∃∀N

Appendix B. The depth-two fully-connected example expands the definitions and reconstruction calculation used in Section 2; the comparison of Theorem 2.3 above now covers it at homogeneity index zero.

Lemma4.1.27

uses 0used by 1XL∃∀N

Lemmas C.1--C.3. Mathlib's Bochner integrability and dominated/bounded convergence results will be cited directly rather than restated.

Theorem4.1.28

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.12

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0XL∃∀N

Theorem C.4. Uniform approximation of a compactly supported Bochner integral by finite networks remains to be formalized with a valid bounded-continuous or compact-domain norm.

Lemma4.1.29

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.12

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0XL∃∀N

Lemmas D.1 and D.2. The remaining Hilbert--Schmidt-type boundedness criteria are deferred. The Euclidean network needed in the main examples already uses the stronger existing L2 theory.

Theorem4.1.30

uses 1used by 0XL∃∀N

Lemma E.1 and Theorem E.2. Their affine irreducibility conclusion is reached through the Mackey model above. The approximate identity, invariant-subspace convergence, compact-kernel convolution continuity, quotient cutoff, and density needed by Folland 6.29 are formalized, together with the measurable lift, the slice integrability of its smoothing integrand, and the convolution formula that complete the lemma, as is the exact 6.30 inducing-fiber correspondence.