OAI/Analysis/CharacterCriterion/OrderZero.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits line 29
  2. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.commute_h line 43
  3. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.column_sum line 59
  4. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.norm_mul_le line 73
  5. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.linear line 91
  6. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.linear_single line 98
  7. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.linear_one line 113
  8. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.linear_star line 127
  9. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.linear_mul line 141
  10. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copy_norm line 171
  11. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.copy line 182
  12. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copy_embed line 185
  13. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.continuous_copy line 189
  14. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copy_orthogonal line 193
  15. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.copies line 205
  16. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.continuous_copies line 221
  17. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copies_orthogonal line 224
  18. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copies_commute line 241
  19. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.leftLinear line 274
  20. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.left_cross_inner line 284
  21. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross line 304
  22. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.continuous_cross line 308
  23. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_embed line 311
  24. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_zero line 320
  25. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_add line 324
  26. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_smul line 336
  27. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.crossLinear line 347
  28. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_star line 352
  29. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_inner line 362
  30. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.cross_diagonal line 374
  31. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.left_mul line 377
  32. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.corner_mul_left line 390
  33. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.transport_right line 406
  34. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.left_mul_of_eq line 422
  35. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copy_mul_left line 437
  36. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.copies_mul_left line 456
  37. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.units_mul_left line 464
  38. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.left_mul_copies line 476
  39. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.frame line 501
  40. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.frame_inner line 505
  41. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.frame_total line 513
  42. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.frame_total_diagonal line 532
  43. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.corner_mul_frame line 545
  44. def OAI.KirchbergRordam.GenericRW.OrderZero.gram line 559
  45. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.toWeightedMatrix line 581
  46. abbrev OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.coneHom line 592
  47. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.coneHom_corner line 594
  48. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.frame_inner_diagonal line 612
  49. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.triple line 617
  50. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.triple_last line 619
  51. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.triple_castSucc line 620
  52. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.triple_relations line 623
  53. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.triple_total line 634
  54. lemma OAI.KirchbergRordam.GenericRW.HereditaryTransport.triple_norm line 643
  55. def OAI.KirchbergRordam.GenericRW.HereditaryTransport.tripleUnits line 658