OAI/Combinatorics/ThinTrees/Signing/StackedSigning.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Stacked signing.

  1. def OAI.AlgorithmicThinTrees.StackedSigning.stack line 15
  2. lemma OAI.AlgorithmicThinTrees.StackedSigning.stack_left line 18
  3. lemma OAI.AlgorithmicThinTrees.StackedSigning.stack_right line 21
  4. lemma OAI.AlgorithmicThinTrees.StackedSigning.dot_stack line 24
  5. lemma OAI.AlgorithmicThinTrees.StackedSigning.stack_norm line 29
  6. def OAI.AlgorithmicThinTrees.StackedSigning.gram line 33
  7. lemma OAI.AlgorithmicThinTrees.StackedSigning.gram_psd line 36
  8. lemma OAI.AlgorithmicThinTrees.StackedSigning.gram_eval line 42
  9. lemma OAI.AlgorithmicThinTrees.StackedSigning.gram_eval_le line 50
  10. lemma OAI.AlgorithmicThinTrees.StackedSigning.stack_covariance line 58
  11. lemma OAI.AlgorithmicThinTrees.StackedSigning.submatrix_mono line 86
  12. lemma OAI.AlgorithmicThinTrees.StackedSigning.gram_submatrix line 91
  13. lemma OAI.AlgorithmicThinTrees.StackedSigning.compress_half line 97
  14. def OAI.AlgorithmicThinTrees.StackedSigning.selected line 112
  15. lemma OAI.AlgorithmicThinTrees.StackedSigning.real_stack line 115
  16. theorem OAI.AlgorithmicThinTrees.StackedSigning.simultaneous line 122