MatrixTrace.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.KervaireMatrix.Space line 22
abbrev OAI.KervaireMatrix.Operator line 23
def OAI.KervaireMatrix.right line 26
Source documentation
Diagonal right translations on the finite multiple of the regular Hilbert space.
```
def right (a : A) : Space D A ≃ₗᵢ[ℂ] Space D A :=
…
```
Mentions: OAI.KervaireMatrix.Space
theorem OAI.KervaireMatrix.right_apply line 29
theorem OAI.KervaireMatrix.right_delta line 32
theorem OAI.KervaireMatrix.right_star line 35
def OAI.KervaireMatrix.InCommutant line 42
Source documentation
The finite matrix group von Neumann algebra, before bundling.
```
def InCommutant (T : Operator D A) : Prop := ∀ a : A, Commute T (right (D := D) a : Operator D A)
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.right
theorem OAI.KervaireMatrix.matrix_coefficient line 45
Source documentation
Matrix equivariance with no countability restriction.
```
theorem matrix_coefficient {T : Operator D A} (hT : InCommutant T)
    (i j : D) (x y : A) : T (delta (j,y)) (i,x) = T (delta (j,1)) (i,x*y⁻¹) := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant
theorem OAI.KervaireMatrix.star_coefficient line 53
Source documentation
The reflected matrix coefficient identity for adjoints.
```
theorem star_coefficient {T : Operator D A} (hT : InCommutant T)
    (i j : D) (x : A) :
    star (star T (delta (i,1)) (j,x)) = T (delta (j,1)) (i,x⁻¹) := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant
def OAI.KervaireMatrix.trace line 67
theorem OAI.KervaireMatrix.trace_apply line 71
theorem OAI.KervaireMatrix.trace_eq_coefficient line 74
theorem OAI.KervaireMatrix.trace_one line 77
theorem OAI.KervaireMatrix.summable_product_coefficients line 83
Source documentation
All double series below are absolutely summable, even for an uncountable group.
```
theorem summable_product_coefficients {S T : Operator D A} (hS : InCommutant S) (i : D) :
    Summable (fun p : D × A => S (delta (p.1,1)) (i,p.2⁻¹) * T (delta (i,1)) p) := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant
theorem OAI.KervaireMatrix.trace_mul_eq_sum_tsum line 93
Source documentation
Trace multiplication expressed by regular matrix coefficients.
```
theorem trace_mul_eq_sum_tsum {S T : Operator D A} (hS : InCommutant S) :
    trace (S*T) = ∑ i : D, ∑ j : D, ∑' x : A,
      S (delta (j,1)) (i,x⁻¹) * T (delta (i,1)) (j,x) := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant, OAI.KervaireMatrix.trace
theorem OAI.KervaireMatrix.trace_mul_comm line 112
Source documentation
Full cyclicity of the finite matrix regular trace.
```
theorem trace_mul_comm {S T : Operator D A} (hS : InCommutant S) (hT : InCommutant T) :
    trace (S*T) = trace (T*S) := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant, OAI.KervaireMatrix.trace
theorem OAI.KervaireMatrix.eq_zero_of_frame line 134
Source documentation
The complete finite frame is separating for the right regular commutant.
```
theorem eq_zero_of_frame {T : Operator D A} (hT : InCommutant T)
    (h : ∀ i : D, T (delta (i,1)) = 0) : T = 0 := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant
theorem OAI.KervaireMatrix.re_trace_star_mul_self line 152
Source documentation
The real trace of a positive square is the sum of squared column norms.
```
theorem re_trace_star_mul_self (T : Operator D A) :
    (trace (star T*T)).re = ∑ i : D, ‖T (delta (i,1))‖^2 := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.trace
theorem OAI.KervaireMatrix.re_trace_star_mul_self_eq_zero_iff line 163
Source documentation
Faithfulness of the real matrix trace, in positive-square form.
```
theorem re_trace_star_mul_self_eq_zero_iff {T : Operator D A} (hT : InCommutant T) :
    (trace (star T*T)).re = 0 ↔ T = 0 := by
…
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant, OAI.KervaireMatrix.trace
theorem OAI.KervaireMatrix.InCommutant.sqrt line 181
Source documentation
Square roots preserve the matrix commutant.
```
theorem InCommutant.sqrt {T : Operator D A} (hT : InCommutant T) :
    InCommutant (CFC.sqrt T) := fun a => (hT a).cfcₙ_nnreal NNReal.sqrt
```
Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant
theorem OAI.KervaireMatrix.re_trace_eq_zero_iff_of_nonneg line 184
def OAI.KervaireMatrix.algebra line 204
Source documentation
The closed algebra M_D(M_A) represented on the arbitrary-group Hilbert space.
```
def algebra : StarSubalgebra ℂ (Operator D A) :=
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.mem_algebra line 207
theorem OAI.KervaireMatrix.trace_eq_vectorSum line 220
Source documentation
The vector family agrees exactly with the unnormalized matrix trace.
```
theorem trace_eq_vectorSum : (trace : Operator D A →L[ℂ] ℂ) =
    vectorSum (fun i : D => (delta (i,(1 : A)))) := rfl
```
Mentions: OAI.KervaireMatrix.trace, OAI.KervaireMatrix.Operator
instance OAI.KervaireMatrix.(instance at line 224) line 224
Source documentation
The regular Hilbert space is nonzero whenever the finite index set is inhabited.
```
instance [Nonempty D] : Nontrivial (Space D A) := by
…
```
Mentions: OAI.KervaireMatrix.Space
def OAI.KervaireMatrix.phase line 232
theorem OAI.KervaireMatrix.phase_mul_le line 236
Source documentation
Subadditivity for the full arbitrary-group matrix algebra, with no approximation hypothesis.
```
theorem phase_mul_le [Nonempty D] (U V : algebra (D := D) (A := A))
…
```
Mentions: OAI.KervaireMatrix.algebra

theorem OAI.KervaireMatrix.phase_nonneg line 253

Source documentation

Phase is nonnegative.

theorem phase_nonneg (U : Operator D A) (hU : U ∈ unitary (Operator D A)) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireMatrix.Operator

theorem OAI.KervaireMatrix.phase_one line 264
Source documentation
The scalar identity has zero phase, including the precise cut convention.
```
theorem phase_one [Nonempty D] : phase (1 : Operator D A) = 0 := by
…
```
Mentions: OAI.KervaireMatrix.phase, OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.phase_eq_zero_iff line 275
Source documentation
Vanishing of the phase detects the identity in the faithful regular algebra.
```
theorem phase_eq_zero_iff [Nonempty D] (U : algebra (D := D) (A := A))
…
```
Mentions: OAI.KervaireMatrix.algebra
theorem OAI.KervaireMatrix.InCommutant.mul line 303
theorem OAI.KervaireMatrix.InCommutant.pow line 307
theorem OAI.KervaireMatrix.InCommutant.star line 311
theorem OAI.KervaireMatrix.conjugate_pow line 317
Source documentation
Telescope powers without a finite-dimensional restriction on the Hilbert space.
```
theorem conjugate_pow (U Q : Operator D A) (hQ : Q ∈ unitary (Operator D A)) (n : ℕ) :
    (Q*U*star Q)^n = Q*U^n*star Q := by
…
```
Mentions: OAI.KervaireMatrix.Operator

theorem OAI.KervaireMatrix.phase_conjugate line 328

Source documentation

Conjugation invariance of the exact phase in the arbitrary-group regular algebra.

theorem phase_conjugate (U Q : Operator D A)
    (hU : U ∈ unitary (Operator D A)) (hQ : Q ∈ unitary (Operator D A))
    (hUc : InCommutant U) (hQc : InCommutant Q) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireMatrix.Operator, OAI.KervaireMatrix.InCommutant

theorem OAI.KervaireMatrix.phase_grid line 343
Source documentation
Matrix trace of the root-grid phase identity, retaining the unnormalized dimension.
```
theorem phase_grid (U : Operator D A) (hU : U ∈ unitary (Operator D A))
    (d : ℕ) (hd : 0 < d) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireMatrix.Operator