OAI/MathematicalPhysics/CriticalSK/EntropyBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.scalar_entropy_upper line 10
  2. lemma OAI.CriticalSK.scalar_entropy_lower line 23
  3. lemma OAI.CriticalSK.variance_eq_second_moment line 39
  4. lemma OAI.CriticalSK.mean_square_pos_full line 45
  5. lemma OAI.CriticalSK.entropy_eq_centered_log line 55
  6. lemma OAI.CriticalSK.entropy_times_mean_le_variance line 59
  7. lemma OAI.CriticalSK.variance_le_entropy_square line 67
  8. lemma OAI.CriticalSK.exists_gibbs_lower line 80
  9. lemma OAI.CriticalSK.square_variance_bound line 89
  10. lemma OAI.CriticalSK.entropy_square_le_variance line 116
  11. lemma OAI.CriticalSK.exists_finite_logSobolev line 132
  12. lemma OAI.CriticalSK.entropy_ratios_bdd line 144
  13. lemma OAI.CriticalSK.variance_add_const line 157
  14. lemma OAI.CriticalSK.dirichlet_add_const line 161
  15. lemma OAI.CriticalSK.full_ratios_nonempty line 166
  16. lemma OAI.CriticalSK.relaxationTime_le_logSobolevConstant line 172