CoordinateMultipliers.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Actual diagonal sign and coordinate operators on the cube

The matrices here act on the cube with its counting inner product. Their continuous linear maps act on EuclideanSpace, so all operator-norm statements refer to the intended Euclidean norm. The Hilbert--Schmidt statements use the explicit squared-entry sum hsNormSq.

def OAI.LeanBlast.GotsmanLinial.signMatrix line 26
Source documentation
Multiplication by a real function on the cube, represented in the point-mass basis.
```
def signMatrix (h : Cube n → ℝ) : Matrix (Cube n) (Cube n) ℂ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix line 30
Source documentation
The actual cube coordinate-sign matrix Z_i.
```
def coordinateSignMatrix (i : Fin n) : Matrix (Cube n) (Cube n) ℂ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_apply line 33
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_apply_self line 37
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_apply line 40
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_conjTranspose line 44
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_star line 48
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_isHermitian line 52
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_mul_self line 56
Source documentation
A sign-valued real diagonal is an involution.
```
theorem signMatrix_mul_self (h : Cube n → ℝ)
    (hh : ∀ x, h x = 1 ∨ h x = -1) : signMatrix h * signMatrix h = 1 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.signMatrix
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_conjTranspose_mul line 65
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_mul_conjTranspose line 70
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_unitary line 75
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_commute_diagonal line 82
Source documentation
A real sign diagonal commutes with every complex diagonal weight.
```
theorem signMatrix_commute_diagonal (h : Cube n → ℝ) (d : Cube n → ℂ) :
    Commute (signMatrix h) (Matrix.diagonal d) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.signMatrix
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_mul_diagonal_comm line 90
theorem OAI.LeanBlast.GotsmanLinial.signMatrix_mulVec line 94
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_signMatrix line 98
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_conjTranspose line 103
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_star line 107
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_isHermitian line 111
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_mul_self line 114
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_conjTranspose_mul line 118
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_mul_conjTranspose line 121
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_unitary line 124
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_commute_diagonal line 128
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_mul_diagonal_comm line 132
theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_mulVec line 137
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_coordinateSignMatrix line 141
def OAI.LeanBlast.GotsmanLinial.signMultiplier line 146
Source documentation
The same diagonal action on the counting-inner-product Euclidean space.
```
def signMultiplier (h : Cube n → ℝ) :
    EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.coordinateMultiplier line 151
Source documentation
The actual coordinate multiplier on Euclidean space.
```
def coordinateMultiplier (i : Fin n) :
    EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.toEuclideanCLM_signMatrix line 155
theorem OAI.LeanBlast.GotsmanLinial.toEuclideanCLM_coordinateSignMatrix line 158
theorem OAI.LeanBlast.GotsmanLinial.signMultiplier_apply line 162
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_apply line 168
theorem OAI.LeanBlast.GotsmanLinial.signMultiplier_isSelfAdjoint line 173
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_isSelfAdjoint line 179
theorem OAI.LeanBlast.GotsmanLinial.signMultiplier_mul_self line 182
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_mul_self line 188
theorem OAI.LeanBlast.GotsmanLinial.norm_signMultiplier_apply line 192
theorem OAI.LeanBlast.GotsmanLinial.norm_coordinateMultiplier_apply line 201
theorem OAI.LeanBlast.GotsmanLinial.norm_signMultiplier_le_one line 205
theorem OAI.LeanBlast.GotsmanLinial.norm_coordinateMultiplier_le_one line 211