OAI/Analysis/Steinitz/Correlation.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanSteinitz.GaussianCorrelation.one_le_det line 15
2. lemma OAI.EuclideanSteinitz.GaussianCorrelation.det_mono line 24
3. def OAI.EuclideanSteinitz.GaussianCorrelation.blockCov line 41
4. lemma OAI.EuclideanSteinitz.GaussianCorrelation.blockCov_schur line 44
5. lemma OAI.EuclideanSteinitz.GaussianCorrelation.blockCov_affine line 53
6. lemma OAI.EuclideanSteinitz.GaussianCorrelation.blockCov_diag_posDef line 59
7. lemma OAI.EuclideanSteinitz.GaussianCorrelation.schur_posDef line 65
8. lemma OAI.EuclideanSteinitz.GaussianCorrelation.blockCov_posDef line 80
9. lemma OAI.EuclideanSteinitz.GaussianCorrelation.blockCov_det_antitone line 104
10. def OAI.EuclideanSteinitz.GaussianCorrelation.interpolate line 125
11. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_one line 129
12. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_blocks line 134
13. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_posDef line 150
14. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_det_antitone line 165
15. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_det_differentiable line 179
16. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_submatrix line 191
17. lemma OAI.EuclideanSteinitz.GaussianCorrelation.principal_minor_deriv_nonpos line 196
18. lemma OAI.EuclideanSteinitz.GaussianCorrelation.det_diagonal_mul_add_one line 206
19. lemma OAI.EuclideanSteinitz.GaussianCorrelation.det_interpolate_derivative line 225
20. lemma OAI.EuclideanSteinitz.GaussianCorrelation.integral_exp_square_gaussian line 244
21. lemma OAI.EuclideanSteinitz.GaussianCorrelation.integrable_exp_square_gaussian line 260
22. lemma OAI.EuclideanSteinitz.GaussianCorrelation.eigenvector_toEuclideanCLM line 272
23. lemma OAI.EuclideanSteinitz.GaussianCorrelation.quadratic_eigenbasis line 278
24. lemma OAI.EuclideanSteinitz.GaussianCorrelation.det_one_add_eigenvalues line 287
25. lemma OAI.EuclideanSteinitz.GaussianCorrelation.quadratic_laplace_stdGaussian line 299
26. lemma OAI.EuclideanSteinitz.GaussianCorrelation.quadratic_diagonal line 327
27. lemma OAI.EuclideanSteinitz.GaussianCorrelation.quadratic_sandwich line 335
28. lemma OAI.EuclideanSteinitz.GaussianCorrelation.sqrt_sandwich_psd line 344
29. lemma OAI.EuclideanSteinitz.GaussianCorrelation.det_one_add_sqrt_sandwich line 350
30. lemma OAI.EuclideanSteinitz.GaussianCorrelation.det_diagonal_mul_add_one_pos line 355
31. lemma OAI.EuclideanSteinitz.GaussianCorrelation.quadratic_laplace_multivariateGaussian line 360
32. lemma OAI.EuclideanSteinitz.GaussianCorrelation.integrable_quadratic_exp line 371
33. def OAI.EuclideanSteinitz.GaussianCorrelation.laplaceKernel line 390
34. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplaceKernel_nonneg line 393
35. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplaceKernel_le_one line 397
36. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplaceKernel_add line 403
37. lemma OAI.EuclideanSteinitz.GaussianCorrelation.continuous_laplaceKernel line 409
38. lemma OAI.EuclideanSteinitz.GaussianCorrelation.measurableSet_nonnegative line 414
39. def OAI.EuclideanSteinitz.GaussianCorrelation.squareLaw line 418
40. instance OAI.EuclideanSteinitz.GaussianCorrelation.squareLaw_isProbabilityMeasure line 421
41. lemma OAI.EuclideanSteinitz.GaussianCorrelation.squareLaw_nonneg line 427
42. lemma OAI.EuclideanSteinitz.GaussianCorrelation.integrable_laplaceKernel line 434
43. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplace_squareLaw line 442
44. def OAI.EuclideanSteinitz.GaussianCorrelation.sumLaw line 451
45. instance OAI.EuclideanSteinitz.GaussianCorrelation.sumLaw_isProbabilityMeasure line 454
46. lemma OAI.EuclideanSteinitz.GaussianCorrelation.sumLaw_nonneg line 461
47. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplace_sumLaw line 471
48. def OAI.EuclideanSteinitz.GaussianCorrelation.tripleSquareLaw line 480
49. instance OAI.EuclideanSteinitz.GaussianCorrelation.tripleSquareLaw_isProbabilityMeasure line 483
50. lemma OAI.EuclideanSteinitz.GaussianCorrelation.tripleSquareLaw_nonneg line 487
51. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplace_tripleSquareLaw line 492
52. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomial_euler_eval line 507
53. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomial_eval_exp line 520
54. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomial_euler_exp line 526
55. abbrev OAI.EuclideanSteinitz.GaussianCorrelation.PolynomialIndex line 532
56. def OAI.EuclideanSteinitz.GaussianCorrelation.polynomialWeight line 534
57. def OAI.EuclideanSteinitz.GaussianCorrelation.exponentVector line 537
58. def OAI.EuclideanSteinitz.GaussianCorrelation.mixedMultiplier line 539
59. def OAI.EuclideanSteinitz.GaussianCorrelation.mixedPolynomial line 542
60. lemma OAI.EuclideanSteinitz.GaussianCorrelation.mixedPolynomial_expansion line 546
61. lemma OAI.EuclideanSteinitz.GaussianCorrelation.mixedPolynomial_nonneg line 566
62. lemma OAI.EuclideanSteinitz.GaussianCorrelation.integrable_mixedPolynomial line 578
63. lemma OAI.EuclideanSteinitz.GaussianCorrelation.integral_mixedPolynomial line 588
64. def OAI.EuclideanSteinitz.GaussianCorrelation.royenCoefficient line 606
65. lemma OAI.EuclideanSteinitz.GaussianCorrelation.royenCoefficient_nonneg line 612
66. lemma OAI.EuclideanSteinitz.GaussianCorrelation.laplace_interpolate_derivative line 616
67. def OAI.EuclideanSteinitz.GaussianCorrelation.polynomialExpectation line 639
68. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomialExpectation_eq_integral line 643
69. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomialExpectation_derivative line 653
70. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomialExpectation_monotone line 680
71. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomial_correlation_interpolate line 701
72. def OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP line 721
73. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP_derivative line 724
74. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP_eval line 750
75. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP_eval_nonneg line 761
76. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP_eval_le_one line 770
77. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP_derivative_nonneg line 779
78. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernsteinP_tendsto line 803
79. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_zero_posSemidef line 817
80. lemma OAI.EuclideanSteinitz.GaussianCorrelation.interpolate_continuous line 830
81. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomialExpectation_continuousAt line 839
82. lemma OAI.EuclideanSteinitz.GaussianCorrelation.polynomial_correlation_psd line 850
83. def OAI.EuclideanSteinitz.GaussianCorrelation.continuousProduct line 876
84. lemma OAI.EuclideanSteinitz.GaussianCorrelation.bernstein_integral_tendsto line 879
85. lemma OAI.EuclideanSteinitz.GaussianCorrelation.continuous_correlation_interpolate line 905
86. def OAI.EuclideanSteinitz.GaussianCorrelation.upperCutoff line 928
87. lemma OAI.EuclideanSteinitz.GaussianCorrelation.upperCutoff_bounds line 931
88. lemma OAI.EuclideanSteinitz.GaussianCorrelation.upperCutoff_monotone line 935
89. lemma OAI.EuclideanSteinitz.GaussianCorrelation.upperCutoff_tendsto line 940
90. def OAI.EuclideanSteinitz.GaussianCorrelation.exponentialBox line 962
91. lemma OAI.EuclideanSteinitz.GaussianCorrelation.measurableSet_exponentialBox line 966
92. lemma OAI.EuclideanSteinitz.GaussianCorrelation.cutoffProduct_tendsto line 972
93. lemma OAI.EuclideanSteinitz.GaussianCorrelation.cutoff_integral_tendsto line 991
94. lemma OAI.EuclideanSteinitz.GaussianCorrelation.rectangle_correlation_interpolate line 1007
95. def OAI.EuclideanSteinitz.GaussianCorrelation.coordinatePi line 1024
96. def OAI.EuclideanSteinitz.GaussianCorrelation.coordinateCLM line 1027
97. lemma OAI.EuclideanSteinitz.GaussianCorrelation.coordinateCLM_apply line 1032
98. lemma OAI.EuclideanSteinitz.GaussianCorrelation.map_coordinate_multivariateGaussian line 1035
99. lemma OAI.EuclideanSteinitz.GaussianCorrelation.block_submatrix_eq line 1059
100. lemma OAI.EuclideanSteinitz.GaussianCorrelation.gaussian_blocks_independent line 1067
101. def OAI.EuclideanSteinitz.GaussianCorrelation.quadraticBox line 1081
102. lemma OAI.EuclideanSteinitz.GaussianCorrelation.measurableSet_quadraticBox line 1085
103. lemma OAI.EuclideanSteinitz.GaussianCorrelation.squareLaw_exponentialBox line 1091
104. lemma OAI.EuclideanSteinitz.GaussianCorrelation.quadratic_correlation_interpolate line 1101
105. lemma OAI.EuclideanSteinitz.GaussianCorrelation.block_marginal_eq line 1109
106. lemma OAI.EuclideanSteinitz.GaussianCorrelation.gaussian_quadraticBox_correlation line 1119
107. def OAI.EuclideanSteinitz.GaussianCorrelation.innerCoordinates line 1181
108. lemma OAI.EuclideanSteinitz.GaussianCorrelation.innerCoordinates_apply line 1186
109. lemma OAI.EuclideanSteinitz.GaussianCorrelation.map_innerCoordinates_stdGaussian line 1189
110. lemma OAI.EuclideanSteinitz.GaussianCorrelation.stdGaussian_finite_slabs_correlation line 1213
111. lemma OAI.EuclideanSteinitz.GaussianCorrelation.closed_symmetric_convex_countable_slabs line 1243
112. def OAI.EuclideanSteinitz.GaussianCorrelation.partialSlabs line 1276
113. lemma OAI.EuclideanSteinitz.GaussianCorrelation.measurableSet_partialSlabs line 1280
114. lemma OAI.EuclideanSteinitz.GaussianCorrelation.partialSlabs_antitone line 1288
115. lemma OAI.EuclideanSteinitz.GaussianCorrelation.partialSlabs_iInter line 1293
116. lemma OAI.EuclideanSteinitz.GaussianCorrelation.stdGaussian_partialSlabs_correlation line 1301
117. lemma OAI.EuclideanSteinitz.GaussianCorrelation.tendsto_real_measure_decreasing line 1325
118. lemma OAI.EuclideanSteinitz.GaussianCorrelation.stdGaussian_closed_convex_correlation line 1332
119. lemma OAI.EuclideanSteinitz.GaussianCorrelation.linear_image_closed_convex_correlation line 1372
120. lemma OAI.EuclideanSteinitz.GaussianCorrelation.linear_image_finite_correlation line 1389