OAI/Probability/InvariantIsing/Gaussian/GordonWeights.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The two finite Gibbs levels in the Gaussian minimum--maximum comparison.

  1. lemma OAI.InvariantIsing.gordon_reference line 12
  2. def OAI.InvariantIsing.gordonRow line 15
  3. def OAI.InvariantIsing.gordonValue line 18
  4. def OAI.InvariantIsing.gordonInner line 21
  5. def OAI.InvariantIsing.gordonOuter line 24
  6. def OAI.InvariantIsing.gordonWeight line 27
  7. def OAI.InvariantIsing.gordonRowMean line 30
  8. def OAI.InvariantIsing.gordonMean line 33
  9. lemma OAI.InvariantIsing.gordonWeight_nonneg line 36
  10. lemma OAI.InvariantIsing.gordonWeight_le_one line 39
  11. lemma OAI.InvariantIsing.gordonWeight_sum line 46
  12. lemma OAI.InvariantIsing.gordonMean_eq_sum line 52
  13. lemma OAI.InvariantIsing.gordonRow_hasDerivAt line 57
  14. lemma OAI.InvariantIsing.gordonValue_hasDerivAt line 62
  15. lemma OAI.InvariantIsing.gordonWeight_hasDerivAt line 70