OAI/Probability/IsingPerceptron/VariationalDefs.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Variational Defs.

  1. def OAI.IsingPerceptron.gaussianTransform line 18

    Also declared: ComparatorChallenges/IsingFiniteness.lean:11 (same declaration text).

  2. structure OAI.IsingPerceptron.Partition line 23

    Also declared: ComparatorChallenges/IsingFiniteness.lean:16 (same declaration text).

  3. structure OAI.IsingPerceptron.FieldStep line 31

    Also declared: ComparatorChallenges/IsingFiniteness.lean:24 (same declaration text).

  4. def OAI.IsingPerceptron.stepAt line 38

    Also declared: ComparatorChallenges/IsingFiniteness.lean:31 (same declaration text).

  5. def OAI.IsingPerceptron.stepFunction line 43

    Also declared: ComparatorChallenges/IsingFiniteness.lean:36 (same declaration text).

  6. def OAI.IsingPerceptron.fieldRecursion line 48

    Also declared: ComparatorChallenges/IsingFiniteness.lean:41 (same declaration text).

  7. structure OAI.IsingPerceptron.OverlapStep line 56
  8. def OAI.IsingPerceptron.patternRecursion line 60
  9. def OAI.IsingPerceptron.pathMeasure line 67

    Also declared: ComparatorChallenges/IsingFiniteness.lean:49 (same declaration text).

  10. structure OAI.IsingPerceptron.OverlapPath line 70

    Also declared: ComparatorChallenges/IsingFiniteness.lean:52 (same declaration text).

  11. def OAI.IsingPerceptron.cellAverage line 77

    Also declared: ComparatorChallenges/IsingFiniteness.lean:59 (same declaration text).

  12. def OAI.IsingPerceptron.uniformPattern line 83

    Also declared: ComparatorChallenges/IsingFiniteness.lean:65 (same declaration text).

  13. def OAI.IsingPerceptron.patternFunctional line 92

    Also declared: ComparatorChallenges/IsingFiniteness.lean:74 (same declaration text).

  14. def OAI.IsingPerceptron.isingEntropy line 97

    Also declared: ComparatorChallenges/IsingFiniteness.lean:79 (same declaration text).

  15. def OAI.IsingPerceptron.variationalValue line 101

    Also declared: ComparatorChallenges/IsingFiniteness.lean:83 (same declaration text).

  16. def OAI.IsingPerceptron.unitMonotoneExtension line 114
  17. lemma OAI.IsingPerceptron.unitMonotoneExtension_eq line 117
  18. lemma OAI.IsingPerceptron.unitMonotoneExtension_mem line 121
  19. lemma OAI.IsingPerceptron.unitMonotoneExtension_monotone line 130
  20. lemma OAI.IsingPerceptron.overlapPath_representative line 143
  21. def OAI.IsingPerceptron.overlapPathOfMonotone line 150
  22. lemma OAI.IsingPerceptron.overlapPathOfMonotone_ae line 154
  23. theorem OAI.IsingPerceptron.enrichedMeanPressure_recursion line 167
  24. def OAI.IsingPerceptron.spinLaw line 218
  25. instance OAI.IsingPerceptron.spinLaw_probability line 220
  26. def OAI.IsingPerceptron.magneticEnergy line 224
  27. lemma OAI.IsingPerceptron.measurable_magneticEnergy line 227
  28. lemma OAI.IsingPerceptron.spinSign_integral line 231
  29. lemma OAI.IsingPerceptron.finiteLogIntegral_magnetic line 241
  30. lemma OAI.IsingPerceptron.logMean_independent_sum line 249
  31. lemma OAI.IsingPerceptron.HasLinearGrowth.scale_argument line 260
  32. lemma OAI.IsingPerceptron.gaussianTransform_positive_linearGrowth line 266
  33. lemma OAI.IsingPerceptron.measurable_gaussianTransform line 284
  34. lemma OAI.IsingPerceptron.gaussianFold_linearGrowth line 292
  35. lemma OAI.IsingPerceptron.magneticEnergy_add line 313
  36. lemma OAI.IsingPerceptron.enrichedIncrement_zero line 318
  37. def OAI.IsingPerceptron.magneticIncrementLaw line 334
  38. lemma OAI.IsingPerceptron.enrichedIncrementLaw_zero line 339
  39. lemma OAI.IsingPerceptron.logMean_magneticIncrement line 358
  40. def OAI.IsingPerceptron.magneticRecursion line 381
  41. lemma OAI.IsingPerceptron.magneticRecursion_growth line 386
  42. lemma OAI.IsingPerceptron.magneticRecursion_eq_fold line 394
  43. lemma OAI.IsingPerceptron.energyRecursion_magnetic line 404
  44. lemma OAI.IsingPerceptron.gaussian_linearGrowth_integrable line 451
  45. lemma OAI.IsingPerceptron.gaussianTransform_const_add line 458
  46. lemma OAI.IsingPerceptron.gaussianFold_const_add line 476
  47. lemma OAI.IsingPerceptron.poissonMeasure_zero_eq_dirac line 488
  48. def OAI.IsingPerceptron.magneticFieldValue line 508
  49. lemma OAI.IsingPerceptron.integral_magnetic_energyRecursion line 512
  50. theorem OAI.IsingPerceptron.enrichedMeanPressure_initial_zero line 536