4.4. Harmonic-analysis method: reconstruction and architectures🔗

Once the intertwining operators of the representation layer are available, the reconstruction theorem is a short Schur argument, and every architecture of the article whose parameter space is a copy of the data space is an instance of it. This chapter covers the commutant reduction and the normalized right inverse, the finite cascade, the fully-connected and group-convolutional networks, the reuse of the existing L^2 operator layer, the comparison with the classical transforms, and the analytic comparisons that remain. Section 7, whose parameter space is the space of symmetric coefficients, has its own chapter.

Intertwiners and the commutant

Definition4.4.1

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 4.4.2

Loading preview

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

✓L∃∀N

Bounded operator API. Synthesis and ridgelet transforms are continuous intertwining maps in opposite directions. The preceding constructors supply values of these types once bounded maps with the displayed coordinate formulas have been proved.

Lean code for Definition4.4.1●2 definitions

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.

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.4.2

uses 1used by 1✓L∃∀N

Composition. The composite of the two intertwiners is a bounded endomorphism of the data space, and the intertwining laws prove that it commutes with every represented group element.

Lean code for Lemma4.4.2●3 declarations

defdefined in LeanRidgelet/HA/Operators.lean

complete

def LeanRidgelet.jointReconstructionOperator.{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}
  (M : LeanRidgelet.JointEquivariantMachine πParameter πData)
  (R : LeanRidgelet.JointEquivariantRidgelet πData πParameter) :
  H →L[ℂ] H

def LeanRidgelet.jointReconstructionOperator.{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}
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter πData)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData πParameter) :
  H →L[ℂ] H

Implementation after :=

:=
  (M.comp R).toContinuousLinearMap

The reconstruction operator `M_φ R_ψ`.

theoremdefined in LeanRidgelet/HA/Operators.lean

complete

theorem LeanRidgelet.jointReconstructionOperator_apply.{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}
  (M : LeanRidgelet.JointEquivariantMachine πParameter πData)
  (R : LeanRidgelet.JointEquivariantRidgelet πData πParameter) (f : H) :
  (LeanRidgelet.jointReconstructionOperator M R) f = M (R f)

theorem LeanRidgelet.jointReconstructionOperator_apply.{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}
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter πData)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData πParameter)
  (f : H) :
  (LeanRidgelet.jointReconstructionOperator
        M R)
      f =
    M (R f)

theoremdefined in LeanRidgelet/HA/Operators.lean

complete

theorem LeanRidgelet.jointReconstructionOperator_commutes.{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}
  (M : LeanRidgelet.JointEquivariantMachine πParameter πData)
  (R : LeanRidgelet.JointEquivariantRidgelet πData πParameter) (g : G) :
  LeanRidgelet.jointReconstructionOperator M R ∘SL πData g =
    πData g ∘SL LeanRidgelet.jointReconstructionOperator M R

theorem LeanRidgelet.jointReconstructionOperator_commutes.{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}
  (M :
    LeanRidgelet.JointEquivariantMachine
      πParameter πData)
  (R :
    LeanRidgelet.JointEquivariantRidgelet
      πData πParameter)
  (g : G) :
  LeanRidgelet.jointReconstructionOperator
        M R ∘SL
      πData g =
    πData g ∘SL
      LeanRidgelet.jointReconstructionOperator
        M R

Lemmas 3.7 and 3.9 imply that `M_φ R_ψ` commutes with the data representation.

Theorem4.4.3

Statement uses 2

Statement dependency previews

Preview

Theorem 4.2.2

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 4.4.4

Loading preview

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

✓L∃∀N

Schur reduction and normalization. The theorem with HasSchurProperty as an explicit hypothesis is proved without placeholders, for both an arbitrary bounded endomorphism intertwiner and a composition of two bounded intertwiners. The topological-irreducibility endpoints are derived from the Schur declaration, and a nonzero scalar gives the normalized ridgelet right inverse by linearity.

Lean code for Theorem4.4.3●5 theorems

theoremdefined in LeanRidgelet/HA/Reconstruction.lean

complete

theorem LeanRidgelet.ha_reconstruction_of_hasSchurProperty_of_intertwiner.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (πData : UnitaryRepresentation G H) (hschur : πData.HasSchurProperty)
  (T :
    LeanRidgelet.JointEquivariantMachine πData.toContRepresentation
      πData.toContRepresentation) :
  ∃ c, T.toContinuousLinearMap = c • ContinuousLinearMap.id ℂ H

theorem LeanRidgelet.ha_reconstruction_of_hasSchurProperty_of_intertwiner.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (πData : UnitaryRepresentation G H)
  (hschur : πData.HasSchurProperty)
  (T :
    LeanRidgelet.JointEquivariantMachine
      πData.toContRepresentation
      πData.toContRepresentation) :
  ∃ c,
    T.toContinuousLinearMap =
      c • ContinuousLinearMap.id ℂ H

A bounded endomorphism already bundled as an intertwiner is scalar under the Schur property.
This form is used when only the composite pointwise synthesis/ridgelet formula has a bounded
extension, without assuming boundedness of the two integral operators separately.

theoremdefined in LeanRidgelet/HA/Reconstruction.lean

complete

theorem LeanRidgelet.ha_reconstruction_of_intertwiner.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (πData : UnitaryRepresentation G H)
  (hirr : πData.IsTopologicallyIrreducible)
  (T :
    LeanRidgelet.JointEquivariantMachine πData.toContRepresentation
      πData.toContRepresentation) :
  ∃ c, T.toContinuousLinearMap = c • ContinuousLinearMap.id ℂ H

theorem LeanRidgelet.ha_reconstruction_of_intertwiner.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (πData : UnitaryRepresentation G H)
  (hirr :
    πData.IsTopologicallyIrreducible)
  (T :
    LeanRidgelet.JointEquivariantMachine
      πData.toContRepresentation
      πData.toContRepresentation) :
  ∃ c,
    T.toContinuousLinearMap =
      c • ContinuousLinearMap.id ℂ H

Topological irreducibility makes every bounded intertwining endomorphism scalar.

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.

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.

Architectures after the abstract reconstruction theorem

Theorem4.4.4

Statement uses 2

Statement dependency previews

Preview

Definition 4.4.1

Loading preview

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

used by 0✓L∃∀N

Reconstruction from the adjoint. Take the machine to be the adjoint of the ridgelet transform. Then the composite is positive, Schur makes it a scalar, and the scalar is \|Rf\|^2/\|f\|^2 — real, nonnegative, and nonzero as soon as the transform is. One datum with nonzero transform gives the reconstruction formula outright.

Lean code for Theorem4.4.4●9 declarations

theoremdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

theorem LeanRidgelet.UnitaryRepresentation.adjoint_coe.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) (g : G) :
  ContinuousLinearMap.adjoint ↑(π g) = ↑(π g⁻¹)

theorem LeanRidgelet.UnitaryRepresentation.adjoint_coe.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H)
  (g : G) :
  ContinuousLinearMap.adjoint ↑(π g) =
    ↑(π g⁻¹)

The adjoint of a unitary representation's operator is the operator at the inverse group element.
This is `star = adjoint` for continuous linear endomorphisms together with `star = inverse` in the
unitary group.

defdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

def LeanRidgelet.adjointIntertwiner.{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]
  [InnerProductSpace ℂ K] [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H} {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap π₁.toContRepresentation
      π₂.toContRepresentation) :
  ContIntertwiningMap π₂.toContRepresentation π₁.toContRepresentation

def LeanRidgelet.adjointIntertwiner.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H}
  {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      π₁.toContRepresentation
      π₂.toContRepresentation) :
  ContIntertwiningMap
    π₂.toContRepresentation
    π₁.toContRepresentation

Implementation after :=

:= ContinuousLinearMap.adjoint R.toContinuousLinearMap
  isIntertwining' g := by
    have h := congrArg ContinuousLinearMap.adjoint (R.isIntertwining' g⁻¹)
    simp only [UnitaryRepresentation.toContRepresentation_apply, ContinuousLinearMap.adjoint_comp,
      UnitaryRepresentation.adjoint_coe, inv_inv] at h
    simpa only [UnitaryRepresentation.toContRepresentation_apply] using h.symm

**The adjoint of an intertwiner is an intertwiner.**  Taking adjoints in the intertwining law
exchanges the two representations and replaces the group element by its inverse, and a group element
ranges over the whole group with its inverse.

theoremdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

theorem LeanRidgelet.adjointIntertwiner_toContinuousLinearMap.{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] [InnerProductSpace ℂ K] [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H} {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap π₁.toContRepresentation
      π₂.toContRepresentation) :
  (LeanRidgelet.adjointIntertwiner R).toContinuousLinearMap =
    ContinuousLinearMap.adjoint R.toContinuousLinearMap

theorem LeanRidgelet.adjointIntertwiner_toContinuousLinearMap.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H}
  {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      π₁.toContRepresentation
      π₂.toContRepresentation) :
  (LeanRidgelet.adjointIntertwiner
        R).toContinuousLinearMap =
    ContinuousLinearMap.adjoint
      R.toContinuousLinearMap

defdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

def LeanRidgelet.adjointReconstructionOperator.{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] [InnerProductSpace ℂ K] [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H} {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap π₁.toContRepresentation
      π₂.toContRepresentation) :
  ContIntertwiningMap π₁.toContRepresentation π₁.toContRepresentation

def LeanRidgelet.adjointReconstructionOperator.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H}
  {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      π₁.toContRepresentation
      π₂.toContRepresentation) :
  ContIntertwiningMap
    π₁.toContRepresentation
    π₁.toContRepresentation

Implementation after :=

:=
  (adjointIntertwiner R).comp R

**The reconstruction operator of the coorbit route.**  The composite of a bounded intertwiner
with
its own adjoint, as an intertwining endomorphism of the data representation.

theoremdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

theorem LeanRidgelet.adjointReconstructionOperator_apply.{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] [InnerProductSpace ℂ K] [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H} {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap π₁.toContRepresentation π₂.toContRepresentation)
  (f : H) :
  (LeanRidgelet.adjointReconstructionOperator R) f =
    (ContinuousLinearMap.adjoint R.toContinuousLinearMap) (R f)

theorem LeanRidgelet.adjointReconstructionOperator_apply.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H}
  {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      π₁.toContRepresentation
      π₂.toContRepresentation)
  (f : H) :
  (LeanRidgelet.adjointReconstructionOperator
        R)
      f =
    (ContinuousLinearMap.adjoint
        R.toContinuousLinearMap)
      (R f)

The reconstruction operator applied to a datum is the adjoint of the transform of the datum.

theoremdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

theorem LeanRidgelet.inner_adjointReconstructionOperator.{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] [InnerProductSpace ℂ K] [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H} {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap π₁.toContRepresentation π₂.toContRepresentation)
  (f : H) :
  inner ℂ ((LeanRidgelet.adjointReconstructionOperator R) f) f =
    inner ℂ (R f) (R f)

theorem LeanRidgelet.inner_adjointReconstructionOperator.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  {π₁ : UnitaryRepresentation G H}
  {π₂ : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      π₁.toContRepresentation
      π₂.toContRepresentation)
  (f : H) :
  inner ℂ
      ((LeanRidgelet.adjointReconstructionOperator
          R)
        f)
      f =
    inner ℂ (R f) (R f)

**Positivity.**  Pairing the reconstruction operator with a datum gives the squared norm of the
datum's transform.  This is what makes the reconstruction constant real, nonnegative, and nonzero
exactly when the transform is.

theoremdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

theorem LeanRidgelet.ha_adjoint_reconstruction.{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]
  [InnerProductSpace ℂ K] [CompleteSpace K]
  (πData : UnitaryRepresentation G H)
  (hirr : πData.IsTopologicallyIrreducible)
  {πParam : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap πData.toContRepresentation
      πParam.toContRepresentation) :
  ∃ c,
    (LeanRidgelet.adjointReconstructionOperator
            R).toContinuousLinearMap =
        c • ContinuousLinearMap.id ℂ H ∧
      ∀ (f : H), inner ℂ (R f) (R f) = c * inner ℂ f f

theorem LeanRidgelet.ha_adjoint_reconstruction.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (πData : UnitaryRepresentation G H)
  (hirr :
    πData.IsTopologicallyIrreducible)
  {πParam : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      πData.toContRepresentation
      πParam.toContRepresentation) :
  ∃ c,
    (LeanRidgelet.adjointReconstructionOperator
            R).toContinuousLinearMap =
        c • ContinuousLinearMap.id ℂ H ∧
      ∀ (f : H),
        inner ℂ (R f) (R f) =
          c * inner ℂ f f

**The orthogonality relation from Schur's lemma.**  For a bounded intertwiner into any unitary
representation of the same group, the composite with its adjoint is a scalar multiple of the
identity,
and the scalar satisfies `⟪R f, R f⟫ = c ⟪f, f⟫` for every datum.  The second statement exhibits the
scalar as `‖R f‖² / ‖f‖²`: it is real and nonnegative, with no positivity argument beyond that
identity.

In coorbit theory this relation is supplied by the Duflo--Moore theorem for a square-integrable
representation; here it comes from irreducibility of the data representation alone, so neither
square
integrability nor an admissible vector is assumed.

theoremdefined in LeanRidgelet/HA/AdjointReconstruction.lean

complete

theorem LeanRidgelet.ha_adjoint_reconstruction_of_ne_zero.{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] [InnerProductSpace ℂ K] [CompleteSpace K]
  (πData : UnitaryRepresentation G H)
  (hirr : πData.IsTopologicallyIrreducible)
  {πParam : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap πData.toContRepresentation
      πParam.toContRepresentation)
  (f₀ : H) (hf₀ : R f₀ ≠ 0) :
  ∃ c,
    c ≠ 0 ∧
      (LeanRidgelet.adjointReconstructionOperator
              R).toContinuousLinearMap =
          c • ContinuousLinearMap.id ℂ H ∧
        (∀ (f : H), inner ℂ (R f) (R f) = c * inner ℂ f f) ∧
          ∀ (f : H),
            c⁻¹ •
                (ContinuousLinearMap.adjoint R.toContinuousLinearMap)
                  (R f) =
              f

theorem LeanRidgelet.ha_adjoint_reconstruction_of_ne_zero.{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]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (πData : UnitaryRepresentation G H)
  (hirr :
    πData.IsTopologicallyIrreducible)
  {πParam : UnitaryRepresentation G K}
  (R :
    ContIntertwiningMap
      πData.toContRepresentation
      πParam.toContRepresentation)
  (f₀ : H) (hf₀ : R f₀ ≠ 0) :
  ∃ c,
    c ≠ 0 ∧
      (LeanRidgelet.adjointReconstructionOperator
              R).toContinuousLinearMap =
          c • ContinuousLinearMap.id ℂ H ∧
        (∀ (f : H),
            inner ℂ (R f) (R f) =
              c * inner ℂ f f) ∧
          ∀ (f : H),
            c⁻¹ •
                (ContinuousLinearMap.adjoint
                    R.toContinuousLinearMap)
                  (R f) =
              f

**A nonzero reconstruction constant, and the reconstruction formula.**  If one datum has nonzero
transform then the constant is nonzero, and the normalized adjoint of the ridgelet transform returns
every datum.  This is the reconstruction formula of coorbit theory -- Corollary 2.34 of Berge's
primer
-- with Schur's lemma in place of the Duflo--Moore orthogonality relation.

The only hypotheses are that the ridgelet transform is a bounded intertwiner and that it does not
annihilate everything.  Nothing is assumed about the synthesis operator, which is the adjoint;
nothing
is assumed about kernels or their square integrability, which is why the compactness obstruction of
`LeanRidgelet.HA.QuadraticComposite` does not arise.

theoremdefined in LeanRidgelet/HA/BochnerAdjoint.lean

complete

theorem LeanRidgelet.bochnerSynthesis_eq_adjoint_bochnerRidgelet.{u_1, u_2}
  {X : Type u_1} {Ξ : Type u_2} [MeasurableSpace X] [MeasurableSpace Ξ]
  (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ]
  (ν : MeasureTheory.Measure Ξ) [MeasureTheory.SFinite ν]
  (φ : X → Ξ → ℂ)
  (M : ↥(MeasureTheory.Lp ℂ 2 ν) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ))
  (R : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 ν))
  (hM :
    ∀ (γ : ↥(MeasureTheory.Lp ℂ 2 ν)),
      ↑↑(M γ) =ᵐ[μ] LeanRidgelet.bochnerSynthesis ν φ ↑↑γ)
  (hR :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      ↑↑(R f) =ᵐ[ν] LeanRidgelet.bochnerRidgelet μ φ ↑↑f)
  (hfub :
    ∀ (γ : ↥(MeasureTheory.Lp ℂ 2 ν)) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.Integrable
        (Function.uncurry fun x ξ ↦
          (starRingEnd ℂ) (↑↑γ ξ) * ((starRingEnd ℂ) (φ x ξ) * ↑↑f x))
        (μ.prod ν)) :
  M = ContinuousLinearMap.adjoint R

theorem LeanRidgelet.bochnerSynthesis_eq_adjoint_bochnerRidgelet.{u_1,
    u_2}
  {X : Type u_1} {Ξ : Type u_2}
  [MeasurableSpace X] [MeasurableSpace Ξ]
  (μ : MeasureTheory.Measure X)
  [MeasureTheory.SFinite μ]
  (ν : MeasureTheory.Measure Ξ)
  [MeasureTheory.SFinite ν]
  (φ : X → Ξ → ℂ)
  (M :
    ↥(MeasureTheory.Lp ℂ 2 ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (R :
    ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 ν))
  (hM :
    ∀ (γ : ↥(MeasureTheory.Lp ℂ 2 ν)),
      ↑↑(M γ) =ᵐ[μ]
        LeanRidgelet.bochnerSynthesis ν φ
          ↑↑γ)
  (hR :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      ↑↑(R f) =ᵐ[ν]
        LeanRidgelet.bochnerRidgelet μ φ
          ↑↑f)
  (hfub :
    ∀ (γ : ↥(MeasureTheory.Lp ℂ 2 ν))
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.Integrable
        (Function.uncurry fun x ξ ↦
          (starRingEnd ℂ) (↑↑γ ξ) *
            ((starRingEnd ℂ) (φ x ξ) *
              ↑↑f x))
        (μ.prod ν)) :
  M = ContinuousLinearMap.adjoint R

**The synthesis integral is the adjoint of the ridgelet transform, for a common feature.**  If a
bounded operator realizes the Bochner synthesis integral against a feature and another realizes the
Bochner ridgelet transform against the *same* feature, the first is the adjoint of the second.

The proof pairs each side against arbitrary vectors and exchanges the order of integration: both
pairings are the double integral of `conj (γ ξ) conj (φ x ξ) f x`, one taken parameter-first and the
other data-first.

This is how coorbit theory and the theory of generalized wavelet transforms get their reconstruction formula, and it dissolves the compactness obstruction recorded below rather than working around it. That obstruction came from treating the synthesis and the analysis as independent integral operators, each with its own square-integrable kernel; here there is no independent synthesis operator, so no kernel is assumed square integrable, and a composite equal to a nonzero multiple of the identity makes the transform a multiple of an isometry, which in infinite dimensions is simply not compact.

Three facts carry it. The adjoint of an intertwiner of unitary representations is an intertwiner the other way — take adjoints in the intertwining law and the group element inverts, which costs nothing since a group element ranges over the group with its inverse. Pairing the composite with a datum gives the squared norm of the datum's transform, which is what makes the scalar real and nonnegative. And Schur applies to the composite because it is an intertwining endomorphism of the data representation, whose topological irreducibility is proved in this development.

In the notation of Berge's A Primer on Coorbit Theory (arXiv:2101.05232), the analysis operator is the wavelet transform \mathcal{W}_g f(x)=\langle f,\pi(x)g\rangle, its adjoint is the weak integral \mathcal{W}_g^*(F)=\int F(x)\pi(x)g\,dx of Proposition 2.33 there, and the reconstruction formula is Corollary 2.34. What supplies the constant there is the Duflo--Moore orthogonality relation for a square-integrable representation; here Schur's lemma supplies it, so neither square integrability of the representation nor an admissible vector is assumed.

The cost is that the machine is the adjoint rather than an independently chosen synthesis integral, and the identification that makes it precise is also proved here: for a single feature the Bochner synthesis integral and the Bochner ridgelet transform are adjoint to each other, by one exchange of the order of integration — both pairings are the double integral of \overline{\gamma(\xi)}\,\overline{\varphi(x,\xi)}\,f(x), one taken parameter-first and the other data-first. So the abstract adjoint is the network's own synthesis integral, provided the synthesis feature is the analysis feature. With a different synthesis feature the two are not adjoint, which is the precise sense in which this route reconstructs with the network whose activation is the analysis feature. Fixing the activation in advance is the harder problem, and it is the one the boundedness appendix is about.

Lemma4.4.5

Statement uses 2

Statement dependency previews

Preview

Lemma 4.2.4

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Definition 4.4.6

Loading preview

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

✓L∃∀N

Finite heterogeneous cascades. A snoc-indexed dependent tuple stores exactly one parameter per layer while allowing every intermediate type to change. Its componentwise group action is a MulAction; induction lifts binary joint equivariance to the full cascade. Corollary 4.1 then reuses the abstract bounded-intertwiner reconstruction and normalization results.

Lean code for Lemma4.4.5●10 declarations

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.DeepParameters.smul.{u_1, u_2} {G : Type u_1}
  {Ξ : ℕ → Type u_2} [(i : ℕ) → SMul G (Ξ i)] (g : G) {n : ℕ} :
  LeanRidgelet.DeepParameters Ξ n → LeanRidgelet.DeepParameters Ξ n

def LeanRidgelet.DeepParameters.smul.{u_1,
    u_2}
  {G : Type u_1} {Ξ : ℕ → Type u_2}
  [(i : ℕ) → SMul G (Ξ i)] (g : G)
  {n : ℕ} :
  LeanRidgelet.DeepParameters Ξ n →
    LeanRidgelet.DeepParameters Ξ n

Componentwise scalar multiplication on a heterogeneous parameter tuple.

theoremdefined in LeanRidgelet/HA/Deep.lean

complete

theorem LeanRidgelet.DeepParameters.smul_nil.{u_1, u_2} {G : Type u_1}
  {Ξ : ℕ → Type u_2} [(i : ℕ) → SMul G (Ξ i)] (g : G) :
  g • LeanRidgelet.DeepParameters.nil = LeanRidgelet.DeepParameters.nil

theorem LeanRidgelet.DeepParameters.smul_nil.{u_1,
    u_2}
  {G : Type u_1} {Ξ : ℕ → Type u_2}
  [(i : ℕ) → SMul G (Ξ i)] (g : G) :
  g • LeanRidgelet.DeepParameters.nil =
    LeanRidgelet.DeepParameters.nil

theoremdefined in LeanRidgelet/HA/Deep.lean

complete

theorem LeanRidgelet.DeepParameters.smul_snoc.{u_1, u_2} {G : Type u_1}
  {Ξ : ℕ → Type u_2} [(i : ℕ) → SMul G (Ξ i)] (g : G) {n : ℕ}
  (ξ : LeanRidgelet.DeepParameters Ξ n) (ξn : Ξ n) :
  g • ξ.snoc ξn = (g • ξ).snoc (g • ξn)

theorem LeanRidgelet.DeepParameters.smul_snoc.{u_1,
    u_2}
  {G : Type u_1} {Ξ : ℕ → Type u_2}
  [(i : ℕ) → SMul G (Ξ i)] (g : G) {n : ℕ}
  (ξ : LeanRidgelet.DeepParameters Ξ n)
  (ξn : Ξ n) :
  g • ξ.snoc ξn = (g • ξ).snoc (g • ξn)

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.deepFeature_zero.{u_2, u_3} {X : ℕ → Type u_2}
  {Ξ : ℕ → Type u_3} (φ : (i : ℕ) → X i → Ξ i → X (i + 1)) (x : X 0) :
  LeanRidgelet.deepFeature φ 0 x LeanRidgelet.DeepParameters.nil = x

theorem LeanRidgelet.deepFeature_zero.{u_2, u_3}
  {X : ℕ → Type u_2} {Ξ : ℕ → Type u_3}
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (x : X 0) :
  LeanRidgelet.deepFeature φ 0 x
      LeanRidgelet.DeepParameters.nil =
    x

theoremdefined in LeanRidgelet/HA/Deep.lean

complete

theorem LeanRidgelet.deepFeature_succ.{u_2, u_3} {X : ℕ → Type u_2}
  {Ξ : ℕ → Type u_3} (φ : (i : ℕ) → X i → Ξ i → X (i + 1)) (n : ℕ)
  (x : X 0) (ξ : LeanRidgelet.DeepParameters Ξ n) (ξn : Ξ n) :
  LeanRidgelet.deepFeature φ (n + 1) x (ξ.snoc ξn) =
    φ n (LeanRidgelet.deepFeature φ n x ξ) ξn

theorem LeanRidgelet.deepFeature_succ.{u_2, u_3}
  {X : ℕ → Type u_2} {Ξ : ℕ → Type u_3}
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (n : ℕ) (x : X 0)
  (ξ : LeanRidgelet.DeepParameters Ξ n)
  (ξn : Ξ n) :
  LeanRidgelet.deepFeature φ (n + 1) x
      (ξ.snoc ξn) =
    φ n (LeanRidgelet.deepFeature φ n x ξ)
      ξn

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.

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.4.6

Statement uses 2

Statement dependency previews

Preview

Definition 4.4.1

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 4.4.9

Loading preview

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

✓L∃∀N

L2 boundedness reuse. Given covariance under chosen representations, the existing L2 networkSynthesis and ridgeletOperator become HA continuous intertwiners. Their concrete norm bound and exact networkSynthesis ∘ ridgeletOperator identity are inherited directly; no second Bochner boundedness proof or assumption structure is introduced.

Lean code for Definition4.4.6●4 declarations

defdefined in LeanRidgelet/HA/L2Bridge.lean

complete

def LeanRidgelet.l2NetworkSynthesisMachine.{u_1} {G : Type u_1} [Monoid G]
  (m : ℕ) [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G ↥(LeanRidgelet.ParameterSpace m s t))
  (πData : ContRepresentation ℂ G ↥(LeanRidgelet.TargetSpace m))
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (hintertwines :
    ∀ (g : G) (γ : ↥(LeanRidgelet.ParameterSpace m s t)),
      (LeanRidgelet.networkSynthesis m s t σ) ((πParameter g) γ) =
        (πData g) ((LeanRidgelet.networkSynthesis m s t σ) γ)) :
  LeanRidgelet.JointEquivariantMachine πParameter πData

def LeanRidgelet.l2NetworkSynthesisMachine.{u_1}
  {G : Type u_1} [Monoid G] (m : ℕ)
  [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.ParameterSpace m s
          t))
  (πData :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.TargetSpace m))
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (hintertwines :
    ∀ (g : G)
      (γ :
        ↥(LeanRidgelet.ParameterSpace m s
            t)),
      (LeanRidgelet.networkSynthesis m s t
            σ)
          ((πParameter g) γ) =
        (πData g)
          ((LeanRidgelet.networkSynthesis
              m s t σ)
            γ)) :
  LeanRidgelet.JointEquivariantMachine
    πParameter πData

Implementation after :=

:= networkSynthesis m s t σ
  isIntertwining' g := by
    apply ContinuousLinearMap.ext
    intro γ
    exact hintertwines g γ

Bundle the already bounded L2 synthesis operator as a joint-equivariant machine.

defdefined in LeanRidgelet/HA/L2Bridge.lean

complete

def LeanRidgelet.l2RidgeletIntertwiningMap.{u_1} {G : Type u_1} [Monoid G]
  (m : ℕ) [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G ↥(LeanRidgelet.ParameterSpace m s t))
  (πData : ContRepresentation ℂ G ↥(LeanRidgelet.TargetSpace m))
  (h : LeanRidgelet.FiberSpace m s t)
  (hintertwines :
    ∀ (g : G) (f : ↥(LeanRidgelet.TargetSpace m)),
      (LeanRidgelet.ridgeletOperator m s t h) ((πData g) f) =
        (πParameter g) ((LeanRidgelet.ridgeletOperator m s t h) f)) :
  LeanRidgelet.JointEquivariantRidgelet πData πParameter

def LeanRidgelet.l2RidgeletIntertwiningMap.{u_1}
  {G : Type u_1} [Monoid G] (m : ℕ)
  [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.ParameterSpace m s
          t))
  (πData :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.TargetSpace m))
  (h : LeanRidgelet.FiberSpace m s t)
  (hintertwines :
    ∀ (g : G)
      (f : ↥(LeanRidgelet.TargetSpace m)),
      (LeanRidgelet.ridgeletOperator m s t
            h)
          ((πData g) f) =
        (πParameter g)
          ((LeanRidgelet.ridgeletOperator
              m s t h)
            f)) :
  LeanRidgelet.JointEquivariantRidgelet
    πData πParameter

Implementation after :=

:= ridgeletOperator m s t h
  isIntertwining' g := by
    apply ContinuousLinearMap.ext
    intro f
    exact hintertwines g f

Bundle an already bounded L2 ridgelet operator as the reverse intertwiner.

theoremdefined in LeanRidgelet/HA/L2Bridge.lean

complete

theorem LeanRidgelet.norm_l2NetworkSynthesisMachine_le.{u_1} {G : Type u_1}
  [Monoid G] (m : ℕ) [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G ↥(LeanRidgelet.ParameterSpace m s t))
  (πData : ContRepresentation ℂ G ↥(LeanRidgelet.TargetSpace m))
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (hintertwines :
    ∀ (g : G) (γ : ↥(LeanRidgelet.ParameterSpace m s t)),
      (LeanRidgelet.networkSynthesis m s t σ) ((πParameter g) γ) =
        (πData g) ((LeanRidgelet.networkSynthesis m s t σ) γ)) :
  ‖(LeanRidgelet.l2NetworkSynthesisMachine m s t πParameter πData σ
          hintertwines).toContinuousLinearMap‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖

theorem LeanRidgelet.norm_l2NetworkSynthesisMachine_le.{u_1}
  {G : Type u_1} [Monoid G] (m : ℕ)
  [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.ParameterSpace m s
          t))
  (πData :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.TargetSpace m))
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (hintertwines :
    ∀ (g : G)
      (γ :
        ↥(LeanRidgelet.ParameterSpace m s
            t)),
      (LeanRidgelet.networkSynthesis m s t
            σ)
          ((πParameter g) γ) =
        (πData g)
          ((LeanRidgelet.networkSynthesis
              m s t σ)
            γ)) :
  ‖(LeanRidgelet.l2NetworkSynthesisMachine
          m s t πParameter πData σ
          hintertwines).toContinuousLinearMap‖ ≤
    (2 * Real.pi) ^ (m - 1) * ‖σ‖

The HA machine retains the concrete L2 synthesis norm bound.

theoremdefined in LeanRidgelet/HA/L2Bridge.lean

complete

theorem LeanRidgelet.l2_jointReconstructionOperator_eq.{u_1} {G : Type u_1}
  [Monoid G] (m : ℕ) [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G ↥(LeanRidgelet.ParameterSpace m s t))
  (πData : ContRepresentation ℂ G ↥(LeanRidgelet.TargetSpace m))
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberSpace m s t)
  (hM :
    ∀ (g : G) (γ : ↥(LeanRidgelet.ParameterSpace m s t)),
      (LeanRidgelet.networkSynthesis m s t σ) ((πParameter g) γ) =
        (πData g) ((LeanRidgelet.networkSynthesis m s t σ) γ))
  (hR :
    ∀ (g : G) (f : ↥(LeanRidgelet.TargetSpace m)),
      (LeanRidgelet.ridgeletOperator m s t h) ((πData g) f) =
        (πParameter g) ((LeanRidgelet.ridgeletOperator m s t h) f)) :
  LeanRidgelet.jointReconstructionOperator
      (LeanRidgelet.l2NetworkSynthesisMachine m s t πParameter πData σ
        hM)
      (LeanRidgelet.l2RidgeletIntertwiningMap m s t πParameter πData h
        hR) =
    (LeanRidgelet.activationFiberFunctional m s t σ) h •
      ContinuousLinearMap.id ℂ ↥(LeanRidgelet.TargetSpace m)

theorem LeanRidgelet.l2_jointReconstructionOperator_eq.{u_1}
  {G : Type u_1} [Monoid G] (m : ℕ)
  [NeZero m] (s t : ℝ)
  (πParameter :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.ParameterSpace m s
          t))
  (πData :
    ContRepresentation ℂ G
      ↥(LeanRidgelet.TargetSpace m))
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (h : LeanRidgelet.FiberSpace m s t)
  (hM :
    ∀ (g : G)
      (γ :
        ↥(LeanRidgelet.ParameterSpace m s
            t)),
      (LeanRidgelet.networkSynthesis m s t
            σ)
          ((πParameter g) γ) =
        (πData g)
          ((LeanRidgelet.networkSynthesis
              m s t σ)
            γ))
  (hR :
    ∀ (g : G)
      (f : ↥(LeanRidgelet.TargetSpace m)),
      (LeanRidgelet.ridgeletOperator m s t
            h)
          ((πData g) f) =
        (πParameter g)
          ((LeanRidgelet.ridgeletOperator
              m s t h)
            f)) :
  LeanRidgelet.jointReconstructionOperator
      (LeanRidgelet.l2NetworkSynthesisMachine
        m s t πParameter πData σ hM)
      (LeanRidgelet.l2RidgeletIntertwiningMap
        m s t πParameter πData h hR) =
    (LeanRidgelet.activationFiberFunctional
          m s t σ)
        h •
      ContinuousLinearMap.id ℂ
        ↥(LeanRidgelet.TargetSpace m)

The HA composite of the L2 bounded operators is the L2 scalar reconstruction identity.

Lemma4.4.7

uses 1used by 1✓L∃∀N

Fully-connected endpoint covariance. Linear maps replace matrices. Direct cancellation proves that (Lx+t, A L⁻¹, b+A L⁻¹t) leaves the first layer unchanged, while composing the last readout with the output linear equivalence transforms the final value. Separate first/last tuple maps and two induction lemmas propagate these identities through every depth.

Lean code for Lemma4.4.7●12 declarations

abbrevdefined in LeanRidgelet/HA/FullyConnected.lean

complete

abbrev LeanRidgelet.FullyConnectedParameter.{u_1, u_2, u_3, u_4} (X : Type u_1)
  (P : Type u_2) (Q : Type u_3) (Y : Type u_4) [AddCommGroup X]
  [Module ℝ X] [AddCommGroup P] [Module ℝ P] [AddCommGroup Q]
  [Module ℝ Q] [AddCommGroup Y] [Module ℝ Y] :
  Type (max (max u_2 u_1) (max u_4 u_3) u_2)

abbrev LeanRidgelet.FullyConnectedParameter.{u_1,
    u_2, u_3, u_4}
  (X : Type u_1) (P : Type u_2)
  (Q : Type u_3) (Y : Type u_4)
  [AddCommGroup X] [Module ℝ X]
  [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q]
  [AddCommGroup Y] [Module ℝ Y] :
  Type
    (max (max u_2 u_1) (max u_4 u_3) u_2)

Implementation after :=

:=
  (X →ₗ[ℝ] P) × P × (Q →ₗ[ℝ] Y)

Parameters `(A,b,C)` of one heterogeneous fully-connected layer.

defdefined in LeanRidgelet/HA/FullyConnected.lean

complete

def LeanRidgelet.fullyConnectedFeature.{u_1, u_2, u_3, u_4} {X : Type u_1}
  {P : Type u_2} {Q : Type u_3} {Y : Type u_4} [AddCommGroup X]
  [Module ℝ X] [AddCommGroup P] [Module ℝ P] [AddCommGroup Q]
  [Module ℝ Q] [AddCommGroup Y] [Module ℝ Y] (σ : P → Q) (x : X)
  (ξ : LeanRidgelet.FullyConnectedParameter X P Q Y) : Y

def LeanRidgelet.fullyConnectedFeature.{u_1,
    u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2}
  {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X]
  [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q]
  [AddCommGroup Y] [Module ℝ Y]
  (σ : P → Q) (x : X)
  (ξ :
    LeanRidgelet.FullyConnectedParameter X
      P Q Y) :
  Y

Implementation after :=

:=
  ξ.2.2 (σ (ξ.1 x - ξ.2.1))

A fully-connected feature `C[σ(Ax-b)]`.

defdefined in LeanRidgelet/HA/FullyConnected.lean

complete

def LeanRidgelet.fullyConnectedInputParameterTransform.{u_1, u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2} {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X] [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q] [AddCommGroup Y] [Module ℝ Y]
  (L : X ≃ₗ[ℝ] X) (t : X)
  (ξ : LeanRidgelet.FullyConnectedParameter X P Q Y) :
  LeanRidgelet.FullyConnectedParameter X P Q Y

def LeanRidgelet.fullyConnectedInputParameterTransform.{u_1,
    u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2}
  {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X]
  [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q]
  [AddCommGroup Y] [Module ℝ Y]
  (L : X ≃ₗ[ℝ] X) (t : X)
  (ξ :
    LeanRidgelet.FullyConnectedParameter X
      P Q Y) :
  LeanRidgelet.FullyConnectedParameter X P
    Q Y

Implementation after :=

:=
  (ξ.1.comp L.symm.toLinearMap, ξ.2.1 + ξ.1 (L.symm t), ξ.2.2)

Change of first-layer parameters contragredient to `x ↦ L x + t`.

theoremdefined in LeanRidgelet/HA/FullyConnected.lean

complete

theorem LeanRidgelet.fullyConnectedFeature_input_invariant.{u_1, u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2} {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X] [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q] [AddCommGroup Y] [Module ℝ Y]
  (σ : P → Q) (L : X ≃ₗ[ℝ] X) (t x : X)
  (ξ : LeanRidgelet.FullyConnectedParameter X P Q Y) :
  LeanRidgelet.fullyConnectedFeature σ (L x + t)
      (LeanRidgelet.fullyConnectedInputParameterTransform L t ξ) =
    LeanRidgelet.fullyConnectedFeature σ x ξ

theorem LeanRidgelet.fullyConnectedFeature_input_invariant.{u_1,
    u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2}
  {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X]
  [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q]
  [AddCommGroup Y] [Module ℝ Y]
  (σ : P → Q) (L : X ≃ₗ[ℝ] X) (t x : X)
  (ξ :
    LeanRidgelet.FullyConnectedParameter X
      P Q Y) :
  LeanRidgelet.fullyConnectedFeature σ
      (L x + t)
      (LeanRidgelet.fullyConnectedInputParameterTransform
        L t ξ) =
    LeanRidgelet.fullyConnectedFeature σ x
      ξ

The transformed first layer has exactly the same value on the transformed input.

defdefined in LeanRidgelet/HA/FullyConnected.lean

complete

def LeanRidgelet.fullyConnectedOutputParameterTransform.{u_1, u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2} {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X] [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q] [AddCommGroup Y] [Module ℝ Y]
  (R : Y ≃ₗ[ℝ] Y) (ξ : LeanRidgelet.FullyConnectedParameter X P Q Y) :
  LeanRidgelet.FullyConnectedParameter X P Q Y

def LeanRidgelet.fullyConnectedOutputParameterTransform.{u_1,
    u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2}
  {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X]
  [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q]
  [AddCommGroup Y] [Module ℝ Y]
  (R : Y ≃ₗ[ℝ] Y)
  (ξ :
    LeanRidgelet.FullyConnectedParameter X
      P Q Y) :
  LeanRidgelet.FullyConnectedParameter X P
    Q Y

Implementation after :=

:=
  (ξ.1, ξ.2.1, R.toLinearMap.comp ξ.2.2)

Change of the last-layer readout by an invertible linear output map.

theoremdefined in LeanRidgelet/HA/FullyConnected.lean

complete

theorem LeanRidgelet.fullyConnectedFeature_output_equivariant.{u_1, u_2, u_3,
    u_4}
  {X : Type u_1} {P : Type u_2} {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X] [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q] [AddCommGroup Y] [Module ℝ Y]
  (σ : P → Q) (R : Y ≃ₗ[ℝ] Y) (x : X)
  (ξ : LeanRidgelet.FullyConnectedParameter X P Q Y) :
  LeanRidgelet.fullyConnectedFeature σ x
      (LeanRidgelet.fullyConnectedOutputParameterTransform R ξ) =
    R (LeanRidgelet.fullyConnectedFeature σ x ξ)

theorem LeanRidgelet.fullyConnectedFeature_output_equivariant.{u_1,
    u_2, u_3, u_4}
  {X : Type u_1} {P : Type u_2}
  {Q : Type u_3} {Y : Type u_4}
  [AddCommGroup X] [Module ℝ X]
  [AddCommGroup P] [Module ℝ P]
  [AddCommGroup Q] [Module ℝ Q]
  [AddCommGroup Y] [Module ℝ Y]
  (σ : P → Q) (R : Y ≃ₗ[ℝ] Y) (x : X)
  (ξ :
    LeanRidgelet.FullyConnectedParameter X
      P Q Y) :
  LeanRidgelet.fullyConnectedFeature σ x
      (LeanRidgelet.fullyConnectedOutputParameterTransform
        R ξ) =
    R
      (LeanRidgelet.fullyConnectedFeature
        σ x ξ)

The transformed last readout applies the output representation to the layer value.

defdefined in LeanRidgelet/HA/FullyConnected.lean

complete

def LeanRidgelet.DeepParameters.mapFirst.{u_1} {Ξ : ℕ → Type u_1}
  (F : Ξ 0 → Ξ 0) {n : ℕ} :
  LeanRidgelet.DeepParameters Ξ (n + 1) →
    LeanRidgelet.DeepParameters Ξ (n + 1)

def LeanRidgelet.DeepParameters.mapFirst.{u_1}
  {Ξ : ℕ → Type u_1} (F : Ξ 0 → Ξ 0)
  {n : ℕ} :
  LeanRidgelet.DeepParameters Ξ (n + 1) →
    LeanRidgelet.DeepParameters Ξ (n + 1)

Apply a map only to the first entry of a nonempty heterogeneous tuple.

defdefined in LeanRidgelet/HA/FullyConnected.lean

complete

def LeanRidgelet.DeepParameters.mapLast.{u_1} {Ξ : ℕ → Type u_1} {n : ℕ}
  (F : Ξ n → Ξ n) :
  LeanRidgelet.DeepParameters Ξ (n + 1) →
    LeanRidgelet.DeepParameters Ξ (n + 1)

def LeanRidgelet.DeepParameters.mapLast.{u_1}
  {Ξ : ℕ → Type u_1} {n : ℕ}
  (F : Ξ n → Ξ n) :
  LeanRidgelet.DeepParameters Ξ (n + 1) →
    LeanRidgelet.DeepParameters Ξ (n + 1)

Apply a map only to the last entry of a nonempty heterogeneous tuple.

theoremdefined in LeanRidgelet/HA/FullyConnected.lean

complete

theorem LeanRidgelet.deepFeature_mapFirst.{u_1, u_2} {X : ℕ → Type u_1}
  {Ξ : ℕ → Type u_2} (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (F : Ξ 0 → Ξ 0) (S : X 0 → X 0)
  (hfirst : ∀ (x : X 0) (ξ : Ξ 0), φ 0 (S x) (F ξ) = φ 0 x ξ) (n : ℕ)
  (x : X 0) (ξ : LeanRidgelet.DeepParameters Ξ (n + 1)) :
  LeanRidgelet.deepFeature φ (n + 1) (S x)
      (LeanRidgelet.DeepParameters.mapFirst F ξ) =
    LeanRidgelet.deepFeature φ (n + 1) x ξ

theorem LeanRidgelet.deepFeature_mapFirst.{u_1,
    u_2}
  {X : ℕ → Type u_1} {Ξ : ℕ → Type u_2}
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (F : Ξ 0 → Ξ 0) (S : X 0 → X 0)
  (hfirst :
    ∀ (x : X 0) (ξ : Ξ 0),
      φ 0 (S x) (F ξ) = φ 0 x ξ)
  (n : ℕ) (x : X 0)
  (ξ :
    LeanRidgelet.DeepParameters Ξ
      (n + 1)) :
  LeanRidgelet.deepFeature φ (n + 1) (S x)
      (LeanRidgelet.DeepParameters.mapFirst
        F ξ) =
    LeanRidgelet.deepFeature φ (n + 1) x ξ

A change absorbed by the first layer does not affect the value of the full cascade.

theoremdefined in LeanRidgelet/HA/FullyConnected.lean

complete

theorem LeanRidgelet.deepFeature_mapLast.{u_1, u_2} {X : ℕ → Type u_1}
  {Ξ : ℕ → Type u_2} (φ : (i : ℕ) → X i → Ξ i → X (i + 1)) (n : ℕ)
  (F : Ξ n → Ξ n) (R : X (n + 1) → X (n + 1))
  (hlast : ∀ (x : X n) (ξ : Ξ n), φ n x (F ξ) = R (φ n x ξ)) (x : X 0)
  (ξ : LeanRidgelet.DeepParameters Ξ (n + 1)) :
  LeanRidgelet.deepFeature φ (n + 1) x
      (LeanRidgelet.DeepParameters.mapLast F ξ) =
    R (LeanRidgelet.deepFeature φ (n + 1) x ξ)

theorem LeanRidgelet.deepFeature_mapLast.{u_1,
    u_2}
  {X : ℕ → Type u_1} {Ξ : ℕ → Type u_2}
  (φ : (i : ℕ) → X i → Ξ i → X (i + 1))
  (n : ℕ) (F : Ξ n → Ξ n)
  (R : X (n + 1) → X (n + 1))
  (hlast :
    ∀ (x : X n) (ξ : Ξ n),
      φ n x (F ξ) = R (φ n x ξ))
  (x : X 0)
  (ξ :
    LeanRidgelet.DeepParameters Ξ
      (n + 1)) :
  LeanRidgelet.deepFeature φ (n + 1) x
      (LeanRidgelet.DeepParameters.mapLast
        F ξ) =
    R
      (LeanRidgelet.deepFeature φ (n + 1)
        x ξ)

A change absorbed by the last layer acts on the output of the full cascade.

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.4.8

Statement uses 4

Statement dependency previews

Preview

Theorem 4.3.3

Loading preview

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

used by 1✓L∃∀N

The Section 5 representation and Lemma 5.1 boundary. The output representation is lifted pointwise to Bochner L^2; it commutes with the affine weighted pullback because a complex-linear unitary commutes with the scalar Radon--Nikodym factor. Their commuting product gives the actual representation on L^2(E;Y) and its article-level a.e. formula. Entrywise complexification of real orthogonal matrices now supplies the concrete standard O(m) output factor, whose irreducibility is proved independently; substituting it gives the article's O(m)\times\operatorname{Aff}(m) representation and matrix-level formula. Naturality of the affine pullback under pointwise coordinate embeddings and projections lets Schur act on every scalar matrix coefficient of an invariant orthogonal projection. Finite coordinate reconstruction makes that projection the lift of a fixed output operator, to which output Schur applies. This closes the Folland-7.12 finite-output step without a completed Hilbert tensor product; the concrete conclusion now depends only on the separate scalar affine induced-system convolution-regularity placeholder.

Lean code for Lemma4.4.8●9 declarations

theoremdefined in LeanRidgelet/HA/Affine.lean

complete

theorem LeanRidgelet.affineDataLpUnitaryRepresentation_apply_ae_vector.{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 μ] (g : E ≃ᵃ[ℝ] E)
  (f : ↥(MeasureTheory.Lp Y 2 μ)) :
  ↑↑(↑((LeanRidgelet.affineDataLpUnitaryRepresentation μ) g) f) =ᵐ[μ]
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight LeanRidgelet.affineDataJacobian)
      g fun x ↦ ↑↑f x

theorem LeanRidgelet.affineDataLpUnitaryRepresentation_apply_ae_vector.{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 μ]
  (g : E ≃ᵃ[ℝ] E)
  (f : ↥(MeasureTheory.Lp Y 2 μ)) :
  ↑↑(↑((LeanRidgelet.affineDataLpUnitaryRepresentation
                μ)
              g)
          f) =ᵐ[μ]
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineDataJacobian)
      g fun x ↦ ↑↑f x

The corrected affine action on vector-valued `L²` has the expected weighted-pullback
representative.  The scalar specialization used by the Mackey analysis is recorded separately in
`HA.AffineIrreducibility`; this version is the Bochner `L²` input needed for Section 5.

theoremdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

theorem LeanRidgelet.compLpL_intertwines_affineData.{u_2, u_3, u_4}
  {E : Type u_2} {Y : Type u_3} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Z : Type u_4} [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z] [CompleteSpace Z] (L : Y →L[ℂ] Z)
  (g : E ≃ᵃ[ℝ] E) :
  ↑((LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume)
          g) ∘SL
      ContinuousLinearMap.compLpL 2 MeasureTheory.volume L =
    ContinuousLinearMap.compLpL 2 MeasureTheory.volume L ∘SL
      ↑((LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume)
          g)

theorem LeanRidgelet.compLpL_intertwines_affineData.{u_2,
    u_3, u_4}
  {E : Type u_2} {Y : Type u_3}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Z : Type u_4}
  [NormedAddCommGroup Z]
  [InnerProductSpace ℂ Z]
  [CompleteSpace Z] (L : Y →L[ℂ] Z)
  (g : E ≃ᵃ[ℝ] E) :
  ↑((LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume)
          g) ∘SL
      ContinuousLinearMap.compLpL 2
        MeasureTheory.volume L =
    ContinuousLinearMap.compLpL 2
        MeasureTheory.volume L ∘SL
      ↑((LeanRidgelet.affineDataLpUnitaryRepresentation
            MeasureTheory.volume)
          g)

Every bounded value-space map intertwines the determinant-corrected affine pullbacks on the
corresponding Bochner `L²` spaces.  This naturality supplies both the coordinate embeddings and
coordinate projections used in the finite-output Schur argument.

theoremdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

theorem LeanRidgelet.lpPointwise_commute_affineData.{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]
  (υ : UnitaryRepresentation G Y) (q : G) (g : E ≃ᵃ[ℝ] E) :
  Commute (υ.lpPointwise q)
    ((LeanRidgelet.affineDataLpUnitaryRepresentation
        MeasureTheory.volume)
      g)

theorem LeanRidgelet.lpPointwise_commute_affineData.{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]
  (υ : UnitaryRepresentation G Y) (q : G)
  (g : E ≃ᵃ[ℝ] E) :
  Commute (υ.lpPointwise q)
    ((LeanRidgelet.affineDataLpUnitaryRepresentation
        MeasureTheory.volume)
      g)

Pointwise output unitaries commute with the determinant-corrected affine pullback on
vector-valued `L²`.

defdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

def LeanRidgelet.fullyConnectedLpUnitaryRepresentation.{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]
  (υ : UnitaryRepresentation G Y) :
  UnitaryRepresentation (G × (E ≃ᵃ[ℝ] E))
    ↥(MeasureTheory.Lp Y 2 MeasureTheory.volume)

def LeanRidgelet.fullyConnectedLpUnitaryRepresentation.{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]
  (υ : UnitaryRepresentation G Y) :
  UnitaryRepresentation (G × (E ≃ᵃ[ℝ] E))
    ↥(MeasureTheory.Lp Y 2
        MeasureTheory.volume)

Implementation after :=

:=
  UnitaryRepresentation.prodOfCommute
    (υ.lpPointwise (μ := (volume : Measure E)))
    (affineDataLpUnitaryRepresentation (Y := Y) (volume : Measure E))
    (lpPointwise_commute_affineData υ)

The Section 5 product-group representation on `L²(E;Y)`: the first factor acts on output
values and the affine factor acts on the input variable.

theoremdefined in LeanRidgelet/HA/FullyConnectedIrreducibility.lean

complete

theorem LeanRidgelet.fullyConnectedLpUnitaryRepresentation_apply_ae.{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]
  (υ : UnitaryRepresentation G Y) (g : G × (E ≃ᵃ[ℝ] E))
  (f : ↥(MeasureTheory.Lp Y 2 MeasureTheory.volume)) :
  ↑↑(↑((LeanRidgelet.fullyConnectedLpUnitaryRepresentation υ) g)
          f) =ᵐ[MeasureTheory.volume]
    fun x ↦
    LeanRidgelet.radonNikodymWeight LeanRidgelet.affineDataJacobian g.2
        x •
      ↑(υ g.1) (↑↑f (g.2⁻¹ • x))

theorem LeanRidgelet.fullyConnectedLpUnitaryRepresentation_apply_ae.{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]
  (υ : UnitaryRepresentation G Y)
  (g : G × (E ≃ᵃ[ℝ] E))
  (f :
    ↥(MeasureTheory.Lp Y 2
        MeasureTheory.volume)) :
  ↑↑(↑((LeanRidgelet.fullyConnectedLpUnitaryRepresentation
                υ)
              g)
          f) =ᵐ[MeasureTheory.volume]
    fun x ↦
    LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineDataJacobian
        g.2 x •
      ↑(υ g.1) (↑↑f (g.2⁻¹ • x))

The product representation has the determinant-corrected form stated in Section 5, with the
output unitary applied after affine pullback.

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.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.

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.4.9

Statement uses 2

Statement dependency previews

Preview

Definition 4.4.6

Loading preview

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

used by 1✓L∃∀N

Group-convolution reduction. The function-valued feature is the orbit lift g\mapsto υ(g)[φ(g^{-1}x,ξ)]. Representation multiplication proves equivariance; a linear isometry commutes through the Bochner integral to identify GCN synthesis with the orbit lift of base synthesis. The ridgelet reads only the identity component, and the two identities transport base reconstruction to Theorem 6.1.

Lean code for Theorem4.4.9●9 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.

defdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

def LeanRidgelet.IsGroupConvolutionEquivariant.{u_1, u_2, u_4}
  {G : Type u_1} {X : Type u_2} {Y : Type u_4} [Group G] [MulAction G X]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (υ : UnitaryRepresentation G Y) (f : X → G → Y) : Prop

def LeanRidgelet.IsGroupConvolutionEquivariant.{u_1,
    u_2, u_4}
  {G : Type u_1} {X : Type u_2}
  {Y : Type u_4} [Group G] [MulAction G X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (υ : UnitaryRepresentation G Y)
  (f : X → G → Y) : Prop

Implementation after :=

:=
  ∀ (h : G) (x : X) (g : G),
    f (h • x) g = (υ h : Y →L[ℂ] Y) (f x (h⁻¹ * g))

Equivariance of a function-valued map under the orbit action.

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.

defdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

def LeanRidgelet.groupConvolutionalSynthesis.{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) : Y

def LeanRidgelet.groupConvolutionalSynthesis.{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) : Y

Implementation after :=

:=
  ∫ ξ, γ ξ • groupConvolutionalFeature υ φ x ξ g ∂μ

Pointwise synthesis of a group-convolutional feature.

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.

defdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

def LeanRidgelet.groupConvolutionalRidgelet.{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) : Ξ → ℂ

def LeanRidgelet.groupConvolutionalRidgelet.{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) : Ξ → ℂ

Implementation after :=

:=
  bochnerRidgelet μ ψ (fun x ↦ f x 1)

The Section 6 ridgelet transform: apply the base ridgelet transform to the value at the
identity element.

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`.

theoremdefined in LeanRidgelet/HA/GroupConvolution.lean

complete

theorem LeanRidgelet.groupConvolutional_reconstruction.{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]
  (μParameter : MeasureTheory.Measure Ξ) (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (γ : Ξ → ℂ) (f : X → G → Y)
  (hf : LeanRidgelet.IsGroupConvolutionEquivariant υ f) (c : ℂ)
  (hrec :
    ∀ (x : X),
      LeanRidgelet.bochnerSynthesis μParameter φ γ x = c • f x 1)
  (x : X) (g : G) :
  LeanRidgelet.groupConvolutionalSynthesis μParameter υ φ γ x g =
    c • f x g

theorem LeanRidgelet.groupConvolutional_reconstruction.{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]
  (μParameter : MeasureTheory.Measure Ξ)
  (υ : UnitaryRepresentation G Y)
  (φ : X → Ξ → Y) (γ : Ξ → ℂ)
  (f : X → G → Y)
  (hf :
    LeanRidgelet.IsGroupConvolutionEquivariant
      υ f)
  (c : ℂ)
  (hrec :
    ∀ (x : X),
      LeanRidgelet.bochnerSynthesis
          μParameter φ γ x =
        c • f x 1)
  (x : X) (g : G) :
  LeanRidgelet.groupConvolutionalSynthesis
      μParameter υ φ γ x g =
    c • f x g

Theorem 6.1: a reconstruction formula for the base feature transports to the
group-convolutional orbit lift.  The bounded L2 theory can provide `hrec`; this theorem performs
only the Section 6 transport and introduces no additional boundedness assumption.

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.

Theorem4.4.10

Statement uses 2

Statement dependency previews

Preview

Theorem 4.3.1

Loading preview

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

used by 1✓L∃∀N

Comparison with the classical transforms. The affine depth-two Bochner pair, the Euclidean ridgelet pair of the L1 track at homogeneity index zero, and the classical synthesis integral of the L2 track are the same integrals.

Lean code for Theorem4.4.10●14 declarations

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`.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.isAddHaarMeasure_volume_ridgeParameter (m : ℕ) :
  MeasureTheory.volume.IsAddHaarMeasure

theorem LeanRidgelet.isAddHaarMeasure_volume_ridgeParameter
  (m : ℕ) :
  MeasureTheory.volume.IsAddHaarMeasure

Lebesgue measure on the ridge parameter space `ℝᵐ × ℝ` is an additive Haar measure. Mathlib
provides the instance for inner-product spaces; the ridge parameter space is a plain product, so
the instance is assembled from the product Haar instance and is introduced locally by the results
below rather than globally.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.quasiMeasurePreserving_affineData_inv {m : ℕ}
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m) :
  MeasureTheory.Measure.QuasiMeasurePreserving (fun x ↦ g⁻¹ • x)
    MeasureTheory.volume MeasureTheory.volume

theorem LeanRidgelet.quasiMeasurePreserving_affineData_inv
  {m : ℕ}
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m) :
  MeasureTheory.Measure.QuasiMeasurePreserving
    (fun x ↦ g⁻¹ • x) MeasureTheory.volume
    MeasureTheory.volume

The inverse affine data action is quasi measure preserving for Lebesgue measure: its
pushforward has a constant density.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.quasiUnitaryPullbackAction_affineData_congr_ae {m : ℕ}
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m)
  {f₁ f₂ : LeanRidgelet.InputSpace m → ℂ}
  (hf : f₁ =ᵐ[MeasureTheory.volume] f₂) :
  LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g f₁ =ᵐ[MeasureTheory.volume]
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g f₂

theorem LeanRidgelet.quasiUnitaryPullbackAction_affineData_congr_ae
  {m : ℕ}
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m)
  {f₁ f₂ : LeanRidgelet.InputSpace m → ℂ}
  (hf : f₁ =ᵐ[MeasureTheory.volume] f₂) :
  LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      f₁ =ᵐ[MeasureTheory.volume]
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      f₂

The corrected affine data pullback respects almost-everywhere equality of representatives.
This is what lets an equality of `L²` classes be transported through the action.

defdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

def LeanRidgelet.affineSchwartzParameterAction {m : ℕ}
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ

def LeanRidgelet.affineSchwartzParameterAction
  {m : ℕ}
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  SchwartzMap
    (LeanRidgelet.InputSpace m × ℝ) ℂ

Implementation after :=

:=
  radonNikodymWeight affineParameterJacobian g 0 •
    SchwartzMap.compCLMOfContinuousLinearEquiv ℂ
      (affineParameterLinearEquiv g).symm.toContinuousLinearEquiv γ

The corrected affine parameter action of `LeanRidgelet.HA.Affine`, realized on the Schwartz
class. Its Radon--Nikodym weight is a constant and its parameter substitution is a linear
automorphism of `ℝᵐ × ℝ`, so the Schwartz class is preserved.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.affineSchwartzParameterAction_coe {m : ℕ}
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  ⇑(LeanRidgelet.affineSchwartzParameterAction g γ) =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g ⇑γ

theorem LeanRidgelet.affineSchwartzParameterAction_coe
  {m : ℕ}
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  ⇑(LeanRidgelet.affineSchwartzParameterAction
        g γ) =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g ⇑γ

The Schwartz realization of the affine parameter action has the expected representative. In
particular the hypothesis `hγg_eq` of the synthesis theorem below is never an obstruction: the
transformed coefficient function is again Schwartz.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_ae_intertwines
  {m : ℕ} [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  {σcl : ℝ → ℂ}
  (hσcl :
    ∀ (φ : SchwartzMap ℝ ℂ),
      ((LeanRidgelet.activationRealization s t) σ) φ =
        ∫ (z : ℝ), φ z * σcl z)
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m)
  (γ γg : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγg_eq :
    ⇑γg =
      LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineParameterJacobian)
        g ⇑γ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume)
  (hγg :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γg) 2
      MeasureTheory.volume)
  (hint :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable (fun p ↦ γ p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume)
  (hintg :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable
        (fun p ↦ γg p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t σ)
          (LeanRidgelet.parameterSchwartzRealization s t γg
            hγg)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      ↑↑((LeanRidgelet.networkSynthesis m s t σ)
            (LeanRidgelet.parameterSchwartzRealization s t γ hγ))

theorem LeanRidgelet.networkSynthesis_parameterSchwartzRealization_ae_intertwines
  {m : ℕ} [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  {σcl : ℝ → ℂ}
  (hσcl :
    ∀ (φ : SchwartzMap ℝ ℂ),
      ((LeanRidgelet.activationRealization
              s t)
            σ)
          φ =
        ∫ (z : ℝ), φ z * σcl z)
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m)
  (γ γg :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγg_eq :
    ⇑γg =
      LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          LeanRidgelet.affineParameterJacobian)
        g ⇑γ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume)
  (hγg :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γg)
      2 MeasureTheory.volume)
  (hint :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable
        (fun p ↦
          γ p * σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume)
  (hintg :
    ∀ (x : LeanRidgelet.InputSpace m),
      MeasureTheory.Integrable
        (fun p ↦
          γg p *
            σcl (inner ℝ p.1 x - p.2))
        MeasureTheory.volume) :
  ↑↑((LeanRidgelet.networkSynthesis m s t
            σ)
          (LeanRidgelet.parameterSchwartzRealization
            s t γg
            hγg)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.quasiUnitaryPullbackAction
      LeanRidgelet.affineDataJacobian 1 g
      ↑↑((LeanRidgelet.networkSynthesis m
              s t σ)
            (LeanRidgelet.parameterSchwartzRealization
              s t γ hγ))

**The synthesis half of the affine equivariance, for the bounded `L²` operator.** Let `γg` be
a Schwartz coefficient function representing the corrected affine parameter action on `γ` — for
instance `LeanRidgelet.affineSchwartzParameterAction g γ`. If both lie in the Schwartz
compatibility domain of `LeanRidgelet.networkSynthesis_parameterSchwartzRealization_classical_ae`,
then the bounded synthesis operator sends the transformed coefficient to the corrected affine data
pullback of the untransformed value, almost everywhere.

The proof transports `LeanRidgelet.affineBochnerSynthesis_intertwines` through
`LeanRidgelet.networkSynthesis_ae_eq_bochnerSynthesis_affineFeature`, using the local additive
Haar instance on the ridge parameters. See the module docstring for why this does not discharge
the `hintertwines` hypotheses of `LeanRidgelet.HA.L2Bridge`.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.euclideanRidgeletTransform_intertwines {m : ℕ} (ψ : ℝ → ℂ)
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (p : LeanRidgelet.RidgeletParameterSpace m) :
  LeanRidgelet.euclideanRidgeletTransform m 0 ψ
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1 g f)
      p =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g (LeanRidgelet.euclideanRidgeletTransform m 0 ψ f) p

theorem LeanRidgelet.euclideanRidgeletTransform_intertwines
  {m : ℕ} (ψ : ℝ → ℂ)
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (p :
    LeanRidgelet.RidgeletParameterSpace
      m) :
  LeanRidgelet.euclideanRidgeletTransform
      m 0 ψ
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1
        g f)
      p =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g
      (LeanRidgelet.euclideanRidgeletTransform
        m 0 ψ f)
      p

**The ridgelet half of the affine equivariance, in classical Euclidean form.** The classical
Euclidean ridgelet transform at homogeneity index `0` intertwines the corrected affine data
pullback with the corrected affine parameter action, at every parameter point and with no
hypothesis. This is `LeanRidgelet.affineBochnerRidgelet_intertwines` read through
`LeanRidgelet.bochnerRidgelet_affineFeature_eq_euclideanRidgeletTransform`; Lebesgue measure on
the data space is an additive Haar measure by Mathlib's inner-product instance.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.classicalRidgeletIntegral_eq_euclideanRidgeletTransform
  {m : ℕ} (ρ : ℝ → ℂ) (f : LeanRidgelet.InputSpace m → ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral f ρ p =
    LeanRidgelet.euclideanRidgeletTransform m 0 ρ f p

theorem LeanRidgelet.classicalRidgeletIntegral_eq_euclideanRidgeletTransform
  {m : ℕ} (ρ : ℝ → ℂ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral f
      ρ p =
    LeanRidgelet.euclideanRidgeletTransform
      m 0 ρ f p

The `L²` track's classical ridgelet integral is the `L¹` track's Euclidean ridgelet transform
at homogeneity index `0`: the two integrands differ by the weight `‖a‖^0 = 1`.

theoremdefined in LeanRidgelet/HA/L2BridgeEquivariance.lean

complete

theorem LeanRidgelet.classicalRidgeletIntegral_intertwines {m : ℕ} (ρ : ℝ → ℂ)
  (g : LeanRidgelet.InputSpace m ≃ᵃ[ℝ] LeanRidgelet.InputSpace m)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1 g f)
      ρ p =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g (LeanRidgelet.classicalRidgeletIntegral f ρ) p

theorem LeanRidgelet.classicalRidgeletIntegral_intertwines
  {m : ℕ} (ρ : ℝ → ℂ)
  (g :
    LeanRidgelet.InputSpace m ≃ᵃ[ℝ]
      LeanRidgelet.InputSpace m)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) :
  LeanRidgelet.classicalRidgeletIntegral
      (LeanRidgelet.quasiUnitaryPullbackAction
        LeanRidgelet.affineDataJacobian 1
        g f)
      ρ p =
    LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        LeanRidgelet.affineParameterJacobian)
      g
      (LeanRidgelet.classicalRidgeletIntegral
        f ρ)
      p

The ridgelet half of the affine equivariance, for the `L²` track's classical ridgelet
integral `R[f; ρ](a, b) = ∫ f(x) conj(ρ(⟪a, x⟫ - b)) dx`.

Nothing is transported: the ridgelet parameter space of the classical development and the affine parameter space of this one are the same type, and the ridge argument of the feature is syntactically the inner product minus the offset. At index zero the classical weight is one, so even the measures agree, and each of the three identifications is definitional up to that weight. There is no Fourier-normalization gap here, because the depth-two formula contains no Fourier transform; the convention enters only the reconstruction constants, whose comparison already exists between the L1 and Fourier-slice tracks.

The reconstruction identity itself is a hypothesis rather than a conclusion, matching the Fourier-slice group-convolution theorem, and for the same reason: the L1 endpoints are stated at homogeneity index one as limits of transforms truncated to annuli, whereas the Bochner synthesis is one absolutely convergent integral, and the dominated-convergence step between them fails for the admissible pairs the L1 track constructs, where the ridgelet transform is only square-integrable against the weighted parameter measure. Given the hypothesis, the composite is reconstructed with the same scalar. The last identification ties the bounded operator of the L2 bridge to the Bochner formula, and transporting the affine intertwining identity through it gives the equivariance of the classical network synthesis on the Schwartz compatibility domain, together with the exact equivariance of the classical ridgelet integral. It does not, however, discharge the equivariance hypotheses the L2 bridge carries. Those are stated over the transported-coordinate parameter space, where the bias variable has been replaced by the fiber frequency, and the affine parameter action lives on functions of the direction and the bias; the two are different Hilbert spaces and no unitary identification of them exists here, since a translation of the bias becomes a modulation in the fiber. Two smaller mismatches compound it: the bridge quantifies over every square-integrable class while the comparison reaches only the Schwartz domain, and there is no ridgelet-side comparison for the transported operator at all.

Theorem4.4.11

Statement uses 2

Statement dependency previews

Preview

Theorem 4.3.1

Loading preview

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

used by 1XL∃∀N

Remaining analytic comparison. Identify the L2 transported-coordinate operators with each classical affine/deep Bochner realization on the appropriate compatibility domain. Architectures with genuinely different parameter spaces continue to use the explicit bounded-extension bridge.

Theorem4.4.12

Statement uses 3

Statement dependency previews

Preview

Theorem 4.3.3

Loading preview

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

used by 0XL∃∀N

Remaining architectures and approximation. The general Hilbert--Schmidt criterion and the finite-sum discretization are now proved in the Mathlib candidate layer; what remains is to instantiate them at the parameter spaces the L2 bridge does not cover, and to derive the quadratic synthesis and ridgelet pair from its parameter representation. Difficult endpoints remain named declarations rather than assumption objects.