OAI/Probability/BinarySweep/MatrixBounds/MatrixRegularize.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Density.meanDensity line 14
2. def OAI.BinaryCoordinateSweeps.Density.regularizedMean line 17
3. lemma OAI.BinaryCoordinateSweeps.Density.meanDensity_psd line 21
4. lemma OAI.BinaryCoordinateSweeps.Density.meanDensity_trace line 26
5. lemma OAI.BinaryCoordinateSweeps.Density.regularizedMean_trace line 31
6. lemma OAI.BinaryCoordinateSweeps.Density.regularizedMean_posDef line 37
7. lemma OAI.BinaryCoordinateSweeps.Density.regularizedMean_even line 46
8. lemma OAI.BinaryCoordinateSweeps.Density.whitened_column_budget line 54