OAI/Probability/IsingPerceptron/FullReplicaIBP.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Full Replica I B P.

  1. theorem OAI.IsingPerceptron.Main.replicated_gaussian_cross_ibp line 15
  2. lemma OAI.IsingPerceptron.Main.fullTensor_selected_cross line 53
  3. lemma OAI.IsingPerceptron.Main.replicated_linear_cross_ibp line 77
  4. theorem OAI.IsingPerceptron.Main.fullTensor_replica_ibp line 95
  5. theorem OAI.IsingPerceptron.Main.fullTensor_raw_replica_ibp line 123
  6. lemma OAI.IsingPerceptron.Main.finiteGibbs_abs_expectation line 151
  7. lemma OAI.IsingPerceptron.Main.replicatedGibbs_centered_bound line 159
  8. def OAI.IsingPerceptron.Main.tensorReplicaCentered line 172
  9. lemma OAI.IsingPerceptron.Main.tensorReplicaCentered_measurable line 179
  10. lemma OAI.IsingPerceptron.Main.tensorReplicaCentered_bound line 187
  11. lemma OAI.IsingPerceptron.Main.tensorReplicaCentered_integrable line 197
  12. lemma OAI.IsingPerceptron.Main.tensorReplicaCentered_integral_bound line 206
  13. def OAI.IsingPerceptron.Main.sourceReplicaCentered line 221
  14. lemma OAI.IsingPerceptron.Main.sourceReplicaCentered_bound line 229
  15. theorem OAI.IsingPerceptron.Main.source_good_replica_factorization line 242
  16. def OAI.IsingPerceptron.Main.tensorReplicaRaw line 260
  17. def OAI.IsingPerceptron.Main.tensorReplicaResponse line 266
  18. lemma OAI.IsingPerceptron.Main.tensorReplicaRaw_measurable line 274
  19. lemma OAI.IsingPerceptron.Main.tensorReplicaRaw_integrable line 282
  20. lemma OAI.IsingPerceptron.Main.perturbed_replica_test_integrable line 298
  21. lemma OAI.IsingPerceptron.Main.tensorReplicaResponse_integrable line 307
  22. theorem OAI.IsingPerceptron.Main.actual_joint_tensor_replica_ibp line 325
  23. lemma OAI.IsingPerceptron.Main.spinOverlap_self line 346
  24. def OAI.IsingPerceptron.Main.tensorReplicaTest line 352
  25. def OAI.IsingPerceptron.Main.tensorPairOverlap line 356
  26. lemma OAI.IsingPerceptron.Main.tensorPairOverlap_integrable line 361
  27. lemma OAI.IsingPerceptron.Main.tensorMeanAt_eq_raw_one line 375
  28. lemma OAI.IsingPerceptron.Main.tensorResponse_one line 382
  29. lemma OAI.IsingPerceptron.Main.actual_tensor_mean_ibp line 397
  30. def OAI.IsingPerceptron.Main.tensorGGResidual line 408
  31. lemma OAI.IsingPerceptron.Main.tensorReplicaCentered_eq line 414
  32. theorem OAI.IsingPerceptron.Main.actual_finite_GG_identity line 422
  33. lemma OAI.IsingPerceptron.Main.actual_finite_GG_bound line 436
  34. def OAI.IsingPerceptron.Main.sourcePolynomialGGResidual line 456
  35. lemma OAI.IsingPerceptron.Main.sourcePolynomialGGResidual_bound line 463
  36. theorem OAI.IsingPerceptron.Main.source_good_polynomial_GG line 474
  37. def OAI.IsingPerceptron.spinBoolEquiv line 494
  38. lemma OAI.IsingPerceptron.spinBoolEquiv_value line 497
  39. def OAI.IsingPerceptron.disorderCurry line 504
  40. lemma OAI.IsingPerceptron.disorderCurry_preserving line 508
  41. lemma OAI.IsingPerceptron.patternEvaluation_equivalent line 517
  42. lemma OAI.IsingPerceptron.pressure_equivalent line 524
  43. lemma OAI.IsingPerceptron.meanPressure_equivalent line 535
  44. lemma OAI.IsingPerceptron.pressure_variance_equivalent line 541
  45. theorem OAI.IsingPerceptron.pressure_variance_bound line 551
  46. lemma OAI.IsingPerceptron.pressure_tail_equivalent line 558
  47. theorem OAI.IsingPerceptron.pressure_tail_bound line 567
  48. theorem OAI.IsingPerceptron.pressure_centered_concentration line 575
  49. def OAI.IsingPerceptron.PressureConvergesInProbability line 582
  50. theorem OAI.IsingPerceptron.pressure_probability_of_expected_limit line 587
  51. lemma OAI.IsingPerceptron.bounded_continuous_activation line 607