OAI/Probability/ParisiFinite/RotateIJApply.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Rotate I J Apply.

  1. theorem OAI.QuaternionControl.rotateIJ_apply line 26
  2. theorem OAI.QuaternionControl.toPauli_apply line 29
  3. def OAI.QuaternionControl.matrixMap line 33
  4. theorem OAI.QuaternionControl.matrixMap_apply line 45
  5. def OAI.QuaternionControl.spinGen line 49
  6. theorem OAI.QuaternionControl.matrixMap_gen line 53
  7. theorem OAI.QuaternionControl.matrixMap_qX line 69
  8. theorem OAI.QuaternionControl.exact_spin_ensemble line 80
  9. theorem OAI.PulseControl.pulseClock_reverse line 109
  10. theorem OAI.PulseControl.pulseClock_eq_sum line 113
  11. theorem OAI.QuaternionControl.matrix_exp_apply line 134
  12. theorem OAI.QuaternionControl.spin_pulseValue_apply line 138
  13. theorem OAI.QuaternionControl.selective_rotations_zero_clocks line 143
  14. def OAI.SKQAOA.History line 168
  15. instance OAI.SKQAOA.historyFintype line 172
  16. def OAI.SKQAOA.historyMix line 177
  17. def OAI.SKQAOA.historyPhase line 183
  18. theorem OAI.SKQAOA.sum_history_zero line 188
  19. theorem OAI.SKQAOA.sum_history_succ line 193
  20. theorem OAI.SKQAOA.historyPhase_succ_sum line 197
  21. theorem OAI.SKQAOA.cost_evolution_mulVec line 211
  22. theorem OAI.SKQAOA.qaoaState_history line 218
  23. def OAI.SKQAOA.pairedPhase line 247
  24. def OAI.SKQAOA.pairedMix line 250
  25. theorem OAI.SKQAOA.qaoaState_pair_history line 253
  26. theorem OAI.SKQAOA.integrable_history_coordinate line 275
  27. theorem OAI.SKQAOA.integral_history_coordinate line 281
  28. theorem OAI.SKQAOA.quad_cost_history_basis line 296
  29. theorem OAI.SKQAOA.coordinate_state_history line 307
  30. theorem OAI.SKQAOA.integrable_coordinate_state line 320
  31. theorem OAI.SKQAOA.integral_coordinate_state line 328
  32. theorem OAI.SKQAOA.integrable_quad_cost line 342
  33. theorem OAI.SKQAOA.expectedEnergy_history line 350