4.2. Harmonic-analysis method: representations and intertwiners🔗

This chapter and the two that follow describe the implementation of the harmonic-analysis method in Lean dependency order; the publication-order roadmap is the overview-ha chapter. The Lean project separates OverviewHA from the detail import carrier LeanRidgelet.HA, the modules under LeanRidgelet/HA/, and the Mathlib-only Schur development under LeanRidgelet/ToMathlib/LieGroup/. This chapter covers the layers that precede any concrete architecture: unitary representations and Schur's lemma, pointwise joint equivariance, induced L^2 representations, and the Bochner integral identities that turn them into intertwining operators.

Unitary representations and the Hilbert-space Schur lemma

Definition4.2.1

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 4.2.2

Loading preview

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

✓L∃∀N

The representation layer. A unitary representation is a monoid homomorphism into the unitary group of bounded operators. Forgetting unitarity produces Mathlib's ContRepresentation; closed submodules state topological irreducibility without strengthening it to algebraic irreducibility.

Lean code for Definition4.2.1●4 definitions

abbrevdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

Implementation after :=

:=
  .ofMonoidHom
    { toFun := fun g ↦ (π g : H →L[ℂ] H)
      map_one' := by simp
      map_mul' := by
        intro g h
        simp }

Forget that the operators in a unitary representation are unitary.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

Implementation after :=

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

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

Theorem4.2.2

uses 1used by 1✓L∃∀N

The upstream candidate. Folland's proof is split into mechanically checkable pieces: invariant closed subspaces correspond to commuting orthogonal projections, the commutant is adjoint-closed, and real and imaginary self-adjoint parts are scalar. The nontrivial spectral subspace is the range closure of a continuous positive-part cutoff. A second orthogonal nonzero cutoff proves that this closure is proper, while continuous-functional-calculus commutation makes its projection belong to the commutant. Conversely, on a nontrivial Hilbert space the Schur property makes the orthogonal projection onto every invariant closed subspace scalar; idempotence forces that scalar to be zero or one. Hence topological irreducibility and scalarity of the commutant are equivalent.

Lean code for Theorem4.2.2●10 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

Implementation after :=

:=
  ∀ g : G, T.comp (π g : H →L[ℂ] H) = (π g : H →L[ℂ] H).comp T

Membership in the commutant of a unitary representation.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.isInvariant_iff_starProjection_commutes.{u_1, u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) (K : ClosedSubmodule ℂ H) :
  π.IsInvariant K ↔ π.Commutes (↑K).starProjection

theorem UnitaryRepresentation.isInvariant_iff_starProjection_commutes.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H)
  (K : ClosedSubmodule ℂ H) :
  π.IsInvariant K ↔
    π.Commutes (↑K).starProjection

Folland Proposition 3.4: a closed subspace is invariant precisely when its orthogonal
projection belongs to the commutant.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.Commutes.adjoint.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  {π : UnitaryRepresentation G H} {T : H →L[ℂ] H} (hT : π.Commutes T) :
  π.Commutes (ContinuousLinearMap.adjoint T)

theorem UnitaryRepresentation.Commutes.adjoint.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  {π : UnitaryRepresentation G H}
  {T : H →L[ℂ] H} (hT : π.Commutes T) :
  π.Commutes
    (ContinuousLinearMap.adjoint T)

The commutant of a unitary representation is closed under adjoints.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.exists_nonzero_orthogonal_cutoffs_of_isSelfAdjoint_not_scalar.{u_2}
  {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A)
  (hscalar : ¬∃ c, A = c • ContinuousLinearMap.id ℂ H) :
  ∃ B C,
    B ≠ 0 ∧
      C ≠ 0 ∧
        IsSelfAdjoint B ∧
          IsSelfAdjoint C ∧
            B ∘SL C = 0 ∧
              ∀ (T : H →L[ℂ] H), A ∘SL T = T ∘SL A → B ∘SL T = T ∘SL B

theorem UnitaryRepresentation.exists_nonzero_orthogonal_cutoffs_of_isSelfAdjoint_not_scalar.{u_2}
  {H : Type u_2} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] (A : H →L[ℂ] H)
  (hA : IsSelfAdjoint A)
  (hscalar :
    ¬∃ c,
        A =
          c •
            ContinuousLinearMap.id ℂ H) :
  ∃ B C,
    B ≠ 0 ∧
      C ≠ 0 ∧
        IsSelfAdjoint B ∧
          IsSelfAdjoint C ∧
            B ∘SL C = 0 ∧
              ∀ (T : H →L[ℂ] H),
                A ∘SL T = T ∘SL A →
                  B ∘SL T = T ∘SL B

A non-scalar self-adjoint operator admits two nonzero orthogonal continuous-functional-calculus
cutoffs. Every operator commuting with the original operator also commutes with the first cutoff.

Choose two distinct points `lo < hi` in the real spectrum and put `r = (lo + hi) / 2`. The
positive parts of `x - r` and `r - x` are nonzero at `hi` and `lo`, respectively, and their product
vanishes everywhere. This continuous substitute for a characteristic function is sufficient for
the infinite-dimensional Schur argument; no Borel functional calculus is needed.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.exists_nontrivial_spectralSubspace_of_isSelfAdjoint_not_scalar.{u_2}
  {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A)
  (hscalar : ¬∃ c, A = c • ContinuousLinearMap.id ℂ H) :
  ∃ K,
    K ≠ ⊥ ∧
      K ≠ ⊤ ∧
        ∀ (T : H →L[ℂ] H),
          A ∘SL T = T ∘SL A →
            (↑K).starProjection ∘SL T = T ∘SL (↑K).starProjection

theorem UnitaryRepresentation.exists_nontrivial_spectralSubspace_of_isSelfAdjoint_not_scalar.{u_2}
  {H : Type u_2} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] (A : H →L[ℂ] H)
  (hA : IsSelfAdjoint A)
  (hscalar :
    ¬∃ c,
        A =
          c •
            ContinuousLinearMap.id ℂ H) :
  ∃ K,
    K ≠ ⊥ ∧
      K ≠ ⊤ ∧
        ∀ (T : H →L[ℂ] H),
          A ∘SL T = T ∘SL A →
            (↑K).starProjection ∘SL T =
              T ∘SL (↑K).starProjection

The continuous-functional-calculus step in the infinite-dimensional self-adjoint spectral
theorem, in the form needed by Schur's lemma.

For the first cutoff `B` supplied above, take the closure `K` of its range. Nonzeroness of `B`
makes `K` nonzero. A second nonzero self-adjoint cutoff `C` with `B C = 0` supplies a nonzero vector
orthogonal to the range of `B`, so `K` is proper. Commutation with `A` preserves both `K` and its
orthogonal complement; hence it commutes with the orthogonal projection onto `K`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.exists_scalar_of_isSelfAdjoint_of_commutes.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) (hπ : π.IsTopologicallyIrreducible)
  (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (hcomm : π.Commutes A) :
  ∃ c, A = c • ContinuousLinearMap.id ℂ H

theorem UnitaryRepresentation.exists_scalar_of_isSelfAdjoint_of_commutes.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H)
  (hπ : π.IsTopologicallyIrreducible)
  (A : H →L[ℂ] H) (hA : IsSelfAdjoint A)
  (hcomm : π.Commutes A) :
  ∃ c, A = c • ContinuousLinearMap.id ℂ H

A self-adjoint member of the commutant of a topologically irreducible unitary representation
is scalar. This is the self-adjoint core of Schur's lemma.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.closedSubmodule_complex_eq_bot_or_top
  (K : ClosedSubmodule ℂ ℂ) : K = ⊥ ∨ K = ⊤

theorem UnitaryRepresentation.closedSubmodule_complex_eq_bot_or_top
  (K : ClosedSubmodule ℂ ℂ) :
  K = ⊥ ∨ K = ⊤

Every closed complex-linear subspace of the one-dimensional Hilbert space `ℂ` is zero or the
whole space.  This is the final fiberwise step in scalar instances of the Mackey correspondence.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

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

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

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

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

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

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

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

Joint-equivariant maps before analysis

Definition4.2.3

uses 0used by 1✓L∃∀N

The pointwise predicate. This layer assumes only group actions and contains no topology, measure, or integrability. It therefore exposes the algebra shared by all architectures without committing to a particular L^2 realization.

Lean code for Definition4.2.3●2 definitions

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

Implementation after :=

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

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

Lemma4.2.4

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 4.2.6

Loading preview

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

✓L∃∀N

Constructors. Fixed parameters recover ordinary equivariance, an arbitrary seed produces an orbit feature, and binary cascade preserves joint equivariance.

Lean code for Lemma4.2.4●5 declarations

theoremdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

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

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

Implementation after :=

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

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

theoremdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

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

defdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

Implementation after :=

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

Cascade composition of two parametrized feature maps.

theoremdefined in LeanRidgelet/HA/JointEquivariance.lean

complete

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

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

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

Induced L^2 representations and Bochner intertwiners

Definition4.2.5

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 4.2.6

Loading preview

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

✓L∃∀N

Measure layer. Mathlib's measure-preserving composition API gives the invariant-measure unitary representation on Lp. Folland's square-root Radon--Nikodym multiplier is defined and its group law follows from the cocycle. For the strongly quasi-invariant case, the withDensity lintegral formula proves norm preservation, Measure.QuasiMeasurePreserving controls representatives under composition, MemLp.toLp descends the action, and the inverse group element proves surjectivity. For a measurable unimodular multiplier cocycle, Mathlib's Lp multiplier isometry composes with this pullback; a.e. representative formulas prove the group law and give the corresponding character-twisted unitary representation.

Lean code for Definition4.2.5●16 declarations

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.quasiRegularAction.{u_1, u_2, u_3} {G : Type u_1}
  {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  (weight : G → X → ℂ) (g : G) (f : X → E) [SMul ℂ E] : X → E

def LeanRidgelet.quasiRegularAction.{u_1, u_2,
    u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  (weight : G → X → ℂ) (g : G) (f : X → E)
  [SMul ℂ E] : X → E

Implementation after :=

:=
  fun x ↦ weight g x • f (g⁻¹ • x)

The pointwise weighted pullback associated with a multiplier `weight`.

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

theorem LeanRidgelet.quasiRegularAction_mul.{u_1, u_2, u_3} {G : Type u_1}
  {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X] [AddMonoid E]
  [DistribMulAction ℂ E] (weight : G → X → ℂ)
  (h_mul :
    ∀ (g h : G) (x : X),
      weight (g * h) x = weight g x * weight h (g⁻¹ • x))
  (g h : G) (f : X → E) :
  LeanRidgelet.quasiRegularAction weight (g * h) f =
    LeanRidgelet.quasiRegularAction weight g
      (LeanRidgelet.quasiRegularAction weight h f)

theorem LeanRidgelet.quasiRegularAction_mul.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [AddMonoid E] [DistribMulAction ℂ E]
  (weight : G → X → ℂ)
  (h_mul :
    ∀ (g h : G) (x : X),
      weight (g * h) x =
        weight g x * weight h (g⁻¹ • x))
  (g h : G) (f : X → E) :
  LeanRidgelet.quasiRegularAction weight
      (g * h) f =
    LeanRidgelet.quasiRegularAction weight
      g
      (LeanRidgelet.quasiRegularAction
        weight h f)

The cocycle law is exactly the group law for weighted pullbacks.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

def LeanRidgelet.radonNikodymWeight.{u_1, u_2} {G : Type u_1} {X : Type u_2}
  [Group G] [MulAction G X] (jacobian : G → X → NNReal) (g : G)
  (x : X) : ℂ

def LeanRidgelet.radonNikodymWeight.{u_1, u_2}
  {G : Type u_1} {X : Type u_2} [Group G]
  [MulAction G X]
  (jacobian : G → X → NNReal) (g : G)
  (x : X) : ℂ

Implementation after :=

:=
  ((jacobian g (g⁻¹ • x)).sqrt : ℂ)⁻¹

Folland's square-root Radon--Nikodym multiplier
`φ(g, g⁻¹ • x)⁻¹/²`, with a positive cocycle represented in `ℝ≥0`.

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

theorem LeanRidgelet.radonNikodymWeight_mul.{u_1, u_2} {G : Type u_1}
  {X : Type u_2} [Group G] [MulAction G X] (jacobian : G → X → NNReal)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x = jacobian g (h • x) * jacobian h x)
  (g h : G) (x : X) :
  LeanRidgelet.radonNikodymWeight jacobian (g * h) x =
    LeanRidgelet.radonNikodymWeight jacobian g x *
      LeanRidgelet.radonNikodymWeight jacobian h (g⁻¹ • x)

theorem LeanRidgelet.radonNikodymWeight_mul.{u_1,
    u_2}
  {G : Type u_1} {X : Type u_2} [Group G]
  [MulAction G X]
  (jacobian : G → X → NNReal)
  (h_cocycle :
    ∀ (g h : G) (x : X),
      jacobian (g * h) x =
        jacobian g (h • x) * jacobian h x)
  (g h : G) (x : X) :
  LeanRidgelet.radonNikodymWeight jacobian
      (g * h) x =
    LeanRidgelet.radonNikodymWeight
        jacobian g x *
      LeanRidgelet.radonNikodymWeight
        jacobian h (g⁻¹ • x)

The Radon--Nikodym chain rule gives the multiplier cocycle used by the pointwise action.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

Implementation after :=

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

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

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

theorem LeanRidgelet.invariantLpUnitaryRepresentation_apply_ae.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SMulInvariantMeasure G X μ] [MeasurableConstSMul G X]
  (g : G) (f : ↥(MeasureTheory.Lp E 2 μ)) :
  ↑↑(↑(LeanRidgelet.invariantLpUnitaryRepresentation g) f) =ᵐ[μ] fun x ↦
    ↑↑f (g⁻¹ • x)

theorem LeanRidgelet.invariantLpUnitaryRepresentation_apply_ae.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SMulInvariantMeasure G X
      μ]
  [MeasurableConstSMul G X] (g : G)
  (f : ↥(MeasureTheory.Lp E 2 μ)) :
  ↑↑(↑(LeanRidgelet.invariantLpUnitaryRepresentation
              g)
          f) =ᵐ[μ]
    fun x ↦ ↑↑f (g⁻¹ • x)

The invariant-measure representation is represented a.e. by `f(g⁻¹ • x)`.

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

theorem LeanRidgelet.quasiRegularAction_lintegral_enorm_sq.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  {μ : MeasureTheory.Measure X} (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero : ∀ (g : G) (x : X), jacobian g x ≠ 0) (g : G)
  (f : X → E) :
  ∫⁻ (x : X),
      ‖LeanRidgelet.quasiRegularAction
            (LeanRidgelet.radonNikodymWeight jacobian) g f x‖ₑ ^
        2 ∂μ =
    ∫⁻ (x : X), ‖f x‖ₑ ^ 2 ∂μ

theorem LeanRidgelet.quasiRegularAction_lintegral_enorm_sq.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero :
    ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (g : G) (f : X → E) :
  ∫⁻ (x : X),
      ‖LeanRidgelet.quasiRegularAction
            (LeanRidgelet.radonNikodymWeight
              jacobian)
            g f x‖ₑ ^
        2 ∂μ =
    ∫⁻ (x : X), ‖f x‖ₑ ^ 2 ∂μ

The `withDensity` change-of-variables identity gives preservation of the squared extended norm
by the Radon--Nikodym-corrected pullback. No measurability of the vector-valued representative is
needed at this stage: the action is a measurable equivalence, and the density is finite.

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

theorem LeanRidgelet.quasiRegularAction_eLpNorm_two.{u_1, u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  {μ : MeasureTheory.Measure X} (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero : ∀ (g : G) (x : X), jacobian g x ≠ 0) (g : G)
  (f : X → E) :
  MeasureTheory.eLpNorm
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight jacobian) g f)
      2 μ =
    MeasureTheory.eLpNorm f 2 μ

theorem LeanRidgelet.quasiRegularAction_eLpNorm_two.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero :
    ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (g : G) (f : X → E) :
  MeasureTheory.eLpNorm
      (LeanRidgelet.quasiRegularAction
        (LeanRidgelet.radonNikodymWeight
          jacobian)
        g f)
      2 μ =
    MeasureTheory.eLpNorm f 2 μ

Folland's corrected pullback preserves the `L²` extended seminorm.

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

theorem LeanRidgelet.quasiRegularAction_memLp_two.{u_1, u_2, u_3} {G : Type u_1}
  {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  {μ : MeasureTheory.Measure X} (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero : ∀ (g : G) (x : X), jacobian g x ≠ 0) (g : G) (f : X → E)
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp
    (LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight jacobian) g f)
    2 μ

theorem LeanRidgelet.quasiRegularAction_memLp_two.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  {μ : MeasureTheory.Measure X}
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (h_ne_zero :
    ∀ (g : G) (x : X), jacobian g x ≠ 0)
  (g : G) (f : X → E)
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp
    (LeanRidgelet.quasiRegularAction
      (LeanRidgelet.radonNikodymWeight
        jacobian)
      g f)
    2 μ

The corrected pullback sends square-integrable representatives to square-integrable
representatives.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

Implementation after :=

:= (quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
    h_ne_zero g f (Lp.memLp f)).toLp _
  map_add' f k := by
    let hsum := quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
      h_ne_zero g (fun x ↦ (f + k) x) (Lp.memLp (f + k))
    let hf := quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
      h_ne_zero g (fun x ↦ f x) (Lp.memLp f)
    let hk := quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
      h_ne_zero g (fun x ↦ k x) (Lp.memLp k)
    change hsum.toLp _ = hf.toLp _ + hk.toLp _
    rw [← MemLp.toLp_add]
    apply MemLp.toLp_congr
    have hq := quasiMeasurePreserving_of_map_eq_withDensity jacobian h_measurable h_map g
    filter_upwards [hq.ae_eq (Lp.coeFn_add f k)] with x hx
    simp only [Function.comp_apply, Pi.add_apply] at hx
    simp only [quasiRegularAction, Pi.add_apply]
    rw [hx, smul_add]
  map_smul' c f := by
    let hcf := quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
      h_ne_zero g (fun x ↦ (c • f) x) (Lp.memLp (c • f))
    let hf := quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
      h_ne_zero g (fun x ↦ f x) (Lp.memLp f)
    change hcf.toLp _ = c • hf.toLp _
    rw [← MemLp.toLp_const_smul]
    apply MemLp.toLp_congr
    have hq := quasiMeasurePreserving_of_map_eq_withDensity jacobian h_measurable h_map g
    filter_upwards [hq.ae_eq (Lp.coeFn_smul c f)] with x hx
    simp only [Function.comp_apply, Pi.smul_apply] at hx
    simp only [quasiRegularAction, Pi.smul_apply]
    rw [hx]
    simp only [smul_smul]
    rw [mul_comm]
  norm_map' f := by
    let hf := quasiRegularAction_memLp_two jacobian h_measurable h_map h_jacobian
      h_ne_zero g (fun x ↦ f x) (Lp.memLp f)
    change ‖hf.toLp _‖ = ‖f‖
    calc
      ‖hf.toLp _‖ = ENNReal.toReal
          (eLpNorm (quasiRegularAction (radonNikodymWeight jacobian) g fun x ↦ f x) 2 μ) :=
        Lp.norm_toLp _ hf
      _ = ENNReal.toReal (eLpNorm (fun x ↦ f x) 2 μ) := congrArg ENNReal.toReal
        (quasiRegularAction_eLpNorm_two jacobian h_measurable h_map h_jacobian
          h_ne_zero g fun x ↦ f x)
      _ = ‖f‖ := (Lp.norm_def f).symm

Folland's corrected pullback, bundled as a linear isometry of the `L²` quotient.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

Implementation after :=

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

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

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

The quasi-invariant `L²` representation is represented a.e. by Folland's corrected pullback.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

Implementation after :=

:=
  (Unitary.linearIsometryEquiv
    (quasiInvariantLpUnitaryRepresentation jacobian h_measurable h_map h_jacobian
      h_ne_zero h_one h_cocycle g)).trans
    (unimodularMultiplierLinearIsometryEquiv (phase g)
      (h_phase_measurable g) (h_phase_norm g))

Compose the Radon--Nikodym-corrected pullback with a measurable unimodular multiplier.  This
is the operator underlying a character-twisted quasi-regular representation.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

Implementation after :=

:= twistedQuasiInvariantLpLinearIsometryEquiv jacobian h_measurable h_map
    h_jacobian h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm
  map_one' := by
    apply LinearIsometryEquiv.ext
    intro f
    apply Lp.ext
    have h := twistedQuasiInvariantLpLinearIsometryEquiv_apply_ae jacobian h_measurable
      h_map h_jacobian h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm 1 f
    filter_upwards [h] with x hx
    rw [hx]
    simp [h_phase_one, radonNikodymWeight, h_one]
  map_mul' g h := by
    apply LinearIsometryEquiv.ext
    intro f
    apply Lp.ext
    simp only [LinearIsometryEquiv.coe_mul, Function.comp_apply]
    have hgh := twistedQuasiInvariantLpLinearIsometryEquiv_apply_ae jacobian h_measurable
      h_map h_jacobian h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm
      (g * h) f
    have hh := twistedQuasiInvariantLpLinearIsometryEquiv_apply_ae jacobian h_measurable
      h_map h_jacobian h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm h f
    have hg := twistedQuasiInvariantLpLinearIsometryEquiv_apply_ae jacobian h_measurable
      h_map h_jacobian h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm g
      (twistedQuasiInvariantLpLinearIsometryEquiv jacobian h_measurable h_map h_jacobian
        h_ne_zero h_one h_cocycle phase h_phase_measurable h_phase_norm h f)
    have hqmp := quasiMeasurePreserving_of_map_eq_withDensity jacobian h_measurable h_map g
    have hhp := hqmp.ae_eq hh
    filter_upwards [hgh, hg, hhp] with x hghx hgx hhx
    rw [hghx, hgx]
    simp only [Function.comp_apply] at hhx
    rw [hhx]
    rw [h_phase_cocycle, radonNikodymWeight_mul jacobian h_cocycle]
    simp only [mul_inv_rev, mul_smul]
    ring

A unimodular multiplier cocycle upgrades the quasi-invariant isometries to a monoid
homomorphism.

defdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

Implementation after :=

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

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

theoremdefined in LeanRidgelet/HA/InducedRepresentation.lean

complete

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

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

The character-twisted representation has the expected phase-times-corrected-pullback
representative.

Lemma4.2.6

Statement uses 3

Statement dependency previews

Preview

Lemma 4.2.4

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 4.3.1

Loading preview

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

✓L∃∀N

Integral-to-operator bridge. Measure-preserving changes of variables give the invariant Bochner synthesis and ridgelet identities. For a strongly quasi-invariant measure, a general withDensity change-of-variables theorem inserts the Jacobian; its product with the inverse square-root representation weight leaves the complementary square root, which the explicit data/parameter balance identifies with the weight on the other side. Joint equivariance then turns both pointwise identities, and any bounded coordinate realization of them, into Mathlib continuous intertwining maps. A separate constructor starts with a bounded extension of the pointwise composite and proves that it is an endomorphism intertwiner without requiring either intermediate integral operator to be bounded.

Lean code for Lemma4.2.6●17 declarations

theoremdefined in LeanRidgelet/ToMathlib/QuasiInvariantIntegral.lean

complete

theorem MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]
  (μ : MeasureTheory.Measure X) (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g)) (g : G)
  (F : X → E) :
  ∫ (x : X), F x ∂μ = ∫ (x : X), jacobian g x • F (g • x) ∂μ

theorem MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  (μ : MeasureTheory.Measure X)
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (g : G) (F : X → E) :
  ∫ (x : X), F x ∂μ =
    ∫ (x : X), jacobian g x • F (g • x) ∂μ

A Bochner change-of-variables formula for a quasi-invariant measure. The hypothesis says
that pushforward by `x ↦ g⁻¹ • x` has density `jacobian g` with respect to `μ`; the conclusion
moves the action from the measure to the integrand and inserts that density as a real scalar.

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerSynthesis.{u_2, u_3, u_4} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [MeasurableSpace Ξ]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (μ : MeasureTheory.Measure Ξ) (φ : X → Ξ → Y) (γ : Ξ → ℂ) : X → Y

def LeanRidgelet.bochnerSynthesis.{u_2, u_3,
    u_4}
  {X : Type u_2} {Ξ : Type u_3}
  {Y : Type u_4} [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (μ : MeasureTheory.Measure Ξ)
  (φ : X → Ξ → Y) (γ : Ξ → ℂ) : X → Y

Implementation after :=

:=
  fun x ↦ ∫ ξ, γ ξ • φ x ξ ∂μ

Pointwise Bochner synthesis of a coefficient function against a feature map.

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

def LeanRidgelet.bochnerRidgelet.{u_2, u_3, u_4} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [MeasurableSpace X]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (μ : MeasureTheory.Measure X) (ψ : X → Ξ → Y) (f : X → Y) : Ξ → ℂ

def LeanRidgelet.bochnerRidgelet.{u_2, u_3,
    u_4}
  {X : Type u_2} {Ξ : Type u_3}
  {Y : Type u_4} [MeasurableSpace X]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (μ : MeasureTheory.Measure X)
  (ψ : X → Ξ → Y) (f : X → Y) : Ξ → ℂ

Implementation after :=

:=
  fun ξ ↦ ∫ x, ⟪ψ x ξ, f x⟫_ℂ ∂μ

Pointwise ridgelet pairing. Mathlib's inner product is linear in the second argument, so this
formula is linear in `f`.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

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

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

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

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

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

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

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

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Implementation after :=

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

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

defdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Implementation after :=

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

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

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Character-twisted form of `bochnerSynthesis_quasi_intertwines`. If the parameter Jacobian's
square root is the data-side Radon--Nikodym multiplier scaled by a group-dependent factor `chi g`,
then the Bochner synthesis integral intertwines the two quasi-invariant actions up to that same
factor. The scalar `chi` is valued in `ℂ` rather than in `ℝ≥0`: the balance equation, the
scalar multiplication on `Y` and the conclusion all already live in `ℂ`, so no coercion is
introduced, and `character_eq_one_of_balance_of_mul_self_eq_one` shows the hypothesis forces
`chi g` to be a nonnegative real anyway.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

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

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

Character-twisted form of `bochnerRidgelet_quasi_intertwines`. The twist enters the balance
hypothesis on the same side as in `bochnerSynthesis_quasi_intertwines_of_character`, because both
hypotheses say the same thing: the product
`(parameterJacobian g ξ).sqrt * (dataJacobian g x).sqrt` equals `chi g`. Consequently the factor
`chi g` again appears on the right-hand side, and not its inverse.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.bochnerReconstruction_quasi_intertwines_of_character.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [MeasurableSpace Ξ] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X) (υ : UnitaryRepresentation G Y)
  (φ ψ : X → Ξ → Y) (chi : G → ℂ) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_parameter_measurable : ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun ξ ↦ g⁻¹ • ξ) μParameter =
        μParameter.withDensity fun ξ ↦ ↑(parameterJacobian g ξ))
  (h_parameter_jacobian : ∀ (g : G), Measurable (parameterJacobian g))
  (h_parameter_ne_zero : ∀ (g : G) (ξ : Ξ), parameterJacobian g ξ ≠ 0)
  (h_data_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μData =
        μData.withDensity fun x ↦ ↑(dataJacobian g x))
  (h_data_jacobian : ∀ (g : G), Measurable (dataJacobian g))
  (h_data_ne_zero : ∀ (g : G) (x : X), dataJacobian g x ≠ 0)
  (h_joint_φ :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_joint_ψ :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_synthesis_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (parameterJacobian g ξ)) =
        chi g * LeanRidgelet.radonNikodymWeight dataJacobian g x)
  (h_ridgelet_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        chi g * LeanRidgelet.radonNikodymWeight parameterJacobian g ξ)
  (g : G) (f : X → Y) (x : X) :
  LeanRidgelet.bochnerSynthesis μParameter φ
      (LeanRidgelet.bochnerRidgelet μData ψ
        (LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g f))
      x =
    (chi g * chi g) •
      LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g
        (LeanRidgelet.bochnerSynthesis μParameter φ
          (LeanRidgelet.bochnerRidgelet μData ψ f))
        x

theorem LeanRidgelet.bochnerReconstruction_quasi_intertwines_of_character.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (φ ψ : X → Ξ → Y) (chi : G → ℂ)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_parameter_measurable :
    ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun ξ ↦ g⁻¹ • ξ) μParameter =
        μParameter.withDensity fun ξ ↦
          ↑(parameterJacobian g ξ))
  (h_parameter_jacobian :
    ∀ (g : G),
      Measurable (parameterJacobian g))
  (h_parameter_ne_zero :
    ∀ (g : G) (ξ : Ξ),
      parameterJacobian g ξ ≠ 0)
  (h_data_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μData =
        μData.withDensity fun x ↦
          ↑(dataJacobian g x))
  (h_data_jacobian :
    ∀ (g : G),
      Measurable (dataJacobian g))
  (h_data_ne_zero :
    ∀ (g : G) (x : X),
      dataJacobian g x ≠ 0)
  (h_joint_φ :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_joint_ψ :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_synthesis_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt
              (parameterJacobian g ξ)) =
        chi g *
          LeanRidgelet.radonNikodymWeight
            dataJacobian g x)
  (h_ridgelet_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        chi g *
          LeanRidgelet.radonNikodymWeight
            parameterJacobian g ξ)
  (g : G) (f : X → Y) (x : X) :
  LeanRidgelet.bochnerSynthesis μParameter
      φ
      (LeanRidgelet.bochnerRidgelet μData
        ψ
        (LeanRidgelet.quasiUnitaryPullbackAction
          dataJacobian υ g f))
      x =
    (chi g * chi g) •
      LeanRidgelet.quasiUnitaryPullbackAction
        dataJacobian υ g
        (LeanRidgelet.bochnerSynthesis
          μParameter φ
          (LeanRidgelet.bochnerRidgelet
            μData ψ f))
        x

The composite of the character-twisted ridgelet with the character-twisted synthesis, under
the hypotheses of `bochnerRidgelet_quasi_intertwines_of_character` and
`bochnerSynthesis_quasi_intertwines_of_character` for one common `chi`. Both steps contribute the
factor `chi g`, so the twists compound instead of cancelling and the composite carries
`chi g * chi g`.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.bochnerReconstruction_commutes_of_character.{u_1, u_2, u_3,
    u_4}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ] [MeasurableSpace X]
  [MeasurableSpace Ξ] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X) (υ : UnitaryRepresentation G Y)
  (φ ψ : X → Ξ → Y) (chi : G → ℂ) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_parameter_measurable : ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun ξ ↦ g⁻¹ • ξ) μParameter =
        μParameter.withDensity fun ξ ↦ ↑(parameterJacobian g ξ))
  (h_parameter_jacobian : ∀ (g : G), Measurable (parameterJacobian g))
  (h_parameter_ne_zero : ∀ (g : G) (ξ : Ξ), parameterJacobian g ξ ≠ 0)
  (h_data_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μData =
        μData.withDensity fun x ↦ ↑(dataJacobian g x))
  (h_data_jacobian : ∀ (g : G), Measurable (dataJacobian g))
  (h_data_ne_zero : ∀ (g : G) (x : X), dataJacobian g x ≠ 0)
  (h_joint_φ :
    ∀ (g : G) (x : X) (ξ : Ξ), φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_joint_ψ :
    ∀ (g : G) (x : X) (ξ : Ξ), ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_synthesis_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (parameterJacobian g ξ)) =
        chi g * LeanRidgelet.radonNikodymWeight dataJacobian g x)
  (h_ridgelet_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        chi g * LeanRidgelet.radonNikodymWeight parameterJacobian g ξ)
  (g : G) (h_chi : chi g * chi g = 1) (f : X → Y) (x : X) :
  LeanRidgelet.bochnerSynthesis μParameter φ
      (LeanRidgelet.bochnerRidgelet μData ψ
        (LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g f))
      x =
    LeanRidgelet.quasiUnitaryPullbackAction dataJacobian υ g
      (LeanRidgelet.bochnerSynthesis μParameter φ
        (LeanRidgelet.bochnerRidgelet μData ψ f))
      x

theorem LeanRidgelet.bochnerReconstruction_commutes_of_character.{u_1,
    u_2, u_3, u_4}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} {Y : Type u_4} [Group G]
  [MulAction G X] [MulAction G Ξ]
  [MeasurableSpace X] [MeasurableSpace Ξ]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (μParameter : MeasureTheory.Measure Ξ)
  (μData : MeasureTheory.Measure X)
  (υ : UnitaryRepresentation G Y)
  (φ ψ : X → Ξ → Y) (chi : G → ℂ)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_parameter_measurable :
    ∀ (g : G), Measurable fun ξ ↦ g • ξ)
  (h_parameter_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun ξ ↦ g⁻¹ • ξ) μParameter =
        μParameter.withDensity fun ξ ↦
          ↑(parameterJacobian g ξ))
  (h_parameter_jacobian :
    ∀ (g : G),
      Measurable (parameterJacobian g))
  (h_parameter_ne_zero :
    ∀ (g : G) (ξ : Ξ),
      parameterJacobian g ξ ≠ 0)
  (h_data_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_data_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μData =
        μData.withDensity fun x ↦
          ↑(dataJacobian g x))
  (h_data_jacobian :
    ∀ (g : G),
      Measurable (dataJacobian g))
  (h_data_ne_zero :
    ∀ (g : G) (x : X),
      dataJacobian g x ≠ 0)
  (h_joint_φ :
    ∀ (g : G) (x : X) (ξ : Ξ),
      φ (g • x) (g • ξ) = ↑(υ g) (φ x ξ))
  (h_joint_ψ :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ψ (g • x) (g • ξ) = ↑(υ g) (ψ x ξ))
  (h_synthesis_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt
              (parameterJacobian g ξ)) =
        chi g *
          LeanRidgelet.radonNikodymWeight
            dataJacobian g x)
  (h_ridgelet_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (dataJacobian g x)) =
        chi g *
          LeanRidgelet.radonNikodymWeight
            parameterJacobian g ξ)
  (g : G) (h_chi : chi g * chi g = 1)
  (f : X → Y) (x : X) :
  LeanRidgelet.bochnerSynthesis μParameter
      φ
      (LeanRidgelet.bochnerRidgelet μData
        ψ
        (LeanRidgelet.quasiUnitaryPullbackAction
          dataJacobian υ g f))
      x =
    LeanRidgelet.quasiUnitaryPullbackAction
      dataJacobian υ g
      (LeanRidgelet.bochnerSynthesis
        μParameter φ
        (LeanRidgelet.bochnerRidgelet
          μData ψ f))
      x

The composite of the twisted ridgelet with the twisted synthesis commutes with the data
action once the compounded twist `chi g * chi g` is trivial. This is the identity the
Schur/commutant argument consumes. The hypothesis `h_chi` is not automatic: by
`character_eq_one_of_balance_of_mul_self_eq_one` it already forces `chi g = 1`, so a genuinely
twisted feature does not become untwisted by composing synthesis with ridgelet.

theoremdefined in LeanRidgelet/HA/BochnerIntertwining.lean

complete

theorem LeanRidgelet.character_eq_one_of_balance_of_mul_self_eq_one.{u_1, u_2,
    u_3}
  {G : Type u_1} {X : Type u_2} {Ξ : Type u_3} [Group G] [MulAction G X]
  (chi : G → ℂ) (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_data_ne_zero : ∀ (g : G) (x : X), dataJacobian g x ≠ 0)
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt (parameterJacobian g ξ)) =
        chi g * LeanRidgelet.radonNikodymWeight dataJacobian g x)
  (g : G) (x : X) (ξ : Ξ) (h_chi : chi g * chi g = 1) : chi g = 1

theorem LeanRidgelet.character_eq_one_of_balance_of_mul_self_eq_one.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {Ξ : Type u_3} [Group G] [MulAction G X]
  (chi : G → ℂ)
  (dataJacobian : G → X → NNReal)
  (parameterJacobian : G → Ξ → NNReal)
  (h_data_ne_zero :
    ∀ (g : G) (x : X),
      dataJacobian g x ≠ 0)
  (h_balance :
    ∀ (g : G) (x : X) (ξ : Ξ),
      ↑↑(NNReal.sqrt
              (parameterJacobian g ξ)) =
        chi g *
          LeanRidgelet.radonNikodymWeight
            dataJacobian g x)
  (g : G) (x : X) (ξ : Ξ)
  (h_chi : chi g * chi g = 1) : chi g = 1

The twisted balance pins `chi g` down: it is the nonnegative real number
`(parameterJacobian g ξ).sqrt * (dataJacobian g (g⁻¹ • x)).sqrt`. Hence the cancellation
hypothesis `chi g * chi g = 1` of `bochnerReconstruction_commutes_of_character` holds only for
the untwisted value `chi g = 1`, which is the obstruction to removing a genuine density mismatch
by composing synthesis with ridgelet.

The balance hypothesis of the quasi-invariant identities — that the parameter density is the reciprocal of the data density — is exactly what the affine ridge feature satisfies and the quadratic feature of Section 7 does not. Replacing it by a balance up to a scalar character shows what goes wrong. Both the synthesis and the ridgelet then pick up the same factor, not reciprocal ones, because the factor is the product of the two square-root densities in either order; so the composite carries its square rather than cancelling it. Requiring that square to be one forces the character itself to be one, which is the exactly balanced case again, and that implication is proved here rather than asserted. The consequence is negative and worth recording: for a feature whose densities are out of balance, the composite of synthesis with ridgelet is not a commutant element of the data representation, and the reconstruction argument does not apply to it.