Commutator.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Entry bounds for a tridiagonal grading commutator

All norms here are norms of individual complex entries. No default norm on a matrix is used. A complete orthogonal family defines a phase unitary with eigenvalues I^k. For a tridiagonal operator the commutator is the difference of two unitary conjugates divided by 2 I.

def OAI.LeanBlast.GotsmanLinial.spectralMultiplier line 27
Source documentation
A complex spectral multiplier for a finite family of projections.
```
def spectralMultiplier (P : κ → Matrix ι ι ℂ) (a : κ → ℂ) : Matrix ι ι ℂ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.spectralMultiplier_mul_projection line 34
theorem OAI.LeanBlast.GotsmanLinial.projection_mul_spectralMultiplier line 39
theorem OAI.LeanBlast.GotsmanLinial.spectralMultiplier_mul line 44
theorem OAI.LeanBlast.GotsmanLinial.star_spectralMultiplier line 53
theorem OAI.LeanBlast.GotsmanLinial.spectralMultiplier_unitary line 57
theorem OAI.LeanBlast.GotsmanLinial.spectralMultiplier_sandwich_block line 65
theorem OAI.LeanBlast.GotsmanLinial.spectralMultiplier_commutator_block line 77
theorem OAI.LeanBlast.GotsmanLinial.spectral_blocks_reconstruct line 94
theorem OAI.LeanBlast.GotsmanLinial.spectral_blocks_ext line 99
theorem OAI.LeanBlast.GotsmanLinial.I_pow_mul_star line 106
theorem OAI.LeanBlast.GotsmanLinial.phase_coeff_adjacent line 110

theorem OAI.LeanBlast.GotsmanLinial.entry_norm_le_one_of_two_unitaries line 136

Source documentation

The difference of two unitary matrices, divided by 2 I, has entries of modulus at most one.

theorem entry_norm_le_one_of_two_unitaries
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (C U V : Matrix ι ι ℂ)
    (hU : U ∈ Matrix.unitaryGroup ι ℂ) (hV : V ∈ Matrix.unitaryGroup ι ℂ)
    (h : (2 * Complex.I) • C = U - V) (x y : ι) : ‖C x y‖ ≤ 1 := by
…

def OAI.LeanBlast.GotsmanLinial.gradingPhase line 157
Source documentation
The spectral phase I^k of the degree grading.
```
def gradingPhase (P : Fin (n + 1) → Matrix ι ι ℂ) : Matrix ι ι ℂ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.gradingPhase_unitary line 160
def OAI.LeanBlast.GotsmanLinial.BlockTridiagonal line 166
Source documentation
Tridiagonality means that blocks at grading distance greater than one vanish.
```
def BlockTridiagonal (P : Fin (n + 1) → Matrix ι ι ℂ) (Z : Matrix ι ι ℂ) : Prop :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.grading_commutator_phase_identity line 171
Source documentation
Two opposite phase conjugations differ by 2 I times the grading commutator.
```
theorem grading_commutator_phase_identity (hP : OrthogonalProjectionFamily P)
    (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) :
    (2 * Complex.I) • (degreeGrading P * Z - Z * degreeGrading P) =
      gradingPhase P * Z * star (gradingPhase P) -
        star (gradingPhase P) * Z * gradingPhase P := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.BlockTridiagonal, OAI.LeanBlast.GotsmanLinial.degreeGrading, OAI.LeanBlast.GotsmanLinial.gradingPhase
theorem OAI.LeanBlast.GotsmanLinial.norm_degreeGrading_commutator_entry_le_one line 192
Source documentation
Every entry of the tridiagonal degree commutator has modulus at most one.
```
theorem norm_degreeGrading_commutator_entry_le_one
    (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ)
    (htri : BlockTridiagonal P Z) (hZ : Z ∈ Matrix.unitaryGroup ι ℂ)
    (x y : ι) : ‖(degreeGrading P * Z - Z * degreeGrading P) x y‖ ≤ 1 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.BlockTridiagonal, OAI.LeanBlast.GotsmanLinial.degreeGrading
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_degreeGrading_commutator_le line 207
Source documentation
The Hilbert--Schmidt commutator bound is a consequence of block Parseval and the fact that each nonzero block has grading distance at most one.
```
theorem hsNormSq_degreeGrading_commutator_le
    (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ)
    (htri : BlockTridiagonal P Z) :
    hsNormSq (degreeGrading P * Z - Z * degreeGrading P) ≤ hsNormSq Z := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.BlockTridiagonal, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.degreeGrading
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_degreeGrading_commutator_le_card line 227
theorem OAI.LeanBlast.GotsmanLinial.centeredGrading_commutator_eq line 236
Source documentation
Centering the grading does not change its commutator.
```
theorem centeredGrading_commutator_eq (hP : OrthogonalProjectionFamily P)
    (Z : Matrix ι ι ℂ) :
    centeredGrading P * Z - Z * centeredGrading P =
      degreeGrading P * Z - Z * degreeGrading P := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.centeredGrading, OAI.LeanBlast.GotsmanLinial.degreeGrading
theorem OAI.LeanBlast.GotsmanLinial.norm_centeredGrading_commutator_entry_le_one line 244
theorem OAI.LeanBlast.GotsmanLinial.sq_norm_centeredGrading_commutator_entry_le_one line 251
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_centeredGrading_commutator_le_card line 258