OAI/Probability/IsingPerceptron/CountableMonomialGG.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Countable Monomial G G.

  1. def OAI.IsingPerceptron.replicaEnergyMean line 17
  2. def OAI.IsingPerceptron.expectedReplicaEnergy line 21
  3. def OAI.IsingPerceptron.gibbsEnergyMean line 25
  4. def OAI.IsingPerceptron.expectedEnergy line 28
  5. def OAI.IsingPerceptron.freshCovarianceMean line 31
  6. def OAI.IsingPerceptron.expectedFreshCovariance line 35
  7. lemma OAI.IsingPerceptron.integrable_replicaEnergyMean line 39
  8. lemma OAI.IsingPerceptron.expectedReplicaEnergy_const line 44
  9. lemma OAI.IsingPerceptron.integrable_gibbsEnergyMean line 54
  10. lemma OAI.IsingPerceptron.integrable_freshCovarianceMean line 61
  11. theorem OAI.IsingPerceptron.gaussian_replica_energy_formula line 87
  12. lemma OAI.IsingPerceptron.expectedReplica_one line 157
  13. def OAI.IsingPerceptron.pairCovariance line 164
  14. lemma OAI.IsingPerceptron.gaussian_single_energy_formula line 167
  15. theorem OAI.IsingPerceptron.gaussian_gg_residual_identity line 174
  16. def OAI.IsingPerceptron.energyFluctuation line 186
  17. lemma OAI.IsingPerceptron.integrable_gibbs_centered_abs_energy line 190
  18. lemma OAI.IsingPerceptron.energy_covariance_bound line 203
  19. theorem OAI.IsingPerceptron.gaussian_gg_residual_bound line 253
  20. def OAI.IsingPerceptron.referencePartition line 266
  21. def OAI.IsingPerceptron.referenceReplicaMean line 269
  22. lemma OAI.IsingPerceptron.reference_replica_partition line 274
  23. lemma OAI.IsingPerceptron.referenceReplicaMean_eq_ratio line 282
  24. lemma OAI.IsingPerceptron.finite_reference_weights_sum line 289
  25. lemma OAI.IsingPerceptron.finite_reference_weight_pos line 295
  26. lemma OAI.IsingPerceptron.referencePartition_finite line 303
  27. lemma OAI.IsingPerceptron.referenceReplicaMean_finite line 308
  28. lemma OAI.IsingPerceptron.referencePartition_map line 323
  29. lemma OAI.IsingPerceptron.referenceReplicaMean_map line 329
  30. lemma OAI.IsingPerceptron.finite_reference_GibbsReference line 347
  31. lemma OAI.IsingPerceptron.referenceReplicaMean_eq_finite line 352
  32. lemma OAI.IsingPerceptron.replicaMean_fresh_eq line 360
  33. theorem OAI.IsingPerceptron.finite_gaussian_reference_insertion line 383
  34. lemma OAI.IsingPerceptron.gaussian_weighted_sum_law line 419
  35. def OAI.IsingPerceptron.gaussianCoordinates line 452
  36. instance OAI.IsingPerceptron.gaussianCoordinates_probability line 455
  37. lemma OAI.IsingPerceptron.gaussian_prefix_measurePreserving line 458
  38. def OAI.IsingPerceptron.cylinderField line 468
  39. lemma OAI.IsingPerceptron.measurable_cylinderField line 471
  40. lemma OAI.IsingPerceptron.measurable_cylinderFields line 476
  41. lemma OAI.IsingPerceptron.cylinderField_eq_prefix line 481
  42. lemma OAI.IsingPerceptron.finite_family_support_bound line 489
  43. lemma OAI.IsingPerceptron.cylinderField_law line 497
  44. lemma OAI.IsingPerceptron.cylinderField_finset_sum line 514
  45. lemma OAI.IsingPerceptron.cylinder_variance_prefix line 523
  46. lemma OAI.IsingPerceptron.cylinder_variance_sum_le line 530
  47. def OAI.IsingPerceptron.cylinderCross line 561
  48. lemma OAI.IsingPerceptron.cylinderCross_prefix line 563
  49. lemma OAI.IsingPerceptron.abs_cylinderCross_le line 570
  50. lemma OAI.IsingPerceptron.measurable_referenceReplicaMean line 594
  51. theorem OAI.IsingPerceptron.finite_cylinder_reference_insertion line 605