OAI/RepresentationTheory/Unitary/Basic.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CoordinateSweeps.UnitaryIrrep line 10

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:197 (same declaration text).

2. def OAI.CoordinateSweeps.UnitaryIrrep.asRepresentation line 22
3. lemma OAI.CoordinateSweeps.UnitaryIrrep.asRepresentation_apply line 25
4. instance OAI.CoordinateSweeps.UnitaryIrrep.asRepresentation_irreducible line 28
5. lemma OAI.CoordinateSweeps.UnitaryIrrep.character_asRepresentation line 40
6. theorem OAI.CoordinateSweeps.UnitaryIrrep.commuting_scalar line 46

   Source comment

   Schur's scalar-commutant statement with all irreducibility obligations proved directly from the exact source realization.

   theorem commuting_scalar (A : Matrix (Fin ρ.dimension) (Fin ρ.dimension) ℂ)
       (hA : ∀ g, A*ρ.matrix g=ρ.matrix g*A) : ∃ c : ℂ, A=c • (1 : Matrix _ _ ℂ) := by
   …

   Mentions: OAI.CoordinateSweeps.c

7. theorem OAI.CoordinateSweeps.UnitaryIrrep.character_norm line 66

   Source comment

   Character normalization in exactly the unnormalized trace convention.

   theorem character_norm :
       (Fintype.card Γ : ℂ)⁻¹ *
         ∑ g : Γ, Matrix.trace (ρ.matrix g)*Matrix.trace (ρ.matrix g⁻¹)=1 := by
   …

8. lemma OAI.CoordinateSweeps.UnitaryIrrep.matrix_inv line 80
9. def OAI.CoordinateSweeps.UnitaryIrrep.coefficient line 89

   Source comment

   Coefficients of the central isotypic projector, in unnormalized trace convention. They are derived from an actual irrep, not supplied as character data satisfying unproved orthogonality equations.

   def coefficient (g : Γ) : ℂ :=
   …

10. lemma OAI.CoordinateSweeps.UnitaryIrrep.coefficient_conj line 92
11. lemma OAI.CoordinateSweeps.UnitaryIrrep.coefficient_star line 98
12. def OAI.CoordinateSweeps.UnitaryIrrep.projector line 104
13. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_commute line 106
14. theorem OAI.CoordinateSweeps.UnitaryIrrep.projector_self line 116

    Source comment

    The isotypic projector acts as identity in its own irreducible.

    theorem projector_self : ρ.projector ρ.matrix=1 := by
    …

15. lemma OAI.CoordinateSweeps.UnitaryIrrep.coefficient_convolution line 134
16. theorem OAI.CoordinateSweeps.UnitaryIrrep.projector_idempotent line 147

    Source comment

    Idempotence in every genuine representation, including absent types.

    theorem projector_idempotent (τ : Γ →* A) : ρ.projector τ * ρ.projector τ=ρ.projector τ := by
    …

17. theorem OAI.CoordinateSweeps.UnitaryIrrep.projector_hermitian line 170
18. theorem OAI.CoordinateSweeps.UnitaryIrrep.projector_posSemidef line 177
19. def OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation line 193
20. lemma OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation_character line 197
21. lemma OAI.CoordinateSweeps.UnitaryIrrep.character_sum_multiplicity line 201
22. lemma OAI.CoordinateSweeps.UnitaryIrrep.sum_trace_norm_sq line 219
23. lemma OAI.CoordinateSweeps.UnitaryIrrep.irrep_sum_trace_norm_sq line 239
24. theorem OAI.CoordinateSweeps.UnitaryIrrep.multiplicity_sq_le_commutant line 255

    Source comment

    No decomposition/classification hypothesis is needed for this character Cauchy--Schwarz bound. It applies also to absent types (multiplicity zero).

    theorem multiplicity_sq_le_commutant (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (hu : ∀ g, (τ g).conjTranspose=τ g⁻¹) :
        (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (matrixRepresentation τ)))^2 ≤
          Module.finrank ℂ ((matrixRepresentation τ).IntertwiningMap (matrixRepresentation τ)) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation

25. lemma OAI.CoordinateSweeps.UnitaryIrrep.central_sum_commute line 302
26. lemma OAI.CoordinateSweeps.UnitaryIrrep.trace_conj line 311
27. lemma OAI.CoordinateSweeps.UnitaryIrrep.central_character_operator line 315
28. theorem OAI.CoordinateSweeps.UnitaryIrrep.projector_twisted_trace line 342

    Source comment

    Exact projected character, with the genuine Hom-space multiplicity.

    theorem projector_twisted_trace (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ) (k : Γ) :
        Matrix.trace (ρ.projector τ*τ k) =
          (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (matrixRepresentation τ)) : ℂ) *
            Matrix.trace (ρ.matrix k) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation

29. theorem OAI.CoordinateSweeps.UnitaryIrrep.projector_lift_trace line 384

    Source comment

    The projected trace formula applies to actual elements of the group algebra, not just to individual group elements.

    theorem projector_lift_trace (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (x : MonoidAlgebra ℂ Γ) :
        Matrix.trace (ρ.projector τ*((MonoidAlgebra.lift ℂ _ Γ) τ x)) =
          (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (matrixRepresentation τ)) : ℂ) *
            Matrix.trace ((MonoidAlgebra.lift ℂ _ Γ) ρ.matrix x) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation

30. def OAI.CoordinateSweeps.UnitaryIrrep.averageMatrix line 396

    Source comment

    Literal finite averages and their adjoints have the same group-algebra word in every unitary representation.

    def averageMatrix {Ω : Type*} [Fintype Ω] (τ : Γ →* Matrix n n ℂ)
        (w : Ω → ℂ) (g : Ω → Γ) : Matrix n n ℂ := ∑ ω, w ω • τ (g ω)

31. def OAI.CoordinateSweeps.UnitaryIrrep.averageAlgebra line 399
32. lemma OAI.CoordinateSweeps.UnitaryIrrep.lift_averageAlgebra line 403
33. lemma OAI.CoordinateSweeps.UnitaryIrrep.averageMatrix_star line 409
34. theorem OAI.CoordinateSweeps.UnitaryIrrep.projected_average_moment line 416

    Source comment

    Exact unnormalized even moment trace on a genuine isotypic component.

    theorem projected_average_moment {Ω : Type*} [Fintype Ω]
        (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (hu : ∀ g, (τ g).conjTranspose=τ g⁻¹) (w : Ω → ℂ) (g : Ω → Γ) (q : ℕ) :
        Matrix.trace (ρ.projector τ*((averageMatrix τ w g).conjTranspose*averageMatrix τ w g)^q) =
          (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (matrixRepresentation τ)) : ℂ) *
            Matrix.trace (((averageMatrix ρ.matrix w g).conjTranspose*averageMatrix ρ.matrix w g)^q) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.UnitaryIrrep.averageMatrix, OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation

35. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_commute_average line 433
36. lemma OAI.CoordinateSweeps.UnitaryIrrep.trace_positive_product line 440
37. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_complement_posSemidef line 446
38. theorem OAI.CoordinateSweeps.UnitaryIrrep.multiplicity_moment_le line 456

    Source comment

    Genuine occurrence gives a lower bound for the encompassing unnormalized moment, with its actual Hom multiplicity and no missing dimension factor.

    theorem multiplicity_moment_le {Ω : Type*} [Fintype Ω]
        (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (hu : ∀ g, (τ g).conjTranspose=τ g⁻¹) (w : Ω → ℂ) (g : Ω → Γ) (q : ℕ) :
        (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (matrixRepresentation τ)) : ℝ) *
          (Matrix.trace (((averageMatrix ρ.matrix w g).conjTranspose*averageMatrix ρ.matrix w g)^q)).re ≤
            (Matrix.trace (((averageMatrix τ w g).conjTranspose*averageMatrix τ w g)^q)).re := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation, OAI.CoordinateSweeps.UnitaryIrrep.averageMatrix

39. theorem OAI.CoordinateSweeps.UnitaryIrrep.projected_operator_moment line 470

    Source comment

    The Schatten moment of the projected average, rather than merely an inserted projector in the trace, is exactly the same multiplicity formula.

    theorem projected_operator_moment {Ω : Type*} [Fintype Ω]
        (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (hu : ∀ g, (τ g).conjTranspose=τ g⁻¹) (w : Ω → ℂ) (g : Ω → Γ) {q : ℕ} (hq : q ≠ 0) :
        Matrix.trace (((ρ.projector τ*averageMatrix τ w g).conjTranspose*
          (ρ.projector τ*averageMatrix τ w g))^q) =
          (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (matrixRepresentation τ)) : ℂ) *
            Matrix.trace (((averageMatrix ρ.matrix w g).conjTranspose*averageMatrix ρ.matrix w g)^q) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.UnitaryIrrep.averageMatrix, OAI.CoordinateSweeps.UnitaryIrrep.matrixRepresentation

40. def OAI.CoordinateSweeps.UnitaryIrrep.pullback line 506
41. lemma OAI.CoordinateSweeps.UnitaryRealization.gram_posDef line 529

    Source comment

    Gram averaging produces the invariant positive form directly from the finite action; no invariant inner product is postulated.

    lemma gram_posDef (τ : G →* Matrix J J ℂ) :
        (∑ g, (τ g).conjTranspose * τ g).PosDef := by
    …

42. lemma OAI.CoordinateSweeps.UnitaryRealization.gram_invariant line 538
43. theorem OAI.CoordinateSweeps.UnitaryRealization.unitarize line 552

    Source comment

    Actual conjugating matrices and a unitary action for any finite complex matrix representation.

    theorem unitarize (τ : G →* Matrix J J ℂ) :
        ∃ A B : Matrix J J ℂ, A*B=1 ∧ B*A=1 ∧ A.IsHermitian ∧ B.IsHermitian ∧
          (∀ g, (B*τ g*A).conjTranspose*(B*τ g*A)=1) := by
    …

44. theorem OAI.CoordinateSweeps.UnitaryRealization.exists_unitary line 581

    Source comment

    A genuine irreducible representation has a unitary finite matrix realization, with the intertwining equivalence retained.

    theorem exists_unitary (σ : Representation ℂ G V) [σ.IsIrreducible] :
        ∃ ρ : UnitaryIrrep G, Nonempty (Representation.Equiv σ ρ.asRepresentation) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep

45. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_other line 652
46. lemma OAI.CoordinateSweeps.UnitaryIrrep.cross_convolution line 677
47. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_orthogonal line 689
48. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_intertwiner line 705
49. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_matrix_asRepresentation line 713