Issues

• [External] Compact self-adjoint spectral theorem (Mathlib gap)

  chapter:spectralexternal:mathlib-gap
  JonCYeh/peter-weyl-lean#49 · Filter by author JonCYeh opened on May 7, 2026

• [External] Adjoint of a compact operator is compact (Schauder, Mathlib gap)

  chapter:convchapter:schurexternal:mathlib-gap
  JonCYeh/peter-weyl-lean#48 · Filter by author JonCYeh opened on May 7, 2026

• [Cluster] Ch.8 Separating irreducibles: downstream wiring of Chs. 2/3/4

  chapter:separatingpriority:p3type:cluster
  JonCYeh/peter-weyl-lean#47 · Filter by author JonCYeh opened on May 7, 2026

• [Cluster] Ch.7 Matrix coefficients: tensor and contragredient representations

  area:tensorchapter:matrixpriority:p2type:cluster
  JonCYeh/peter-weyl-lean#46 · Filter by author JonCYeh opened on May 7, 2026

• [Cluster] Ch.3 Convolution: Fubini and change-of-variables on L²(G)

  area:fubinichapter:convpriority:p1type:cluster
  JonCYeh/peter-weyl-lean#45 · Filter by author JonCYeh opened on May 7, 2026

• [Cluster] Ch.2 Regular representations: dense extension of translation from C(G) to L²(G)

  area:dense-extensionchapter:reppriority:p1type:cluster
  JonCYeh/peter-weyl-lean#44 · Filter by author JonCYeh opened on May 7, 2026

• [Cluster] Ch.11 Isotypic decomposition + Plancherel

  area:bochnerarea:hilbert-sumchapter:isotypicpriority:p1type:cluster
  JonCYeh/peter-weyl-lean#43 · Filter by author JonCYeh opened on May 7, 2026

• [Cluster] Ch.10 Schur orthogonality: Bochner integration scaffolding

  area:bochnerchapter:orthogpriority:p1type:cluster
  JonCYeh/peter-weyl-lean#42 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-plancherel-isotypic] Plancherel: per-isotypic norm sum

  area:bochnerchapter:isotypictype:atomic
  JonCYeh/peter-weyl-lean#41 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-PW-HilbertSum] L^2(G) is the Hilbert sum of isotypic components

  area:bochnerchapter:isotypictype:atomic
  JonCYeh/peter-weyl-lean#40 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-isotypic-spans] Closed sum of isotypic components is dense

  area:bochnerchapter:isotypictype:atomic
  JonCYeh/peter-weyl-lean#39 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-mc-in-isotypic] Matrix coefficients of \rho_\xi live in L^2(G)_\xi

  area:bochnerchapter:isotypictype:atomic
  JonCYeh/peter-weyl-lean#38 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-isotypic-orthog] Distinct isotypic components are orthogonal

  area:bochnerchapter:isotypictype:atomic
  JonCYeh/peter-weyl-lean#37 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-isotypic-invariant] L^2(G)_\xi is \rho^R-invariant

  area:bochnerchapter:isotypictype:atomic
  JonCYeh/peter-weyl-lean#36 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-mc-orthog-same] Inner product of matrix coefficients of same irreducible

  area:bochnerchapter:orthogtype:atomic
  JonCYeh/peter-weyl-lean#35 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-mc-orthog-distinct] Inner product of matrix coefficients across distinct irreducibles

  area:bochnerchapter:orthogtype:atomic
  JonCYeh/peter-weyl-lean#34 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-fd-irr-nontrivial] Finite-dim invariant non-trivial action splits to non-trivial irreducible action

  chapter:separatingtype:atomic
  JonCYeh/peter-weyl-lean#33 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-eigenspace-separates] T_\phi has a non-zero finite-dim eigenspace separating g_0

  chapter:separatingtype:atomic
  JonCYeh/peter-weyl-lean#32 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-existsSepConv] Existence of separating self-adjoint convolution operator

  chapter:separatingtype:atomic
  JonCYeh/peter-weyl-lean#31 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-rightReg-faithful] Right regular action is faithful

  chapter:separatingtype:atomic
  JonCYeh/peter-weyl-lean#30 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-mc-conj] Conjugate of a matrix coefficient

  area:tensorchapter:matrixtype:atomic
  JonCYeh/peter-weyl-lean#29 · Filter by author JonCYeh opened on May 7, 2026

• [def:c2-contragredient] Contragredient (dual) representation

  area:tensorchapter:matrixtype:atomic
  JonCYeh/peter-weyl-lean#28 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-mc-mul] Product of matrix coefficients

  area:tensorchapter:matrixtype:atomic
  JonCYeh/peter-weyl-lean#27 · Filter by author JonCYeh opened on May 7, 2026

• [def:c2-tensor-rep] Tensor product of unitary reps

  area:tensorchapter:matrixtype:atomic
  JonCYeh/peter-weyl-lean#26 · Filter by author JonCYeh opened on May 7, 2026

• [thm:c2-mc-sum] Sum of matrix coefficients is a matrix coefficient

  area:tensorchapter:matrixtype:atomic
  JonCYeh/peter-weyl-lean#25 · Filter by author JonCYeh opened on May 7, 2026