OAI/Probability/IsingPerceptron/EnergyShift.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Energy Shift.

  1. lemma OAI.IsingPerceptron.energyRecursion_add_const line 17
  2. def OAI.IsingPerceptron.scalarShiftLaw line 40
  3. lemma OAI.IsingPerceptron.scalarShiftLaw_exponentialNormMoments line 46
  4. lemma OAI.IsingPerceptron.logMean_scalarShift line 68
  5. theorem OAI.IsingPerceptron.energyRecursion_scalarShift line 92
  6. abbrev OAI.IsingPerceptron.EnrichedLabeledData line 144
  7. def OAI.IsingPerceptron.enrichedCoordinateLaw line 148
  8. instance OAI.IsingPerceptron.enrichedCoordinateLaw_probability line 154
  9. def OAI.IsingPerceptron.enrichedCoordinatePressure line 162
  10. def OAI.IsingPerceptron.enrichedToNoise line 170
  11. lemma OAI.IsingPerceptron.enrichedToNoise_preserving line 174
  12. theorem OAI.IsingPerceptron.enrichedCoordinatePressure_eq_noise line 195
  13. theorem OAI.IsingPerceptron.enrichedCoordinatePressure_field_cap line 232
  14. def OAI.IsingPerceptron.nodeAddress line 268
  15. lemma OAI.IsingPerceptron.nodeAddress_injective line 273
  16. def OAI.IsingPerceptron.nodeAt line 298
  17. lemma OAI.IsingPerceptron.nodeAddress_nodeAt line 302
  18. lemma OAI.IsingPerceptron.nodeAddress_length_some line 311
  19. lemma OAI.IsingPerceptron.nodeAddress_nodeAt_length line 320
  20. def OAI.IsingPerceptron.enrichedNodeTag line 326
  21. lemma OAI.IsingPerceptron.enrichedNodeTag_injective line 330
  22. def OAI.IsingPerceptron.enrichedGaussianNodes line 359
  23. lemma OAI.IsingPerceptron.measurable_enrichedGaussianNodes line 363
  24. theorem OAI.IsingPerceptron.enrichedGaussianNodes_law line 368
  25. theorem OAI.IsingPerceptron.enrichedGaussianRootForest_law line 390
  26. lemma OAI.IsingPerceptron.cylinderField_tag line 409
  27. lemma OAI.IsingPerceptron.cylinderField_feature line 414
  28. def OAI.IsingPerceptron.edgeAt line 422
  29. lemma OAI.IsingPerceptron.nodeAt_zero line 426
  30. lemma OAI.IsingPerceptron.nodeAt_succ line 429
  31. lemma OAI.IsingPerceptron.labeledEnergy_edge_sum line 435
  32. lemma OAI.IsingPerceptron.labeledEnergy_node_sum line 446
  33. lemma OAI.IsingPerceptron.enrichedIncrement_nodes line 454
  34. lemma OAI.IsingPerceptron.cylinderField_external_nodes line 462
  35. lemma OAI.IsingPerceptron.cylinderField_monomial_nodes line 473
  36. lemma OAI.IsingPerceptron.cylinderField_enriched_nodes line 493
  37. theorem OAI.IsingPerceptron.enrichedEnergy_eq_cylinder line 509
  38. lemma OAI.IsingPerceptron.preserving_three_rotate line 541
  39. lemma OAI.IsingPerceptron.preserving_four_shuffle line 549
  40. abbrev OAI.IsingPerceptron.EnrichedCylinderBase line 561
  41. abbrev OAI.IsingPerceptron.EnrichedCylinderData line 562
  42. def OAI.IsingPerceptron.enrichedCylinderBaseLaw line 564
  43. def OAI.IsingPerceptron.enrichedCylinderLaw line 568
  44. instance OAI.IsingPerceptron.enrichedCylinderBaseLaw_probability line 572
  45. instance OAI.IsingPerceptron.enrichedCylinderLaw_probability line 578
  46. def OAI.IsingPerceptron.enrichedCylinderToCoordinates line 584
  47. theorem OAI.IsingPerceptron.enrichedCylinderToCoordinates_preserving line 589
  48. def OAI.IsingPerceptron.enrichedCylinderPressure line 609
  49. theorem OAI.IsingPerceptron.enrichedCylinderPressure_eq_coordinates line 615
  50. theorem OAI.IsingPerceptron.enrichedCylinderPressure_field_cap line 632