OAI/RepresentationTheory/RowColumn/Postselection.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RowColumn.MatrixState.indexInclusion line 13

   Source documentation

   Rectangular coordinate inclusion for an actual injective index map.

   def indexInclusion (e : J ↪ I) : Matrix I J ℂ := fun i j => if i=e j then 1 else 0
   …

2. lemma OAI.RowColumn.MatrixState.indexInclusion_star_mul line 16
3. def OAI.RowColumn.MatrixState.extendMatrix line 27
4. lemma OAI.RowColumn.MatrixState.indexInclusion_mul line 30
5. lemma OAI.RowColumn.MatrixState.extendMatrix_apply line 35
6. lemma OAI.RowColumn.MatrixState.extendMatrix_eq_zero_left line 42
7. lemma OAI.RowColumn.MatrixState.extendMatrix_eq_zero_right line 48
8. lemma OAI.RowColumn.MatrixState.extendMatrix_positive line 54
9. lemma OAI.RowColumn.MatrixState.extendMatrix_trace line 57
10. def OAI.RowColumn.MatrixState.blockMask line 62
11. def OAI.RowColumn.MatrixState.pinchMatrix line 63
12. lemma OAI.RowColumn.MatrixState.blockMask_hermitian line 66
13. lemma OAI.RowColumn.MatrixState.pinchMatrix_apply line 71
14. lemma OAI.RowColumn.MatrixState.pinchMatrix_positive line 83
15. lemma OAI.RowColumn.MatrixState.pinchMatrix_trace line 92
16. lemma OAI.RowColumn.MatrixState.pinchMatrix_support line 96
17. lemma OAI.RowColumn.MatrixState.quadratic_eq_energy line 111
18. lemma OAI.RowColumn.MatrixState.posSemidef_of_quadratic line 124
19. lemma OAI.RowColumn.MatrixState.quadratic_smul line 135
20. lemma OAI.RowColumn.MatrixState.quadratic_sub line 142
21. lemma OAI.RowColumn.MatrixState.quadratic_sum line 147
22. lemma OAI.RowColumn.MatrixState.le_of_quadratic_le line 153
23. lemma OAI.RowColumn.MatrixState.quadratic_pinch line 158
24. def OAI.RowColumn.Signed.intertwinerMatrix line 183

    Source documentation

    Matrix in the actual orthonormal word basis, with no change of representation.

    def intertwinerMatrix (line : S → L)
        (T : Representation.IntertwiningMap (lineRepresentation (odd := odd) (k := k) line)
    …

    Mentions: OAI.RowColumn.Signed.lineRepresentation

25. lemma OAI.RowColumn.Signed.intertwinerMatrix_apply line 190
26. lemma OAI.RowColumn.Signed.intertwinerMatrix_positive line 199
27. lemma OAI.RowColumn.Signed.parityPattern_eq_iff line 209
28. lemma OAI.RowColumn.Signed.pinch_intertwiner_invariant line 214
29. lemma OAI.RowColumn.Signed.intertwiner_le_pinch line 235
30. lemma OAI.RowColumn.MatrixState.extendMatrix_equiv line 273
31. lemma OAI.RowColumn.MatrixState.submatrix_mono line 291
32. def OAI.RowColumn.Signed.wordInclusion line 303
33. def OAI.RowColumn.Signed.extendedPinch line 305
34. lemma OAI.RowColumn.Signed.extendedPinch_positive line 311
35. lemma OAI.RowColumn.Signed.extendedPinch_trace line 318
36. lemma OAI.RowColumn.Signed.extendedPinch_invariant line 325
37. lemma OAI.RowColumn.Signed.extendedPinch_support line 339
38. theorem OAI.RowColumn.Signed.signed_line_postselection line 355

    Source documentation

    Finite positive even product-state majorant of the true signed line commutant. Both parity bandwidth and the local-state normalization are retained.

    theorem signed_line_postselection (line : S → L) (a₀ : S → C × C)
        (hn : 0 < Fintype.card S)
        (T : Representation.IntertwiningMap (lineRepresentation (odd := odd) (k := k) line)
    …

    Mentions: OAI.RowColumn.Signed.lineRepresentation