Model.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.GroupRingDeterminant.Hilbert line 11
Source documentation
The Hilbert space l²(G)^n, with the product coordinates flattened.
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:11 (same declaration text).
```
abbrev Hilbert (G : Type) (n : ℕ) := lp (fun _ : Fin n × G => ℂ) 2
```
def OAI.GroupRingDeterminant.identityVector line 14
Source documentation
The identity vector in component i.
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:14 (same declaration text).
```
def identityVector {G : Type} [Group G] {n : ℕ} (i : Fin n) : Hilbert G n :=
…
```
Mentions: OAI.GroupRingDeterminant.Hilbert
def OAI.GroupRingDeterminant.groupTrace line 20
Source documentation
The unnormalized matrix trace, linear in its operator argument.
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:20 (same declaration text).
```
def groupTrace {G : Type} [Group G] {n : ℕ}
    (T : Hilbert G n →L[ℂ] Hilbert G n) : ℂ :=
…
```
Mentions: OAI.GroupRingDeterminant.Hilbert
def OAI.GroupRingDeterminant.fkDet line 26
Source documentation
The invertible-case Fuglede--Kadison determinant. It is used below only for invertible regular operators.
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:26 (same declaration text).
```
def fkDet {G : Type} [Group G] {n : ℕ}
    (T : Hilbert G n →L[ℂ] Hilbert G n) : ℝ :=
…
```
Mentions: OAI.GroupRingDeterminant.Hilbert
def OAI.GroupRingDeterminant.IsRegularOperator line 31
Source documentation
Exact coordinate specification of the bounded left-regular operator of A.
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:31 (same declaration text).
```
def IsRegularOperator {G : Type} [Group G] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) (MonoidAlgebra ℤ G))
    (T : Hilbert G n →L[ℂ] Hilbert G n) : Prop :=
…
```
Mentions: OAI.GroupRingDeterminant.Hilbert
def OAI.GroupRingDeterminant.rationalMatrix line 39
Source documentation
Coefficientwise extension from the integral to the rational group ring.
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:39 (same declaration text).
```
def rationalMatrix {G : Type} [Group G] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) (MonoidAlgebra ℤ G)) :
    Matrix (Fin n) (Fin n) (MonoidAlgebra ℚ G) :=
…
```
def OAI.GroupRingDeterminant.MainStatement line 45
Source documentation
An integral group-ring matrix with rational and bounded inverses and determinant in (0, 1).
Also declared: ComparatorChallenges/GroupRingDeterminant.lean:45 (same declaration text).
```
def MainStatement : Prop :=
…
```