The core transfer component of the Connes rigidity formalization.

@[simp]

theorem Connes.OpenAIPort.l2Reindex_apply {α : Type u} {β : Type v} (e : α ≃ β) (f : ↥(GroupL2 α)) (j : β) : ↑((l2Reindex e) f) j = ↑f (e.symm j)

Public OpenAI reindexing computation. Paper: §3.

@[simp]

theorem Connes.OpenAIPort.l2Reindex_symm {α : Type u} {β : Type v} (e : α ≃ β) : (l2Reindex e).symm = l2Reindex e.symm

Public OpenAI reindexing symmetry. Paper: §3.

@[simp]

theorem Connes.OpenAIPort.leftRegularUnitary_apply {G : Type u} [Group G] (g : G) (f : ↥(GroupL2 G)) (h : G) : ↑(↑(leftRegularUnitary g) f) h = ↑f (g⁻¹ * h)

Public OpenAI left-regular computation. Paper: §3.

theorem Connes.OpenAIPort.hasAlmostInvariantUnitVectors_comp {G H : Type u} {K : Type v} [Group G] [Group H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (π : UnitaryRepresentation H K) (f : G →* H) (hπ : π.HasAlmostInvariantUnitVectors) : UnitaryRepresentation.HasAlmostInvariantUnitVectors (MonoidHom.comp π f)

Public OpenAI transfer of almost-invariant vectors. Paper: §4.

theorem Connes.OpenAIPort.hasKazhdanPropertyT_of_surjective (G H : CountableDiscreteGroup) (f : G.Carrier →* H.Carrier) (hf : Function.Surjective ⇑f) (hG : HasKazhdanPropertyT G) : HasKazhdanPropertyT H

Public OpenAI property-(T) quotient transfer. Paper: §4.

theorem Connes.OpenAIPort.hasKazhdanPropertyT_iff_of_mulEquiv (G H : CountableDiscreteGroup) (e : G.Carrier ≃* H.Carrier) : HasKazhdanPropertyT G ↔ HasKazhdanPropertyT H

Public OpenAI property-(T) transport across a group equivalence. Paper: §4.