OAI/Probability/SwitchChain/SliceSynthesis.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.SliceSynthesis.Coeff line 15
  2. def OAI.Problem315.SliceSynthesis.ofMatrix line 17
  3. theorem OAI.Problem315.SliceSynthesis.ofMatrix_apply line 21
  4. def OAI.Problem315.SliceSynthesis.synthesis line 26
  5. theorem OAI.Problem315.SliceSynthesis.synthesis_ofMatrix line 32
  6. def OAI.Problem315.SliceSynthesis.symMatrix line 37
  7. theorem OAI.Problem315.SliceSynthesis.symMatrix_diag line 40
  8. theorem OAI.Problem315.SliceSynthesis.symMatrix_symmetric line 43
  9. theorem OAI.Problem315.SliceSynthesis.synthesis_symMatrix line 46
  10. theorem OAI.Problem315.SliceSynthesis.synthesis_constant line 69
  11. theorem OAI.Problem315.SliceSynthesis.ofMatrix_inner line 81
  12. theorem OAI.Problem315.SliceSynthesis.exists_synthesis_decomposition line 87
  13. theorem OAI.Problem315.SliceSynthesis.synthesis_single line 112
  14. theorem OAI.Problem315.SliceSynthesis.adjoint_synthesis_apply line 117
  15. theorem OAI.Problem315.SliceSynthesis.gram_synthesis_apply line 122
  16. theorem OAI.Problem315.SliceSynthesis.comparison_of_scalar_actions line 128