OAI/Analysis/CharacterCriterion/SquareZeroCone.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KirchbergRordam.GenericRW.Intertwining.algebra line 29
2. instance OAI.KirchbergRordam.GenericRW.Intertwining.closed line 56
3. lemma OAI.KirchbergRordam.GenericRW.Intertwining.cfc line 60
4. lemma OAI.KirchbergRordam.GenericRW.Intertwining.sqrt line 78
5. lemma OAI.KirchbergRordam.GenericRW.Intertwining.mul_sqrt_eq_zero line 85
6. lemma OAI.KirchbergRordam.GenericRW.Intertwining.sqrt_mul_eq_zero line 89
7. structure OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix line 103
8. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.norm_mul_le_of_pair line 113
9. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.commute_h line 138
10. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.column_sum line 144
11. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.norm_mul_le line 148
12. def OAI.KirchbergRordam.GenericRW.IntervalCalculus.coord line 173
13. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.coord_apply line 175
14. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.spectrum_mem_interval line 182
15. def OAI.KirchbergRordam.GenericRW.IntervalCalculus.spectralPoint line 198
16. def OAI.KirchbergRordam.GenericRW.IntervalCalculus.hom line 201
17. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.hom_coord line 205
18. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.norm_hom_le line 215
19. def OAI.KirchbergRordam.GenericRW.IntervalCalculus.coordMul line 223
20. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.coordMul_apply line 229
21. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.coordMul_dense line 235
22. abbrev OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.eval line 284
23. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.commute_eval line 286
24. def OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coeffAux line 290
25. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coeffAux_bound line 295
26. def OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coeff line 304
27. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coeff_coordMul line 307
28. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.norm_coeff_le line 312
29. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coordMul_star line 317
30. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coordMul_mul line 324
31. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.star_coeff line 332
32. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.mul_coeff line 339
33. abbrev OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.ConeMatrix line 366
34. def OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs line 368
35. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs_add line 370
36. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs_smul line 374
37. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs_single line 378
38. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs_zero line 382
39. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs_mul line 384
40. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixCoeffs_star line 401
41. def OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.matrixHom line 406