OAI/Probability/BinarySweep/TensorBounds/SignedPinching.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.BinaryCoordinateSweeps.Signed.pinch_traceline 16 - lemma
OAI.BinaryCoordinateSweeps.Signed.comp_parity_eq_iffline 21 - lemma
OAI.BinaryCoordinateSweeps.Signed.pinch_blockline 31 - lemma
OAI.BinaryCoordinateSweeps.Signed.pinch_invariantline 36 - lemma
OAI.BinaryCoordinateSweeps.Signed.signed_sparse_pinchingline 45 - theorem
OAI.BinaryCoordinateSweeps.Signed.signed_psd_postselectionline 66