OAI/Analysis/CharacterCriterion/WeightedUnits.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.total_mul_v line 31
2. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.defect_mul_v line 39
3. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.commute_defect line 42
4. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.defect_nonneg line 46
5. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.defect_selfAdjoint line 48
6. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.polarVectors line 52
7. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.column_inner line 56
8. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.polarVectors_inner line 68
9. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.polarVectors_annihilate line 89
10. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.units_polarVectors line 96
11. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.defectCopies line 108
12. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.defectCopies_orthogonal line 111
13. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.defectCopies_commute line 116
14. abbrev OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.lambda line 130
15. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwK line 133
16. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwH line 135
17. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwQ line 136
18. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwQ_star line 138
19. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwQ_sq line 141
20. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwK_star_mul line 145
21. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwK_mul_star line 152
22. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwH_norm line 160
23. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwAlpha line 165
24. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwAlpha_total line 170
25. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rescale line 182
26. def OAI.KirchbergRordam.GenericRW.ConeModel.scalarRemainder line 210
27. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.lambda_remainder line 220
28. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.scalar_mul_left line 228
29. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.scalar_mul_copies line 237
30. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.copies_mul_scalar line 244
31. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwH_val line 259
32. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwH_selfAdjoint line 261
33. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL line 266
34. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL_eq line 268
35. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL_nonneg line 273
36. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL_norm line 277
37. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL_commute line 281
38. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL_commute_scalar line 286
39. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwR line 296
40. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwR_selfAdjoint line 298
41. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwR_commute line 304
42. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwR_total line 307
43. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwBeta line 326
44. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rw_complementary line 330
45. def OAI.KirchbergRordam.GenericRW.ConeModel.defectMul line 337
46. def OAI.KirchbergRordam.GenericRW.FlipPath.weightedC line 347
47. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedC_val line 349
48. lemma OAI.KirchbergRordam.GenericRW.FlipPath.conePath_top line 353
49. def OAI.KirchbergRordam.GenericRW.FlipPath.e line 361
50. lemma OAI.KirchbergRordam.GenericRW.FlipPath.e_star line 363
51. lemma OAI.KirchbergRordam.GenericRW.FlipPath.e_mul line 367
52. lemma OAI.KirchbergRordam.GenericRW.FlipPath.scalar_weight line 373
53. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedC_apply line 378
54. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedC_residual_apply line 383
55. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedC_flip_pointwise line 390
56. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedC_flip line 413
57. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwLeft line 440
58. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwLeft_sub line 445
59. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwLeft_mul line 451
60. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rw_spoke line 457
61. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwLeft_scalar line 469
62. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwLeft_units line 473
63. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwL_mul_left line 478
64. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwBeta_mul_spoke line 499
65. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwLeft_mul_beta line 513
66. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rw_commute_spoke line 547