MatrixShifts.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireMatrix.coordinateProjection line 25
Source documentation
Projection to a scalar coordinate, on the actual product-index regular Hilbert space.
```
def coordinateProjection (i : D) : Operator D A := by
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.coordinateProjection_apply line 43
def OAI.KervaireMatrix.matrixUnit line 49
Source documentation
The scalar matrix unit, continuously acting on all (possibly uncountable) group coordinates.
```
def matrixUnit (i j : D) : Operator D A := by
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.matrixUnit_apply line 54
theorem OAI.KervaireMatrix.ext_delta line 66
Source documentation
Equality of operators on the standard orthonormal basis.
```
theorem ext_delta {T U : Operator D A}
    (h : ∀ p : D × A, T (delta p) = U (delta p)) : T = U := by
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.star_eq_of_coefficients line 80
Source documentation
Matrix coefficients suffice to establish an adjoint identity.
```
theorem star_eq_of_coefficients {T U : Operator D A}
    (h : ∀ p q : D × A, star (T (delta p) q) = U (delta q) p) : star T = U := by
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.matrixUnit_star line 93
def OAI.KervaireMatrix.scalarTensor line 108
Source documentation
Scalar matrices embedded without any finite/countable assumption on the group.
```
def scalarTensor (M : Matrix D D ℂ) : Operator D A :=
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.scalarTensor_apply line 111
theorem OAI.KervaireMatrix.scalarTensor_one line 118
theorem OAI.KervaireMatrix.scalarTensor_mul line 123
theorem OAI.KervaireMatrix.scalarTensor_star line 135
theorem OAI.KervaireMatrix.scalarTensor_mem_commutant line 148
Source documentation
Scalar matrices lie in exactly the commutant required by the phase theorem.
```
theorem scalarTensor_mem_commutant (M : Matrix D D ℂ) :
    InCommutant (scalarTensor (A := A) M) := by
…
```
Mentions: OAI.KervaireMatrix.InCommutant, OAI.KervaireMatrix.scalarTensor
theorem OAI.KervaireMatrix.trace_scalarTensor line 156
Source documentation
The scalar trace on tensoring with the regular identity is unnormalized matrix trace.
```
@[simp] theorem trace_scalarTensor (M : Matrix D D ℂ) :
    trace (scalarTensor (A := A) M) = Matrix.trace M := by
…
```
Mentions: OAI.KervaireMatrix.trace, OAI.KervaireMatrix.scalarTensor
theorem OAI.KervaireMatrix.scalarTensor_mem_unitary line 164
Source documentation
Unitary scalar matrices remain unitary in the full regular operator algebra.
```
theorem scalarTensor_mem_unitary {M : Matrix D D ℂ} (hM : M ∈ Matrix.unitaryGroup D ℂ) :
    scalarTensor (A := A) M ∈ unitary (Operator D A) := by
…
```
Mentions: OAI.KervaireMatrix.scalarTensor, OAI.KervaireMatrix.Operator
def OAI.KervaireMatrix.labelledPermutation line 179
Source documentation
The coordinate permutation underlying a group-labelled shift. Labels act on the left so that the operator commutes with every right translation.
```
def labelledPermutation (σ : Equiv.Perm D) (a : D → A) : Equiv.Perm (D × A) where
…
```
def OAI.KervaireMatrix.labelledShift line 186
Source documentation
A corner-labelled permutation on the actual arbitrary-group Hilbert space.
```
def labelledShift (σ : Equiv.Perm D) (a : D → A) : Operator D A :=
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.labelledShift_apply line 189
theorem OAI.KervaireMatrix.labelledShift_delta line 193
theorem OAI.KervaireMatrix.labelledShift_unitary line 198
Source documentation
This representation is unitary without dimensional or cardinality assumptions.
```
theorem labelledShift_unitary (σ : Equiv.Perm D) (a : D → A) :
    labelledShift σ a ∈ unitary (Operator D A) := by
…
```
Mentions: OAI.KervaireMatrix.labelledShift, OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.labelledShift_mem_commutant line 208
Source documentation
The commutant contains every group-labelled shift.
```
theorem labelledShift_mem_commutant (σ : Equiv.Perm D) (a : D → A) :
    InCommutant (labelledShift σ a) := by
…
```
Mentions: OAI.KervaireMatrix.InCommutant, OAI.KervaireMatrix.labelledShift
theorem OAI.KervaireMatrix.labelledShift_one line 215
theorem OAI.KervaireMatrix.labelledShift_mul line 220
def OAI.KervaireMatrix.scalarDiagonal line 230
Source documentation
A scalar diagonal on the finite coordinate set.
```
def scalarDiagonal (u : D → ℂ) : Operator D A :=
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.scalarDiagonal_apply line 234
theorem OAI.KervaireMatrix.scalarDiagonal_delta line 240
theorem OAI.KervaireMatrix.scalarDiagonal_one line 250
theorem OAI.KervaireMatrix.scalarDiagonal_mul line 255
theorem OAI.KervaireMatrix.scalarDiagonal_star line 261
theorem OAI.KervaireMatrix.scalarDiagonal_unitary line 272
def OAI.KervaireMatrix.weightedShift line 282
Source documentation
This includes both shifts: S has coefficient labels, while Theta has only scalar phase labels.
```
def weightedShift (σ : Equiv.Perm D) (u : D → ℂ) (a : D → A) : Operator D A :=
…
```
Mentions: OAI.KervaireMatrix.Operator
theorem OAI.KervaireMatrix.weightedShift_apply line 285
theorem OAI.KervaireMatrix.weightedShift_delta line 291
theorem OAI.KervaireMatrix.weightedShift_unitary line 296
theorem OAI.KervaireMatrix.weightedShift_mem_commutant line 300

theorem OAI.KervaireMatrix.weightedShift_mul line 307

Source documentation

Multiplication proves the exact order of coefficient inverses on every boundary step.

theorem weightedShift_mul (σ τ : Equiv.Perm D) (u v : D → ℂ) (a b : D → A) :
    weightedShift σ u a * weightedShift τ v b =
      weightedShift (σ*τ) (fun d => u (τ d)*v d) (fun d => a (τ d)*b d) := by
…

Mentions: OAI.KervaireMatrix.weightedShift

theorem OAI.KervaireSpectral.scalarRotation_nat line 316
theorem OAI.KervaireSpectral.scalarRotation_grid_pow line 322