OAI/Combinatorics/ThinTrees/Signing/RationalSigning.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Rational signing.

  1. def OAI.AlgorithmicThinTrees.RationalSigning.entry line 18
  2. lemma OAI.AlgorithmicThinTrees.RationalSigning.entry_value line 20
  3. def OAI.AlgorithmicThinTrees.RationalSigning.input line 23
  4. def OAI.AlgorithmicThinTrees.RationalSigning.selected line 28
  5. def OAI.AlgorithmicThinTrees.RationalSigning.realVec line 31
  6. def OAI.AlgorithmicThinTrees.RationalSigning.outer line 33
  7. lemma OAI.AlgorithmicThinTrees.RationalSigning.input_matrix line 36
  8. lemma OAI.AlgorithmicThinTrees.RationalSigning.complex_outer line 44
  9. lemma OAI.AlgorithmicThinTrees.RationalSigning.input_admissible line 49
  10. lemma OAI.AlgorithmicThinTrees.RationalSigning.outer_psd line 55
  11. lemma OAI.AlgorithmicThinTrees.RationalSigning.outer_square line 58
  12. lemma OAI.AlgorithmicThinTrees.RationalSigning.complexMatrix_sum line 65
  13. lemma OAI.AlgorithmicThinTrees.RationalSigning.variance_eq line 70
  14. lemma OAI.AlgorithmicThinTrees.RationalSigning.scalar_order line 79
  15. lemma OAI.AlgorithmicThinTrees.RationalSigning.variance_bound line 84
  16. lemma OAI.AlgorithmicThinTrees.RationalSigning.signed_eq line 102
  17. lemma OAI.AlgorithmicThinTrees.RationalSigning.half_identity line 111
  18. theorem OAI.AlgorithmicThinTrees.RationalSigning.half_bounds line 121