OAI/Probability/SignedSweeps/HilbertBlockNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.orthogonal_adjoint_norm_sq_le line 13
2. lemma OAI.SignedSweeps.hilbertBlock_sum_norm_le line 35
3. lemma OAI.SignedSweeps.hilbertBlock_left_intertwine line 51
4. lemma OAI.SignedSweeps.pairTypeProjection_norm_le line 65
5. theorem OAI.SignedSweeps.pairTypeProjection_norm_of_factors line 71