OAI/Probability/BinarySweep/TensorBounds/PiTensorMatrices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Density.piTensorMatrices line 15
2. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_mul line 21
3. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_star line 30
4. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_one line 36
5. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_psd line 44
6. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_trace line 58
7. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_smul line 65
8. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_sum line 72
9. lemma OAI.BinaryCoordinateSweeps.Density.piTensorMatrices_mono line 79
10. theorem OAI.BinaryCoordinateSweeps.Density.piTensor_density_domination line 99