OAI/Probability/IsingPerceptron/ReplicaEnergyCovarianceBound.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Replica Energy Covariance Bound.

  1. lemma OAI.IsingPerceptron.replica_energy_covariance_bound line 15
  2. lemma OAI.IsingPerceptron.cylinderField_smul line 50
  3. lemma OAI.IsingPerceptron.cylinder_norm_smul line 60
  4. lemma OAI.IsingPerceptron.cylinderCross_smul_right line 66
  5. lemma OAI.IsingPerceptron.joint_cylinder_energy_covariance_bound line 74
  6. lemma OAI.IsingPerceptron.referenceReplicaMean_const_mul line 117
  7. lemma OAI.IsingPerceptron.referenceReplicaMean_const line 126
  8. lemma OAI.IsingPerceptron.referenceReplicaMean_add_bounded line 134
  9. lemma OAI.IsingPerceptron.cylinderCross_self line 147
  10. lemma OAI.IsingPerceptron.cylinderCross_bound line 150
  11. def OAI.IsingPerceptron.randomReplicaAverage line 159
  12. def OAI.IsingPerceptron.randomReplicaEnergy line 164
  13. lemma OAI.IsingPerceptron.integrable_random_scaled_mean line 170
  14. lemma OAI.IsingPerceptron.randomReplicaAverage_const line 180
  15. lemma OAI.IsingPerceptron.randomReplicaAverage_abs_le line 193
  16. theorem OAI.IsingPerceptron.randomReplicaEnergy_identity line 204
  17. theorem OAI.IsingPerceptron.countable_gaussian_gg_bound line 270
  18. lemma OAI.IsingPerceptron.cylinderCross_zero_left line 325
  19. lemma OAI.IsingPerceptron.cylinderCross_add_left line 327
  20. lemma OAI.IsingPerceptron.cylinderCross_single_left line 330
  21. lemma OAI.IsingPerceptron.cylinderCross_finset_left line 333
  22. def OAI.IsingPerceptron.featureCoefficients line 340
  23. lemma OAI.IsingPerceptron.featureCoefficients_apply line 343
  24. lemma OAI.IsingPerceptron.featureCoefficients_cross line 348
  25. lemma OAI.IsingPerceptron.featureCoefficients_diagonal line 363
  26. lemma OAI.IsingPerceptron.featureCoefficients_variance line 377
  27. def OAI.IsingPerceptron.labeledAddress line 383
  28. def OAI.IsingPerceptron.labeledCommonDepth line 387
  29. lemma OAI.IsingPerceptron.labeledAddress_length line 391
  30. lemma OAI.IsingPerceptron.labeledCommonDepth_le line 396
  31. lemma OAI.IsingPerceptron.labeledCommonDepth_self line 405
  32. lemma OAI.IsingPerceptron.labeled_prefix_eq_iff line 410
  33. instance OAI.IsingPerceptron.labeledLeafEncodable line 428
  34. def OAI.IsingPerceptron.treeFeatureTag line 430
  35. lemma OAI.IsingPerceptron.treeFeatureTag_cross line 434
  36. lemma OAI.IsingPerceptron.treeFeatureTag_injective line 449
  37. def OAI.IsingPerceptron.treeFieldCoefficients line 454
  38. lemma OAI.IsingPerceptron.treeFieldCoefficients_cross line 458
  39. def OAI.IsingPerceptron.pathIncrement line 478
  40. def OAI.IsingPerceptron.pathAmplitude line 482
  41. lemma OAI.IsingPerceptron.pathIncrement_nonneg line 484
  42. lemma OAI.IsingPerceptron.pathAmplitude_sq line 490
  43. lemma OAI.IsingPerceptron.pathIncrement_sum line 493
  44. lemma OAI.IsingPerceptron.pathIncrement_prefix line 499
  45. lemma OAI.IsingPerceptron.treeField_path_cross line 516
  46. def OAI.IsingPerceptron.tensorFeature line 525
  47. lemma OAI.IsingPerceptron.tensorFeature_cross line 528
  48. def OAI.IsingPerceptron.spinCoordinate line 536
  49. lemma OAI.IsingPerceptron.spinValue_sq line 539
  50. lemma OAI.IsingPerceptron.spinCoordinate_cross line 542
  51. lemma OAI.IsingPerceptron.spinOverlap_self line 547
  52. def OAI.IsingPerceptron.treeOverlap line 552
  53. def OAI.IsingPerceptron.monomialPath line 555
  54. lemma OAI.IsingPerceptron.monomialPath_monotone line 557
  55. lemma OAI.IsingPerceptron.monomialPath_nonneg line 563
  56. lemma OAI.IsingPerceptron.monomialPath_diag_le_one line 566
  57. def OAI.IsingPerceptron.monomialCoefficients line 572
  58. lemma OAI.IsingPerceptron.monomialCoefficients_cross line 576
  59. lemma OAI.IsingPerceptron.monomialCoefficients_variance line 585
  60. lemma OAI.IsingPerceptron.monomialCoefficients_variance_le line 591
  61. lemma OAI.IsingPerceptron.gaussian_pullback_measurePreserving line 597