OAI/Probability/ParisiFinite/Count.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Count.

  1. def OAI.BinaryOccupations.count line 26
  2. theorem OAI.BinaryOccupations.count_eq_iff line 29
  3. theorem OAI.BinaryOccupations.count_surjective line 32
  4. theorem OAI.BinaryOccupations.fiber_card line 39
  5. def OAI.BinaryOccupations.embedding line 48
  6. theorem OAI.BinaryOccupations.embedding_apply line 52
  7. theorem OAI.BinaryOccupations.mem_range_iff_card line 60
  8. def OAI.SKQAOA.extendAngles line 70
  9. theorem OAI.SKQAOA.expectedEnergy_extendAngles line 74
  10. theorem OAI.SKQAOA.value_extendAngles line 80
  11. theorem OAI.SKQAOA.explicit_ground_lower_bound line 90
  12. theorem OAI.SKQAOA.Pstar_pos line 100
  13. theorem OAI.SKQAOA.exists_positive_word_every_depth line 105
  14. theorem OAI.SKQAOA.hamiltonian_neg_disorder line 124
  15. theorem OAI.SKQAOA.neg_energyDensity_le_groundMaximum line 130
  16. theorem OAI.SKQAOA.disorder_neg_preserving line 149
  17. theorem OAI.SKQAOA.abs_expectedEnergy_le_expectedGround line 158
  18. theorem OAI.SKQAOA.eventually_uniform_expectedEnergy_bound line 181
  19. def OAI.SKQAOA.SiteHistories.Bits line 199
  20. instance OAI.SKQAOA.SiteHistories.bitsFintype line 203
  21. instance OAI.SKQAOA.SiteHistories.bitsDecidableEq line 207
  22. def OAI.SKQAOA.SiteHistories.atVertex line 211
  23. def OAI.SKQAOA.SiteHistories.assemble line 215
  24. theorem OAI.SKQAOA.SiteHistories.atVertex_assemble line 219
  25. theorem OAI.SKQAOA.SiteHistories.assemble_atVertex line 229
  26. def OAI.SKQAOA.SiteHistories.historyEquiv line 238
  27. def OAI.SKQAOA.SiteHistories.step line 244
  28. def OAI.SKQAOA.SiteHistories.mix line 247
  29. lemma OAI.SKQAOA.SiteHistories.sqrt_nat_pow line 251
  30. theorem OAI.SKQAOA.SiteHistories.historyMix_factor line 256
  31. abbrev OAI.SKQAOA.SiteHistories.Site line 267
  32. def OAI.SKQAOA.SiteHistories.weight line 269
  33. def OAI.SKQAOA.SiteHistories.trajectoriesEquiv line 272
  34. theorem OAI.SKQAOA.SiteHistories.trajectoriesEquiv_apply line 280
  35. theorem OAI.SKQAOA.SiteHistories.pairedMix_factor line 284
  36. theorem OAI.SKQAOA.SiteHistories.sum_pairedMix line 291
  37. theorem OAI.SKQAOA.SiteHistories.sum_weight line 303
  38. lemma OAI.SKQAOA.SiteHistories.norm_step_le_one line 314
  39. lemma OAI.SKQAOA.SiteHistories.norm_mix_le_one line 321
  40. lemma OAI.SKQAOA.SiteHistories.norm_weight_le_one line 332
  41. def OAI.SKQAOA.SiteHistories.bitSpin line 338
  42. theorem OAI.SKQAOA.SiteHistories.abs_bitSpin line 340
  43. def OAI.SKQAOA.SiteHistories.interaction line 342
  44. def OAI.SKQAOA.SiteHistories.angleMass line 347
  45. lemma OAI.SKQAOA.SiteHistories.angleMass_nonneg line 351
  46. lemma OAI.SKQAOA.SiteHistories.abs_interaction_le line 356
  47. def OAI.SKQAOA.SiteHistories.delta line 370
  48. lemma OAI.SKQAOA.SiteHistories.abs_delta_le line 373
  49. theorem OAI.SKQAOA.SiteHistories.historyPhase_local line 380
  50. theorem OAI.SKQAOA.SiteHistories.pairedPhase_local line 391
  51. def OAI.SKQAOA.SiteHistories.edgeKernel line 401
  52. lemma OAI.SKQAOA.SiteHistories.edgeKernel_pos line 404
  53. lemma OAI.SKQAOA.SiteHistories.edgeKernel_le_one line 407
  54. lemma OAI.SKQAOA.SiteHistories.abs_edgeKernel_sub_one_le line 413
  55. theorem OAI.SKQAOA.SiteHistories.exp_pairedPhase_sq line 426
  56. def OAI.FiniteHistory.expectation line 446
  57. theorem OAI.FiniteHistory.restrict_expectation line 451
  58. lemma OAI.FiniteHistory.norm_expectation_le line 475
  59. def OAI.FiniteHistory.extend line 492
  60. lemma OAI.FiniteHistory.extend_apply line 496
  61. theorem OAI.FiniteHistory.norm_expectation_le_of_local line 501
  62. lemma OAI.SKQAOA.SiteHistories.tendsto_scaled_exp line 526
  63. def OAI.SKQAOA.SiteHistories.kernelScaled line 538
  64. lemma OAI.SKQAOA.SiteHistories.tendsto_kernel line 541
  65. lemma OAI.SKQAOA.SiteHistories.tendsto_kernelScaled line 554
  66. def OAI.SKQAOA.SiteHistories.graphCoefficient line 565
  67. def OAI.SKQAOA.SiteHistories.graphCoefficientLimit line 573
  68. theorem OAI.SKQAOA.SiteHistories.tendsto_graphCoefficient line 582
  69. theorem OAI.FiniteHistory.expectation_equiv line 617
  70. theorem OAI.FiniteHistory.expectation_embedding line 632