@[reducible, inline]

abbrev SL2C : Type

structure SL2C_UnitaryRep : Type (u_1 + 1)

• V : Type u_1
• instNACG : NormedAddCommGroup self.V
• instIPS : InnerProductSpace ℂ self.V
• instCS : CompleteSpace self.V
• action : SL2C →* self.V ≃ₗᵢ[ℂ] self.V

def SL2C_UnitaryRep.IsIrreducible (ρ : SL2C_UnitaryRep) : Prop

def SL2C_UnitaryRep.IsUnitarilyEquiv (ρ₁ : SL2C_UnitaryRep) (ρ₂ : SL2C_UnitaryRep) : Prop

noncomputable def trivialSL2CRep : SL2C_UnitaryRep

structure PSActionBundle : Type

• action : ℤ → ℝ → SL2C →* ↥(lp (fun (x : ℕ) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ℕ) => ℂ) 2)
• symm (m : ℤ) (t : ℝ) : self.action m t = self.action (-m) (-t)

structure CSActionBundle : Type

• action (s : ℝ) : -1 < s → s < 1 → SL2C →* ↥(lp (fun (x : ℕ) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ℕ) => ℂ) 2)
• symm (s : ℝ) (hs1 : -1 < s) (hs2 : s < 1) (hs1' : -1 < -s) (hs2' : -s < 1) : self.action s hs1 hs2 = self.action (-s) hs1' hs2'

theorem gn_analytical_data : ∃ (ps : PSActionBundle) (cs : CSActionBundle), (∀ (m₁ m₂ : ℤ) (t₁ t₂ : ℝ), (∃ (T : ↥(lp (fun (x : ℕ) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ℕ) => ℂ) 2)), ∀ (g : SL2C) (v : ↥(lp (fun (x : ℕ) => ℂ) 2)), T (((ps.action m₁ t₁) g) v) = ((ps.action m₂ t₂) g) (T v)) → m₁ = m₂ ∧ t₁ = t₂ ∨ m₁ = -m₂ ∧ t₁ = -t₂) ∧ (∀ (s₁ s₂ : ℝ) (hs₁_neg : -1 < s₁) (hs₁_pos : s₁ < 1) (hs₂_neg : -1 < s₂) (hs₂_pos : s₂ < 1), (∃ (T : ↥(lp (fun (x : ℕ) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ℕ) => ℂ) 2)), ∀ (g : SL2C) (v : ↥(lp (fun (x : ℕ) => ℂ) 2)), T (((cs.action s₁ hs₁_neg hs₁_pos) g) v) = ((cs.action s₂ hs₂_neg hs₂_pos) g) (T v)) → s₁ = s₂ ∨ s₁ = -s₂) ∧ (∀ (m : ℤ) (t s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1), ¬∃ (T : ↥(lp (fun (x : ℕ) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ℕ) => ℂ) 2)), ∀ (g : SL2C) (v : ↥(lp (fun (x : ℕ) => ℂ) 2)), T (((ps.action m t) g) v) = ((cs.action s hs_neg hs_pos) g) (T v)) ∧ ∀ (ρ : SL2C_UnitaryRep), ρ.IsIrreducible → (∃ (m : ℤ) (t : ℝ), ρ.IsUnitarilyEquiv { V := ↥(lp (fun (x : ℕ) => ℂ) 2), instNACG := lp.normedAddCommGroup, instIPS := lp.instInnerProductSpace, instCS := ⋯, action := ps.action m t }) ∨ (∃ (s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1), ρ.IsUnitarilyEquiv { V := ↥(lp (fun (x : ℕ) => ℂ) 2), instNACG := lp.normedAddCommGroup, instIPS := lp.instInnerProductSpace, instCS := ⋯, action := cs.action s hs_neg hs_pos }) ∨ ρ.IsUnitarilyEquiv trivialSL2CRep

noncomputable def thePSAction : PSActionBundle

noncomputable def theCSAction : CSActionBundle

noncomputable def unitaryPrincipalSeriesRep (m : ℤ) (t : ℝ) : SL2C_UnitaryRep

noncomputable def complementarySeriesRep (s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1) : SL2C_UnitaryRep

theorem gelfand_naimark_exhaustion (ρ : SL2C_UnitaryRep) (hirr : ρ.IsIrreducible) : (∃ (m : ℤ) (t : ℝ), ρ.IsUnitarilyEquiv (unitaryPrincipalSeriesRep m t)) ∨ (∃ (s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1), ρ.IsUnitarilyEquiv (complementarySeriesRep s hs_neg hs_pos)) ∨ ρ.IsUnitarilyEquiv trivialSL2CRep

theorem gelfand_naimark_ps_injective (m₁ m₂ : ℤ) (t₁ t₂ : ℝ) (h : (unitaryPrincipalSeriesRep m₁ t₁).IsUnitarilyEquiv (unitaryPrincipalSeriesRep m₂ t₂)) : m₁ = m₂ ∧ t₁ = t₂ ∨ m₁ = -m₂ ∧ t₁ = -t₂

theorem gelfand_naimark_cs_injective (s₁ s₂ : ℝ) (hs₁_neg : -1 < s₁) (hs₁_pos : s₁ < 1) (hs₂_neg : -1 < s₂) (hs₂_pos : s₂ < 1) (h : (complementarySeriesRep s₁ hs₁_neg hs₁_pos).IsUnitarilyEquiv (complementarySeriesRep s₂ hs₂_neg hs₂_pos)) : s₁ = s₂ ∨ s₁ = -s₂

theorem gelfand_naimark_ps_cs_disjoint (m : ℤ) (t s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1) : ¬(unitaryPrincipalSeriesRep m t).IsUnitarilyEquiv (complementarySeriesRep s hs_neg hs_pos)

theorem lp_single_linearIndependent : LinearIndependent ℂ fun (i : ℕ) => lp.single 2 i 1

theorem lp_not_finiteDimensional : ¬FiniteDimensional ℂ ↥(lp (fun (x : ℕ) => ℂ) 2)

theorem no_liso_lp_complex : IsEmpty (↥(lp (fun (x : ℕ) => ℂ) 2) ≃ₗᵢ[ℂ] ℂ)

theorem gelfand_naimark_classification : (∀ (ρ : SL2C_UnitaryRep), ρ.IsIrreducible → (∃ (m : ℤ) (t : ℝ), ρ.IsUnitarilyEquiv (unitaryPrincipalSeriesRep m t)) ∨ (∃ (s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1), ρ.IsUnitarilyEquiv (complementarySeriesRep s hs_neg hs_pos)) ∨ ρ.IsUnitarilyEquiv trivialSL2CRep) ∧ (∀ (m₁ m₂ : ℤ) (t₁ t₂ : ℝ), (unitaryPrincipalSeriesRep m₁ t₁).IsUnitarilyEquiv (unitaryPrincipalSeriesRep m₂ t₂) → m₁ = m₂ ∧ t₁ = t₂ ∨ m₁ = -m₂ ∧ t₁ = -t₂) ∧ (∀ (s₁ s₂ : ℝ) (hs₁_neg : -1 < s₁) (hs₁_pos : s₁ < 1) (hs₂_neg : -1 < s₂) (hs₂_pos : s₂ < 1), (complementarySeriesRep s₁ hs₁_neg hs₁_pos).IsUnitarilyEquiv (complementarySeriesRep s₂ hs₂_neg hs₂_pos) → s₁ = s₂ ∨ s₁ = -s₂) ∧ ∀ (m : ℤ) (t s : ℝ) (hs_neg : -1 < s) (hs_pos : s < 1), ¬(unitaryPrincipalSeriesRep m t).IsUnitarilyEquiv (complementarySeriesRep s hs_neg hs_pos)

structure HCBimoduleParam : Type

• mu : ℂ
• lam : ℂ
• diff_is_int : ∃ (n : ℤ), self.lam - self.mu = ↑n

def HCBimoduleParam.Equiv (ξ₁ ξ₂ : HCBimoduleParam) : Prop

def HCBimoduleParam.neg (ξ : HCBimoduleParam) : HCBimoduleParam

def HCBimoduleParam.IsSameSignNonzeroIntegers (ξ : HCBimoduleParam) : Prop

def principalSeriesKTypes (k : ℤ) : Set ℕ

theorem prop_26_1_i (ξ₁ ξ₂ : HCBimoduleParam) (h₁ : ¬ξ₁.IsSameSignNonzeroIntegers) (h₂ : ¬ξ₂.IsSameSignNonzeroIntegers) (h_chi_left : ξ₁.lam ^ 2 = ξ₂.lam ^ 2) (h_chi_right : ξ₁.mu ^ 2 = ξ₂.mu ^ 2) : ξ₁.Equiv ξ₂

def IsHermitianPS (lam mu : ℂ) : Prop

inductive SL2C_IrredAdmissible : Type

• finiteDim (n : ℕ) : SL2C_IrredAdmissible
• principalSeries (lam mu : ℂ) (h_diff : ∃ (k : ℤ), mu - lam = ↑k) : SL2C_IrredAdmissible

def SL2C_IrredAdmissible.kTypes : SL2C_IrredAdmissible → Set ℕ