OAI/Probability/ParisiFinite/FiniteMaxHamiltonian.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Finite Max Hamiltonian.

  1. theorem OAI.SKQAOA.finiteMax_hamiltonian line 17
  2. theorem OAI.SKQAOA.log_card_configuration line 21
  3. theorem OAI.SKQAOA.finite_pressure_bounds line 25
  4. theorem OAI.SKQAOA.pressure_bounds line 37
  5. theorem OAI.SKQAOA.pressure_linear_bound line 52
  6. theorem OAI.SKQAOA.tendsto_freeEnergy line 59
  7. theorem OAI.SKQAOA.freeEnergy_bounds line 84
  8. theorem OAI.SKQAOA.limitingFreeEnergy_bounds line 103
  9. theorem OAI.PulseControl.exp_hasFDerivAt_zero line 128
  10. theorem OAI.PulseControl.exp_curve_deriv_zero line 135
  11. theorem OAI.PulseControl.norm_pow_sub_pow_le line 144
  12. theorem OAI.PulseControl.tendsto_tangent_powers line 162
  13. theorem OAI.PulseControl.exp_mul_exp_neg line 200
  14. theorem OAI.PulseControl.exp_neg_mul_exp line 204
  15. theorem OAI.PulseControl.norm_exp_smul_le line 210
  16. theorem OAI.PulseControl.tangent_mem_closed_submonoid line 215
  17. def OAI.PulseControl.tangents line 224
  18. theorem OAI.PulseControl.mem_tangents line 240
  19. theorem OAI.PulseControl.isClosed_tangents line 243
  20. theorem OAI.PulseControl.conjugation_deriv_zero line 251
  21. theorem OAI.PulseControl.star_exp_smul line 259
  22. theorem OAI.PulseControl.commutator_loop_tangent_mem line 263
  23. theorem OAI.PulseControl.normalized_bracket_mem line 294
  24. def OAI.PulseControl.pulseValue line 309
  25. def OAI.PulseControl.pulseClock line 312
  26. theorem OAI.PulseControl.pulseValue_nil line 316
  27. theorem OAI.PulseControl.pulseValue_append line 319
  28. theorem OAI.PulseControl.pulseClock_nil line 323
  29. theorem OAI.PulseControl.pulseClock_append line 325
  30. def OAI.PulseControl.zeroClockWords line 330
  31. theorem OAI.PulseControl.commutator_loop_mem line 337
  32. theorem OAI.PulseControl.conjugate_word_mem line 347
  33. theorem OAI.PulseControl.conjugate_closure_mem line 358
  34. theorem OAI.PulseControl.zeroClockWords_le_unitary line 375
  35. theorem OAI.PulseControl.closure_le_unitary line 383
  36. def OAI.PulseControl.zeroClockTangents line 389
  37. theorem OAI.PulseControl.bracket_mem_zeroClockTangents line 392
  38. theorem OAI.PulseControl.bracket_closed_zeroClockTangents line 398
  39. theorem OAI.PulseControl.approximate_zeroClock line 407
  40. theorem OAI.ExactPulseControl.contDiff_exp_curve line 426
  41. def OAI.ExactPulseControl.actualTangents line 434
  42. theorem OAI.ExactPulseControl.actualTangents_closed line 450
  43. theorem OAI.ExactPulseControl.bracket_actualTangents line 453
  44. theorem OAI.ExactPulseControl.bracket_closed_actualTangents line 474
  45. theorem OAI.ExactPulseControl.hasStrictFDerivAt_list_prod_one line 506
  46. theorem OAI.ExactPulseControl.projected_reachable_nhds line 525
  47. theorem OAI.ExactPulseControl.surjective_tangents_reachable_nhds line 563