OAI/Probability/IsingPerceptron/NamespaceSplit.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Namespace Split.

  1. abbrev OAI.IsingPerceptron.OtherNamespaces line 16
  2. def OAI.IsingPerceptron.otherNamespacesLaw line 18
  3. instance OAI.IsingPerceptron.otherNamespacesLaw_probability line 21
  4. def OAI.IsingPerceptron.gaussianNamespaceSplit line 25
  5. lemma OAI.IsingPerceptron.measurable_gaussianNamespaceSplit line 28
  6. lemma OAI.IsingPerceptron.gaussianNamespaceSplit_law line 32
  7. def OAI.IsingPerceptron.gaussianNamespaceJoin line 64
  8. lemma OAI.IsingPerceptron.measurable_gaussianNamespaceJoin line 68
  9. lemma OAI.IsingPerceptron.gaussianNamespaceJoin_split line 77
  10. lemma OAI.IsingPerceptron.gaussianNamespaceJoin_law line 85
  11. lemma OAI.IsingPerceptron.gaussianNamespaceJoin_selected line 92
  12. lemma OAI.IsingPerceptron.gaussianNamespaceJoin_other line 96
  13. theorem OAI.IsingPerceptron.gaussianNamespaceJoin_preserving line 101
  14. lemma OAI.IsingPerceptron.cylinderField_enriched_expand line 106
  15. lemma OAI.IsingPerceptron.cylinderField_enriched_update line 117
  16. lemma OAI.IsingPerceptron.cylinderField_enriched_frozen line 143
  17. lemma OAI.IsingPerceptron.cylinderField_enriched_insert line 173
  18. lemma OAI.IsingPerceptron.namespaceInsertion_preserving line 185
  19. def OAI.IsingPerceptron.gibbsProbability line 202
  20. instance OAI.IsingPerceptron.gibbsProbability_probability line 205
  21. lemma OAI.IsingPerceptron.gibbsProbability_eq_tilted line 215
  22. lemma OAI.IsingPerceptron.measurable_random_tilted_measure line 221
  23. lemma OAI.IsingPerceptron.measurable_gibbsProbability line 242
  24. lemma OAI.IsingPerceptron.integrable_exp_bounded_add line 250
  25. lemma OAI.IsingPerceptron.gibbsProbability_fold line 262
  26. lemma OAI.IsingPerceptron.cgf_fold line 275
  27. lemma OAI.IsingPerceptron.quadratic_minimum_subtract_constant line 289
  28. lemma OAI.IsingPerceptron.centered_sub_L1_bound line 295
  29. lemma OAI.IsingPerceptron.measurable_labeledSpinReference line 322
  30. abbrev OAI.IsingPerceptron.EnrichedFrozenData line 337
  31. def OAI.IsingPerceptron.enrichedFrozenLaw line 340
  32. instance OAI.IsingPerceptron.enrichedFrozenLaw_probability line 344
  33. def OAI.IsingPerceptron.enrichedInsert line 350
  34. lemma OAI.IsingPerceptron.enrichedInsert_preserving line 354
  35. def OAI.IsingPerceptron.enrichedFrozenHamiltonian line 360
  36. lemma OAI.IsingPerceptron.measurable_patternBase_infinite line 367
  37. lemma OAI.IsingPerceptron.measurable_enrichedFrozenHamiltonian line 386
  38. def OAI.IsingPerceptron.enrichedFrozenReference line 404
  39. instance OAI.IsingPerceptron.enrichedFrozenReference_probability line 409
  40. lemma OAI.IsingPerceptron.measurable_enrichedFrozenReference line 417
  41. lemma OAI.IsingPerceptron.update_abs_le_two line 426
  42. lemma OAI.IsingPerceptron.enrichedCylinder_exp_ae line 433
  43. def OAI.IsingPerceptron.perturbationAmplitude line 457
  44. lemma OAI.IsingPerceptron.perturbationAmplitude_pos line 460
  45. lemma OAI.IsingPerceptron.enrichedInsertedPressure_eq line 465
  46. lemma OAI.IsingPerceptron.enrichedFrozen_exp_ae line 485
  47. lemma OAI.IsingPerceptron.enrichedInserted_exp_ae line 515
  48. theorem OAI.IsingPerceptron.enriched_cgf_eq_pressure_difference line 540