OAI/Probability/InvariantIsing/Gaussian/GaussianPatternModel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian-pattern Hamiltonian with its diagonal self-interactions. The array is indexed by spin coordinate first and pattern coordinate second.

  1. def OAI.InvariantIsing.gaussianPatternArray line 13

    Also declared: ComparatorChallenges/InvariantIsing.lean:254 (same declaration text).

  2. def OAI.InvariantIsing.gaussianPatternCoupling line 16
  3. def OAI.InvariantIsing.gaussianPatternSum line 20

    Also declared: ComparatorChallenges/InvariantIsing.lean:257 (same declaration text).

  4. def OAI.InvariantIsing.gaussianPatternPressure line 24

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:261 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPatternPressure@path.

  5. lemma OAI.InvariantIsing.gaussianPatternCoupling_isHermitian line 28
  6. lemma OAI.InvariantIsing.quadraticEnergy_dotProduct line 32
  7. lemma OAI.InvariantIsing.gaussianPattern_energy line 37
  8. lemma OAI.InvariantIsing.gaussianPatternPressure_eq line 52
  9. lemma OAI.InvariantIsing.measurable_gaussianPatternPressure line 58