OAI/Analysis/MatrixSigning/Optimization/Outside.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.RationalInput.zero_outside line 15
2. lemma OAI.CurrentKS.RationalInput.trimmed_square_sum line 21
3. lemma OAI.CurrentKS.RationalInput.lifted_signs_abs line 28
4. lemma OAI.CurrentKS.RationalInput.sign_bits_value line 37
5. theorem OAI.CurrentKS.RationalInput.signing_good line 45