OAI/Analysis/FreeWords/ControlledMatrixConjugation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKControlledConjugation.amplifyConj line 17
  2. theorem OAI.KKControlledConjugation.amplifyConj_apply line 26
  3. theorem OAI.KKControlledConjugation.conj_trace line 31
  4. theorem OAI.KKControlledConjugation.amplifyConj_trace line 37
  5. theorem OAI.KKControlledConjugation.amplifyConj_expectation line 42
  6. theorem OAI.KKControlledConjugation.amplifyConj_numerical line 48
  7. theorem OAI.KKControlledConjugation.amplifyConj_entry_range line 54
  8. theorem OAI.KKControlledConjugation.amplifyConj_eq_scalarConjugate line 65