OAI/MathematicalPhysics/CriticalSK/FunctionalMeasurability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalSK.variance_pos_iff_nonconstant line 13
2. lemma OAI.CriticalSK.dirichlet_pos_of_nonconstant line 35
3. lemma OAI.CriticalSK.entropy_square_pos_iff_nonconstant line 44
4. lemma OAI.CriticalSK.relaxationTime_eq_iSup line 64
5. lemma OAI.CriticalSK.logSobolevConstant_eq_iSup line 75
6. lemma OAI.CriticalSK.entropy_continuous line 89
7. lemma OAI.CriticalSK.relaxationTime_measurable line 94
8. lemma OAI.CriticalSK.logSobolevConstant_measurable line 108