OAI/Analysis/CharacterCriterion/FactorIndependence.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.GenericRW.FactorIndependence.IsFactor line 15
  2. abbrev OAI.KirchbergRordam.GenericRW.FactorIndependence.SumHilbert line 18
  3. def OAI.KirchbergRordam.GenericRW.FactorIndependence.diagonal line 20
  4. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.diagonal_apply line 25
  5. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.star_diagonal line 28
  6. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.projection_commutes line 39
  7. def OAI.KirchbergRordam.GenericRW.FactorIndependence.injection line 54
  8. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.injection_apply line 59
  9. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.sum_injection line 64
  10. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.diagonal_injection line 70
  11. def OAI.KirchbergRordam.GenericRW.FactorIndependence.entry line 75
  12. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.entry_apply line 79
  13. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.entry_commutes line 83
  14. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.apply_eq_sum_entries line 90
  15. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.invariant_closure line 97
  16. def OAI.KirchbergRordam.GenericRW.FactorIndependence.column line 101
  17. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.column_apply line 105
  18. def OAI.KirchbergRordam.GenericRW.FactorIndependence.columnSpace line 107
  19. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.columnSpace_closed line 113
  20. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.generator_mem line 118
  21. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.column_mem line 124
  22. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.invariant_span_closure line 130
  23. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.commutant_invariant line 140
  24. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.algebra_invariant line 150
  25. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.columnSpace_eq_top line 166
  26. def OAI.KirchbergRordam.GenericRW.FactorIndependence.row line 210
  27. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.row_apply line 214
  28. lemma OAI.KirchbergRordam.GenericRW.FactorIndependence.row_injection line 218
  29. theorem OAI.KirchbergRordam.GenericRW.FactorIndependence.relation_coefficients_zero line 224
  30. def OAI.KirchbergRordam.GenericRW.GroupedFactors.commutantOf line 258
  31. def OAI.KirchbergRordam.GenericRW.GroupedFactors.bicommutant line 267
  32. lemma OAI.KirchbergRordam.GenericRW.GroupedFactors.mem_commutantOf_iff line 270
  33. lemma OAI.KirchbergRordam.GenericRW.GroupedFactors.subset_bicommutant line 277
  34. lemma OAI.KirchbergRordam.GenericRW.GroupedFactors.closures_commute line 284
  35. theorem OAI.KirchbergRordam.GenericRW.GroupedFactors.isFactor_of_total line 295
  36. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.commute_of_legs line 316
  37. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.left_factor line 339
  38. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.right_factor line 350
  39. def OAI.KirchbergRordam.GenericRW.MaxTensor.leg line 369
  40. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.leg_zero line 373
  41. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.leg_succ_zero line 374
  42. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.leg_succ_succ line 375
  43. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.commute_legs line 378
  44. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.commute_of_power_legs line 395
  45. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.power_leg_factor line 410
  46. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.power_leg_factors_commute line 435
  47. lemma OAI.KirchbergRordam.GenericRW.ProductIndependence.selfAdjoint_complex_independent line 453
  48. lemma OAI.KirchbergRordam.GenericRW.ProductIndependence.pair_independent line 475
  49. theorem OAI.KirchbergRordam.GenericRW.ProductIndependence.many_independent line 498
  50. def OAI.KirchbergRordam.GenericRW.RealProduct.multiply line 534
  51. lemma OAI.KirchbergRordam.GenericRW.RealProduct.multiply_tprod line 537
  52. lemma OAI.KirchbergRordam.GenericRW.RealProduct.multiply_injective line 544
  53. lemma OAI.KirchbergRordam.GenericRW.RealProduct.selfAdjoint_product line 562
  54. lemma OAI.KirchbergRordam.GenericRW.RealProduct.multiply_selfAdjoint line 580