OAI/Probability/ParisiFinite/BalancedConeEqForest.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Balanced Cone Eq Forest.

  1. theorem OAI.SKQAOA.SiteHistories.balanced_cone_eq_forest line 49
  2. theorem OAI.SKQAOA.SiteHistories.nonzero_shape_is_forest line 61
  3. theorem OAI.SKQAOA.SiteHistories.energySliceLimit_eq_forests line 82
  4. theorem OAI.SKQAOA.SiteHistories.continuous_step line 109
  5. theorem OAI.SKQAOA.SiteHistories.continuous_mix line 113
  6. theorem OAI.SKQAOA.SiteHistories.continuous_weight line 123
  7. theorem OAI.SKQAOA.SiteHistories.continuous_interaction line 128
  8. theorem OAI.SKQAOA.SiteHistories.continuous_delta line 138
  9. theorem OAI.SKQAOA.SiteHistories.continuous_angleMass line 143
  10. theorem OAI.SKQAOA.SiteHistories.continuous_variation line 153
  11. theorem OAI.SKQAOA.SiteHistories.continuous_activity line 158
  12. theorem OAI.SKQAOA.SiteHistories.continuous_markedBound line 163
  13. theorem OAI.SKQAOA.SiteHistories.continuous_tower line 168
  14. theorem OAI.SKQAOA.SiteHistories.continuous_tailConstant line 176
  15. theorem OAI.SKQAOA.SiteHistories.continuous_graphCoefficientLimit line 181
  16. theorem OAI.SKQAOA.SiteHistories.continuous_shapeTermLimit line 195
  17. theorem OAI.SKQAOA.SiteHistories.continuous_energySliceLimit line 200
  18. theorem OAI.UniformApproximation.continuous_of_geometric_approximants line 216
  19. def OAI.SKQAOA.SiteHistories.valueApprox line 253
  20. theorem OAI.SKQAOA.SiteHistories.continuous_valueApprox line 256
  21. theorem OAI.SKQAOA.SiteHistories.value_approx_error line 263
  22. theorem OAI.SKQAOA.continuous_value line 283
  23. theorem OAI.SKQAOA.SiteHistories.norm_energySlice_bound line 306
  24. theorem OAI.SKQAOA.SiteHistories.norm_energySliceLimit_bound line 323
  25. theorem OAI.SKQAOA.SiteHistories.summable_energySliceLimit line 330
  26. theorem OAI.SKQAOA.SiteHistories.value_eq_support_series line 342
  27. theorem OAI.SKQAOA.SiteHistories.value_eq_forest_series line 361
  28. def OAI.RawPulseControl.words line 385
  29. theorem OAI.RawPulseControl.words_unitary line 394
  30. theorem OAI.RawPulseControl.closure_unitary line 402
  31. def OAI.RawPulseControl.directions line 408
  32. theorem OAI.RawPulseControl.generator_mem line 411
  33. theorem OAI.RawPulseControl.bracket_mem line 416
  34. theorem OAI.RawPulseControl.closed_directions line 425
  35. theorem OAI.RawPulseControl.approximate line 431
  36. abbrev OAI.CompactSeedControl.SpinField line 448
  37. def OAI.CompactSeedControl.X line 452
  38. def OAI.CompactSeedControl.Y line 454
  39. def OAI.CompactSeedControl.Z line 456
  40. theorem OAI.CompactSeedControl.X_apply line 460
  41. theorem OAI.CompactSeedControl.Y_apply line 464
  42. theorem OAI.CompactSeedControl.Z_apply line 468
  43. theorem OAI.CompactSeedControl.X_add line 473
  44. theorem OAI.CompactSeedControl.X_smul line 479
  45. theorem OAI.CompactSeedControl.Y_smul line 485
  46. theorem OAI.CompactSeedControl.Z_smul line 491
  47. theorem OAI.CompactSeedControl.bracket_ZX line 498
  48. theorem OAI.CompactSeedControl.bracket_ZY line 506
  49. theorem OAI.CompactSeedControl.bracket_YX line 515
  50. def OAI.CompactSeedControl.generator line 524
  51. theorem OAI.CompactSeedControl.generator_skew line 527
  52. def OAI.CompactSeedControl.available line 543
  53. theorem OAI.CompactSeedControl.X_one_mem line 546
  54. theorem OAI.CompactSeedControl.Z_seed_mem line 549
  55. theorem OAI.CompactSeedControl.Y_seed_mul_mem line 552
  56. theorem OAI.CompactSeedControl.X_sq_mul_mem line 559
  57. theorem OAI.CompactSeedControl.X_even_power_mem line 567
  58. theorem OAI.CompactSeedControl.X_even_polynomial_mem line 574
  59. theorem OAI.CompactSeedControl.Z_seed_mul_mem line 583
  60. theorem OAI.CompactSeedControl.polynomial_pulse_approximation line 592
  61. theorem OAI.CompactSeedControl.continuous_X line 612
  62. theorem OAI.CompactSeedControl.continuous_Y line 617
  63. theorem OAI.CompactSeedControl.continuous_Z line 622
  64. theorem OAI.CompactSeedControl.X_function_square_mem line 628
  65. theorem OAI.CompactSeedControl.X_even_continuous_mem line 657
  66. theorem OAI.CompactSeedControl.even_continuous_pulse_approximation line 670