def SL2IrredGKModule.principalSeriesParamSq : SL2IrredGKModule → ℂ

def SL2IrredGKModule.IsBargmannUnitary (μ : SL2IrredGKModule) : Prop

inductive SL2UnitaryIrred : Type

• discreteSeriesPlus (m : ℕ) (hm : m ≥ 1) : SL2UnitaryIrred
• discreteSeriesMinus (m : ℕ) (hm : m ≥ 1) : SL2UnitaryIrred
• unitaryPrincipalSeries (t : ℝ) (ε : ZMod 2) (hirred : t ≠ 0 ∨ ε = 0) : SL2UnitaryIrred
• complementarySeries (s : ℝ) (hs_ne : s ≠ 0) (hs_sq : s ^ 2 < 1) : SL2UnitaryIrred
• trivial : SL2UnitaryIrred

def SL2UnitaryIrred.toIrredGKModule : SL2UnitaryIrred → SL2IrredGKModule

theorem int_sq_ge_one_of_ne_zero (k : ℤ) (hk : k ≠ 0) : 1 ≤ k ^ 2

theorem complex_sq_im_zero (ν : ℂ) (h : (ν ^ 2).im = 0) : ν.re = 0 ∨ ν.im = 0

theorem zmod2_ne_zero_eq_one (ε : ZMod 2) (h : ε ≠ 0) : ε = 1

theorem bargmann_classification (μ : SL2IrredGKModule) : μ.IsBargmannUnitary ↔ ∃ (ν : SL2UnitaryIrred), ν.toIrredGKModule = μ

theorem theorem_9_3_gelfand_naimark_bargmann (μ : SL2IrredGKModule) : μ.IsBargmannUnitary ↔ ∃ (ν : SL2UnitaryIrred), ν.toIrredGKModule = μ

theorem unitaryPrincipalSeries_neg_kTypes (t : ℝ) (ε : ZMod 2) (h : t ≠ 0 ∨ ε = 0) (h' : -t ≠ 0 ∨ ε = 0) : (SL2UnitaryIrred.unitaryPrincipalSeries t ε h).toIrredGKModule.kTypes = (SL2UnitaryIrred.unitaryPrincipalSeries (-t) ε h').toIrredGKModule.kTypes

theorem unitaryPrincipalSeries_neg_paramSq (t : ℝ) (ε : ZMod 2) (h : t ≠ 0 ∨ ε = 0) (h' : -t ≠ 0 ∨ ε = 0) : (SL2UnitaryIrred.unitaryPrincipalSeries t ε h).toIrredGKModule.principalSeriesParamSq = (SL2UnitaryIrred.unitaryPrincipalSeries (-t) ε h').toIrredGKModule.principalSeriesParamSq