OAI/MeasureTheory/CompactFactors/RelativeProducts.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.EuclideanFiveColor.RelativeProduct.law_probability_add line 19
2. lemma OAI.EuclideanFiveColor.RelativeProduct.conditional_covariance_add line 24
3. lemma OAI.EuclideanFiveColor.RelativeProduct.law_preserving_add line 34
4. lemma OAI.EuclideanFiveColor.RelativeProduct.law_invariant_add line 68
5. def OAI.EuclideanFiveColor.BoundedMeasurable.projectCLM line 88
6. lemma OAI.EuclideanFiveColor.BoundedMeasurable.projectCLM_l2 line 92
7. lemma OAI.EuclideanFiveColor.BoundedMeasurable.norm_project_l2 line 97
8. def OAI.EuclideanFiveColor.BoundedMeasurable.act line 111
9. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_apply line 112
10. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_add line 113
11. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_mul line 116
12. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_conj line 117
13. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_sub line 118
14. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_act line 121
15. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_sub line 133
16. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_bound line 137
17. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_comp line 139
18. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_project line 141
19. lemma OAI.EuclideanFiveColor.BoundedMeasurable.center_project_l2 line 143
20. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_pullout line 149
21. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_mul_lift line 153
22. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_act line 164
23. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_lift line 175
24. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_act line 182
25. def OAI.EuclideanFiveColor.BoundedMeasurable.familyAlgebra line 194
26. abbrev OAI.EuclideanFiveColor.BoundedMeasurable.Family line 208
27. instance OAI.EuclideanFiveColor.BoundedMeasurable.(instance at line 210) line 210
28. instance OAI.EuclideanFiveColor.BoundedMeasurable.familyRealModule line 211
29. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.bound line 214
30. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.norm_le_bound line 215
31. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.ext line 216
32. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.add_apply line 217
33. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.mul_apply line 218
34. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.sub_apply line 219
35. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.zero_apply line 220
36. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.one_apply line 221
37. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.real_smul_apply line 222
38. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.complex_smul_apply line 223
39. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.prod_apply line 224
40. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.const line 231
41. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.const_apply line 233
42. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.bmConj line 235
43. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.conj_apply line 237
44. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.toL2 line 242
45. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.toL2_apply line 245
46. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.l2Linear line 247
47. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.avg line 259
48. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.avg_pair line 264
49. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.avg_congr_ae line 267
50. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.orbit line 276
51. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.orbit_apply line 279
52. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.orbit_add line 280
53. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.orbit_sub line 281
54. def OAI.EuclideanFiveColor.BoundedMeasurable.tensor line 291
55. lemma OAI.EuclideanFiveColor.BoundedMeasurable.tensor_apply line 293
56. lemma OAI.EuclideanFiveColor.BoundedMeasurable.tensor_mul line 294
57. lemma OAI.EuclideanFiveColor.BoundedMeasurable.tensor_conj line 296
58. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_law line 302
59. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_tensor line 311
60. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_tensor_self line 318
61. lemma OAI.EuclideanFiveColor.BoundedMeasurable.inner_tensor line 331
62. lemma OAI.EuclideanFiveColor.Amenable.Koopman.vector_orbit_hom_zero line 358
63. instance OAI.EuclideanFiveColor.BoundedMeasurable.product_measurable_vadd line 372
64. def OAI.EuclideanFiveColor.BoundedMeasurable.pairSequence line 376
65. lemma OAI.EuclideanFiveColor.BoundedMeasurable.pairSequence_apply line 391
66. lemma OAI.EuclideanFiveColor.BoundedMeasurable.tensor_act line 395
67. lemma OAI.EuclideanFiveColor.BoundedMeasurable.pair_mean_sq_zero line 401
68. lemma OAI.EuclideanFiveColor.AlgebraReplacement.mixed_prod line 433
69. lemma OAI.EuclideanFiveColor.AlgebraReplacement.linear_prod_replace line 442
70. lemma OAI.EuclideanFiveColor.AlgebraReplacement.add_prod_replace line 456