OAI/Probability/IsingPerceptron/TiltedLabelLaw.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Tilted Label Law.

  1. lemma OAI.IsingPerceptron.measurable_labeledSpinReference_general line 18
  2. lemma OAI.IsingPerceptron.measurable_cascadeCoordinateEnergy line 33
  3. lemma OAI.IsingPerceptron.measurable_cascadeCoordinateLog line 45
  4. def OAI.IsingPerceptron.cascadeCoordinateLog line 53
  5. lemma OAI.IsingPerceptron.scalarCoordinate_cgf_eq_ae line 57
  6. lemma OAI.IsingPerceptron.scalarCoordinate_log_difference_mean line 78
  7. lemma OAI.IsingPerceptron.scalarCoordinate_cgf_mean line 103
  8. theorem OAI.IsingPerceptron.cascadeCoordinate_tilted_label_tail line 120
  9. lemma OAI.IsingPerceptron.enrichedEnergyCoords_preserving line 166
  10. def OAI.IsingPerceptron.enrichedRootLaw line 179
  11. instance OAI.IsingPerceptron.enrichedRootLaw_probability line 184
  12. def OAI.IsingPerceptron.enrichedToEnergyCoords line 188
  13. lemma OAI.IsingPerceptron.enrichedToEnergyCoords_preserving line 192
  14. lemma OAI.IsingPerceptron.enrichedHamiltonian_eq_energyCoords line 198
  15. lemma OAI.IsingPerceptron.measurable_cascadeCoordinateReplicaMean line 210
  16. lemma OAI.IsingPerceptron.cascadeCoordinate_tilted_label_tail_random line 231
  17. theorem OAI.IsingPerceptron.enriched_tilted_label_tail line 253
  18. lemma OAI.IsingPerceptron.measurable_countable_pi line 286
  19. lemma OAI.IsingPerceptron.measurable_countable_infinitePi line 305
  20. def OAI.IsingPerceptron.replicaKernel line 334
  21. instance OAI.IsingPerceptron.replicaKernel_markov line 339
  22. def OAI.IsingPerceptron.replicaLaw line 348
  23. instance OAI.IsingPerceptron.replicaLaw_probability line 353
  24. lemma OAI.IsingPerceptron.replica_prefix_map line 358
  25. lemma OAI.IsingPerceptron.replicaLaw_integral_bounded line 368
  26. lemma OAI.IsingPerceptron.replicaLaw_integral_prefix line 383
  27. abbrev OAI.IsingPerceptron.JointEntry line 396
  28. abbrev OAI.IsingPerceptron.JointArray line 397
  29. def OAI.IsingPerceptron.sampledOverlapArray line 399
  30. lemma OAI.IsingPerceptron.measurable_sampledOverlapArray line 402
  31. def OAI.IsingPerceptron.overlapArrayLaw line 413
  32. theorem OAI.IsingPerceptron.jointArrayLaw_subsequence line 421
  33. lemma OAI.IsingPerceptron.jointArray_tendsto_integral line 428
  34. abbrev OAI.IsingPerceptron.JointBlock line 436
  35. def OAI.IsingPerceptron.entryCoordinate line 438
  36. lemma OAI.IsingPerceptron.continuous_entryCoordinate line 440
  37. lemma OAI.IsingPerceptron.entryCoordinate_ext line 445
  38. def OAI.IsingPerceptron.blockPairCoordinate line 451
  39. lemma OAI.IsingPerceptron.continuous_blockPairCoordinate line 457
  40. lemma OAI.IsingPerceptron.blockPairCoordinate_ext line 463
  41. theorem OAI.IsingPerceptron.block_pair_monomials_unique line 474
  42. def OAI.IsingPerceptron.jointBlockView line 534
  43. def OAI.IsingPerceptron.jointBlockLink line 536
  44. lemma OAI.IsingPerceptron.continuous_jointBlockView line 539
  45. lemma OAI.IsingPerceptron.continuous_jointBlockLink line 543
  46. lemma OAI.IsingPerceptron.compact_integrable line 547
  47. def OAI.IsingPerceptron.HasEntryGhirlandaGuerra line 552
  48. theorem OAI.IsingPerceptron.joint_monomial_measure_identity line 562
  49. theorem OAI.IsingPerceptron.joint_monomialGG_measurable line 607