OAI/Analysis/CharacterCriterion/FlipPath.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KirchbergRordam.GenericRW.FlipPath.M2 line 26
2. abbrev OAI.KirchbergRordam.GenericRW.FlipPath.M4 line 27
3. def OAI.KirchbergRordam.GenericRW.FlipPath.flip line 29
4. lemma OAI.KirchbergRordam.GenericRW.FlipPath.flip_star line 31
5. lemma OAI.KirchbergRordam.GenericRW.FlipPath.flip_mul line 36
6. def OAI.KirchbergRordam.GenericRW.FlipPath.left line 41
7. def OAI.KirchbergRordam.GenericRW.FlipPath.right line 42
8. lemma OAI.KirchbergRordam.GenericRW.FlipPath.flip_exchange line 44
9. def OAI.KirchbergRordam.GenericRW.FlipPath.angle line 50
10. def OAI.KirchbergRordam.GenericRW.FlipPath.phase line 52
11. lemma OAI.KirchbergRordam.GenericRW.FlipPath.phase_zero line 56
12. lemma OAI.KirchbergRordam.GenericRW.FlipPath.phase_top line 60
13. lemma OAI.KirchbergRordam.GenericRW.FlipPath.phase_unitary line 67
14. def OAI.KirchbergRordam.GenericRW.FlipPath.path line 75
15. lemma OAI.KirchbergRordam.GenericRW.FlipPath.path_zero line 77
16. lemma OAI.KirchbergRordam.GenericRW.FlipPath.path_top line 78
17. lemma OAI.KirchbergRordam.GenericRW.FlipPath.path_continuous line 80
18. lemma OAI.KirchbergRordam.GenericRW.FlipPath.path_star_mul line 82
19. lemma OAI.KirchbergRordam.GenericRW.FlipPath.path_mul_star line 103
20. def OAI.KirchbergRordam.GenericRW.FlipPath.block line 108
21. lemma OAI.KirchbergRordam.GenericRW.FlipPath.block_star line 128
22. def OAI.KirchbergRordam.GenericRW.FlipPath.conePath line 131
23. lemma OAI.KirchbergRordam.GenericRW.FlipPath.conePath_star_mul line 142
24. lemma OAI.KirchbergRordam.GenericRW.FlipPath.conePath_mul_star line 155
25. def OAI.KirchbergRordam.GenericRW.RWFunctions.realG line 172
26. def OAI.KirchbergRordam.GenericRW.RWFunctions.g line 173
27. def OAI.KirchbergRordam.GenericRW.RWFunctions.q line 174
28. def OAI.KirchbergRordam.GenericRW.RWFunctions.realJ line 176
29. def OAI.KirchbergRordam.GenericRW.RWFunctions.j line 178
30. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_nonneg line 181
31. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_le_one line 185
32. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_ge_defect line 189
33. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_zero line 197
34. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_one line 201
35. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.q_one line 205
36. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.j_one line 209
37. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_low line 214
38. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_norm line 220
39. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.q_star line 228
40. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.g_star line 232
41. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.j_star line 236
42. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.q_sq line 239
43. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.residual_inverse line 245
44. lemma OAI.KirchbergRordam.GenericRW.RWFunctions.overlap_zero line 255
45. lemma OAI.KirchbergRordam.GenericRW.ConeModel.scalar_commute line 260
46. def OAI.KirchbergRordam.GenericRW.FlipPath.flatK line 271
47. def OAI.KirchbergRordam.GenericRW.FlipPath.weightedK line 273
48. def OAI.KirchbergRordam.GenericRW.FlipPath.scalarG line 277
49. def OAI.KirchbergRordam.GenericRW.FlipPath.scalarQ line 279
50. lemma OAI.KirchbergRordam.GenericRW.FlipPath.scalarQ_star line 281
51. lemma OAI.KirchbergRordam.GenericRW.FlipPath.scalarQ_sq line 286
52. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weighted_mul line 291
53. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weighted_mul' line 297
54. lemma OAI.KirchbergRordam.GenericRW.FlipPath.flatK_star_mul line 301
55. lemma OAI.KirchbergRordam.GenericRW.FlipPath.flatK_mul_star line 307
56. lemma OAI.KirchbergRordam.GenericRW.FlipPath.coe_defect_sum line 313
57. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedK_star_mul line 317
58. lemma OAI.KirchbergRordam.GenericRW.FlipPath.weightedK_mul_star line 329