GroupTrace.lean`

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.UltrapowerBridge.Ell2 line 17
abbrev OAI.UltrapowerBridge.Operator line 18
abbrev OAI.UltrapowerBridge.reindexVector line 20
Source documentation
Reindex a square-summable vector by a permutation.
```
abbrev reindexVector {G : Type*} (e : G ≃ G) (f : Ell2 G) : Ell2 G :=
…
```
Mentions: OAI.UltrapowerBridge.Ell2
theorem OAI.UltrapowerBridge.reindexVector_apply line 23
theorem OAI.UltrapowerBridge.reindexVector_norm line 26
abbrev OAI.UltrapowerBridge.reindex line 31
Source documentation
The bounded unitary implementation of a permutation on ell2.
```
abbrev reindex {G : Type*} (e : G ≃ G) : Ell2 G ≃ₗᵢ[ℂ] Ell2 G :=
…
```
Mentions: OAI.UltrapowerBridge.Ell2
abbrev OAI.UltrapowerBridge.leftRegular line 35
Source documentation
The left regular operator, constructed on every square-summable vector.
```
abbrev leftRegular {G : Type*} [Group G] (g : G) : Ell2 G →L[ℂ] Ell2 G :=
…
```
Mentions: OAI.UltrapowerBridge.Ell2
theorem OAI.UltrapowerBridge.leftRegular_apply line 38
theorem OAI.UltrapowerBridge.leftRegular_one line 41
theorem OAI.UltrapowerBridge.leftRegular_mul line 45
theorem OAI.UltrapowerBridge.leftRegular_norm_vector line 50
abbrev OAI.UltrapowerBridge.regularOperators line 55
abbrev OAI.UltrapowerBridge.groupAlgebra line 56
def OAI.UltrapowerBridge.delta line 59
def OAI.UltrapowerBridge.trace line 62
theorem OAI.UltrapowerBridge.leftRegular_trace line 64
theorem OAI.UltrapowerBridge.leftRegular_star line 71
def OAI.UltrapowerBridge.rightRegular line 80
Source documentation
Right translations, needed to prove that the identity vector is separating.
```
def rightRegular {G : Type*} [Group G] (g : G) : Ell2 G →L[ℂ] Ell2 G :=
…
```
Mentions: OAI.UltrapowerBridge.Ell2
theorem OAI.UltrapowerBridge.rightRegular_apply line 83
theorem OAI.UltrapowerBridge.left_right_commute line 86
theorem OAI.UltrapowerBridge.regularOperators_star line 91
theorem OAI.UltrapowerBridge.groupAlgebra_carrier line 103
Source documentation
Exact equality with the manuscript's plain double commutant of lambda(G).
```
theorem groupAlgebra_carrier (G : Type*) [Group G] :
    (groupAlgebra G : Set (Operator G)) =
      Set.centralizer (Set.centralizer (regularOperators G)) := by
…
```
Mentions: OAI.UltrapowerBridge.groupAlgebra, OAI.UltrapowerBridge.Operator, OAI.UltrapowerBridge.regularOperators
abbrev OAI.UltrapowerBridge.concreteGroupAlgebra line 111
Source documentation
The target algebra actually satisfies mathlib's concrete von Neumann algebra definition.
```
abbrev concreteGroupAlgebra (G : Type*) [Group G] : VonNeumannAlgebra (Ell2 G) :=
…
```
Mentions: OAI.UltrapowerBridge.Ell2
theorem OAI.UltrapowerBridge.rightRegular_mem_commutant line 114
theorem OAI.UltrapowerBridge.algebra_right_commute line 122
theorem OAI.UltrapowerBridge.rightRegular_delta line 132
theorem OAI.UltrapowerBridge.delta_separating line 140
Source documentation
Fourier coefficients at the identity separate all elements of the group algebra, by commuting with right translations and using the density of finitely supported vectors.
```
theorem delta_separating (G : Type*) [Group G] (T : groupAlgebra G)
    (hT : (T : Operator G) (delta G) = 0) : T = 0 := by
…
```
Mentions: OAI.UltrapowerBridge.groupAlgebra, OAI.UltrapowerBridge.Operator, OAI.UltrapowerBridge.delta
theorem OAI.UltrapowerBridge.trace_star_mul_self line 161
Source documentation
The canonical vector functional evaluated on a positive square.
```
theorem trace_star_mul_self (G : Type*) [Group G] (T : groupAlgebra G) :
    trace G (star T * T) =
      inner ℂ ((T : Operator G) (delta G))
        ((T : Operator G) (delta G)) := by
…
```
Mentions: OAI.UltrapowerBridge.groupAlgebra, OAI.UltrapowerBridge.trace, OAI.UltrapowerBridge.Operator, OAI.UltrapowerBridge.delta
theorem OAI.UltrapowerBridge.trace_faithful line 169
Source documentation
Faithfulness of the canonical vector trace.
```
theorem trace_faithful (G : Type*) [Group G] (T : groupAlgebra G) :
    trace G (star T * T) = 0 ↔ T = 0 := by
…
```
Mentions: OAI.UltrapowerBridge.groupAlgebra, OAI.UltrapowerBridge.trace
theorem OAI.UltrapowerBridge.delta_inner line 185
theorem OAI.UltrapowerBridge.algebra_apply_single line 189
theorem OAI.UltrapowerBridge.adjoint_coefficient line 196
theorem OAI.UltrapowerBridge.trace_mul_formula line 205
theorem OAI.UltrapowerBridge.trace_mul_comm line 217
Source documentation
Cyclicity for all bounded operators in the actual double commutant.
```
theorem trace_mul_comm (S T : groupAlgebra G) : trace G (S * T) = trace G (T * S) := by
…
```
Mentions: OAI.UltrapowerBridge.groupAlgebra, OAI.UltrapowerBridge.trace
theorem OAI.UltrapowerBridge.trace_one line 225
theorem OAI.UltrapowerBridge.trace_add line 229
theorem OAI.UltrapowerBridge.trace_smul line 232
def OAI.UltrapowerBridge.traceLinear line 235
def OAI.UltrapowerBridge.traceNorm line 241
Source documentation
The canonical trace two-norm is the norm of the identity-vector image.
```
def traceNorm (T : groupAlgebra G) : ℝ := ‖(T : Operator G) (delta G)‖
```
Mentions: OAI.UltrapowerBridge.groupAlgebra, OAI.UltrapowerBridge.Operator, OAI.UltrapowerBridge.delta
theorem OAI.UltrapowerBridge.traceNorm_sq line 243
structure OAI.UltrapowerBridge.TracialRepresentation line 256
Source documentation
A concrete finite tracial von Neumann algebra in a faithful vector-trace representation. These are operator-algebra data, without approximation assumptions.
```
structure TracialRepresentation (M : VonNeumannAlgebra H) where
…
```
abbrev OAI.UltrapowerBridge.TracialRepresentation.Algebra line 266
def OAI.UltrapowerBridge.TracialRepresentation.trace line 268
def OAI.UltrapowerBridge.TracialRepresentation.norm₂ line 269
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_one line 271
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_mul_comm line 274
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_star_mul line 277
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_star line 284
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_zero line 295
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_sub line 296
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_add_le line 299
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_smul line 302
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_mul_le line 305
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_mul_le_right line 308
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_le_norm line 313
theorem OAI.UltrapowerBridge.TracialRepresentation.norm_trace_le_norm₂ line 317
theorem OAI.UltrapowerBridge.TracialRepresentation.norm₂_eq_zero_iff line 320
def OAI.UltrapowerBridge.groupTracialRepresentation line 332
Source documentation
The actual group algebra supplies the concrete tracial data; no group approximation, ICC, factor, or countability premise occurs.
```
def groupTracialRepresentation (G : Type*) [Group G] :
    TracialRepresentation (concreteGroupAlgebra G) where
…
```
Mentions: OAI.UltrapowerBridge.TracialRepresentation, OAI.UltrapowerBridge.concreteGroupAlgebra
def OAI.UltrapowerBridge.ultraweakTopology line 345
Source documentation
The actual ultraweak topology, generated by absolutely summable vector functionals. No continuity of a chosen trace is built into this definition.
```
@[instance_reducible] def ultraweakTopology : TopologicalSpace (H →L[ℂ] H) :=
…
```
theorem OAI.UltrapowerBridge.vectorFunctional_ultraweak_continuous line 352
def OAI.UltrapowerBridge.algebraUltraweakTopology line 376
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_normal line 381
Source documentation
Vector traces are normal, expressed as continuity for the actual ultraweak topology.
```
theorem TracialRepresentation.trace_normal {M : VonNeumannAlgebra H}
    (τ : TracialRepresentation M) :
    @Continuous _ _ (algebraUltraweakTopology M) inferInstance τ.trace :=
…
```
Mentions: OAI.UltrapowerBridge.TracialRepresentation, OAI.UltrapowerBridge.algebraUltraweakTopology