OAI/Probability/SKGap/Terminal/PairGibbsBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.siteVariance line 13
  2. def OAI.SKGap.weightedGradient line 16
  3. lemma OAI.SKGap.pairConditional_signed_bound line 19
  4. lemma OAI.SKGap.expectation_mono line 37
  5. lemma OAI.SKGap.gibbs_pair_signed_bound line 43
  6. lemma OAI.SKGap.siteVariance_pos line 69
  7. lemma OAI.SKGap.siteVariance_le_one line 76
  8. lemma OAI.SKGap.dirichlet_weighted line 79
  9. lemma OAI.SKGap.symmetric_fourth_cost line 84
  10. lemma OAI.SKGap.heatBathGenerator_square line 105
  11. theorem OAI.SKGap.gibbs_signed_curvature line 112