OAI/Probability/InvariantIsing/Gaussian/GaussianPatternGroundFinite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual Gaussian-pattern maximum energies and their finite-temperature squeeze.

  1. def OAI.InvariantIsing.gaussianPatternGroundEnergy line 13

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

  2. lemma OAI.InvariantIsing.measurable_gaussianPatternGroundEnergy line 18
  3. lemma OAI.InvariantIsing.gaussianPatternGroundEnergy_squeeze line 31
  4. lemma OAI.InvariantIsing.gaussianPatternGroundEnergy_orbit line 56
  5. lemma OAI.InvariantIsing.abs_gaussianPatternGroundEnergy_le line 69
  6. lemma OAI.InvariantIsing.gaussianPatternGroundEnergy_nonneg line 77
  7. lemma OAI.InvariantIsing.gaussianPatternGroundEnergy_nonpos line 84