OAI/RepresentationTheory/SpinAngle/Compression.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SpinAngle.Analytic.norm_mul_projection_sq line 40
2. lemma OAI.SpinAngle.Analytic.norm_projection_mul_sq line 50
3. lemma OAI.SpinAngle.Analytic.norm_mul_projection_sq_le_sum line 62
4. lemma OAI.SpinAngle.Analytic.norm_projection_mul_sq_le_sum line 83
5. lemma OAI.SpinAngle.Analytic.support_inverse_factorization line 100
6. lemma OAI.SpinAngle.Analytic.norm_support_inverse_le line 114
7. lemma OAI.SpinAngle.Analytic.norm_projection_sqrt_sq line 126
8. lemma OAI.SpinAngle.Analytic.norm_three_projections_sq_le_one line 136
9. theorem OAI.SpinAngle.Analytic.three_projection_angle_of_density_mixtures line 158