OAI/Probability/LogConcave/Sampling/MatrixColor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.integral_sq_le_of_eLpNorm line 15
2. lemma OAI.LogConcaveSampling.allSplit_integral_frobenius line 45
3. lemma OAI.LogConcaveSampling.TensorSum.spatialTensor_integrable_sq line 63
4. lemma OAI.LogConcaveSampling.TensorSum.spatialTensor_l2 line 77
5. def OAI.LogConcaveSampling.matrixZeroColor line 109
6. def OAI.LogConcaveSampling.matrixOneColor line 120
7. lemma OAI.LogConcaveSampling.matrix_zero_energy_eq line 132
8. lemma OAI.LogConcaveSampling.matrix_one_energy_eq line 139
9. lemma OAI.LogConcaveSampling.TensorSum.slice_integrable_sq line 148
10. lemma OAI.LogConcaveSampling.TensorSum.slice_directional_integrable_sq line 155
11. lemma OAI.LogConcaveSampling.TensorSum.matrix_zero_energy line 163
12. lemma OAI.LogConcaveSampling.TensorSum.matrix_one_energy line 173