OAI/Analysis/CharacterCriterion/FieldCalculus.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.GenericRW.M2 line 28
  2. abbrev OAI.KirchbergRordam.GenericRW.M3 line 29
  3. abbrev OAI.KirchbergRordam.GenericRW.M6 line 30
  4. def OAI.KirchbergRordam.GenericRW.leftMatrixAlgebra line 33
  5. def OAI.KirchbergRordam.GenericRW.rightMatrixAlgebra line 50
  6. def OAI.KirchbergRordam.GenericRW.leftMatrix line 67
  7. def OAI.KirchbergRordam.GenericRW.rightMatrix line 72
  8. def OAI.KirchbergRordam.GenericRW.matrixEval line 77
  9. def OAI.KirchbergRordam.GenericRW.dimensionDropSubalgebra line 87
  10. instance OAI.KirchbergRordam.GenericRW.(instance at line 90) line 90
  11. instance OAI.KirchbergRordam.GenericRW.dimensionDropClosed line 93
  12. abbrev OAI.KirchbergRordam.GenericRW.DimensionDrop23 line 103
  13. instance OAI.KirchbergRordam.GenericRW.dropSubringClass line 105
  14. instance OAI.KirchbergRordam.GenericRW.(instance at line 109) line 109
  15. example OAI.KirchbergRordam.GenericRW.(example at line 111) line 111
  16. def OAI.KirchbergRordam.GenericRW.dropCoordinate line 114
  17. def OAI.KirchbergRordam.GenericRW.leftCone line 124
  18. def OAI.KirchbergRordam.GenericRW.rightCone line 136
  19. def OAI.KirchbergRordam.GenericRW.matrixUnit line 148
  20. theorem OAI.KirchbergRordam.GenericRW.drop_ext line 152
  21. theorem OAI.KirchbergRordam.GenericRW.matrixUnit_mul line 159
  22. theorem OAI.KirchbergRordam.GenericRW.matrixUnit_mul_self line 168
  23. theorem OAI.KirchbergRordam.GenericRW.leftCone_mul_self line 175
  24. theorem OAI.KirchbergRordam.GenericRW.rightCone_mul_self line 183
  25. structure OAI.KirchbergRordam.GenericRW.FieldCalculus.Data line 200
  26. abbrev OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.Domain line 213
  27. def OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.aux line 215
  28. def OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.coeff line 220
  29. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.coeff_mul line 222
  30. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.norm_coeff_le line 227
  31. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.multiplier_star line 233
  32. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.multiplier_product line 252
  33. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.star_coeff line 271
  34. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.product_coeff line 278
  35. def OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.scalarMul line 296
  36. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.scalar_coeff line 302
  37. abbrev OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.Matrices line 313
  38. def OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.matrices line 315
  39. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.matrices_single line 321
  40. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.matrices_product line 337
  41. lemma OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.matrices_star line 353
  42. def OAI.KirchbergRordam.GenericRW.FieldCalculus.Data.hom line 358
  43. structure OAI.KirchbergRordam.GenericRW.OrderZero.Pair line 374
  44. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_h line 385
  45. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_commute_right_h line 401
  46. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.right_commute_left_h line 419
  47. abbrev OAI.KirchbergRordam.GenericRW.OrderZero.Pair.eval line 423
  48. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.commute_eval line 425
  49. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weight line 430
  50. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.selfAdjoint_weight line 434
  51. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.eval_weight line 450
  52. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.norm_product line 453
  53. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.field line 469
  54. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_x_field line 500
  55. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.right_x_field line 507
  56. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_x_coeff line 519
  57. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.right_x_coeff line 534